Commit 2026-02-10 13:35 040cf2f4

View on Github →

chore: cleanup using new to_dual capabilities (#34879) This PR gets rid of some to_dual existing that can be resolved now that to_dual can insert cast when translating. This PR adds 2 new definitions: gtEmbedding and toRelIsoGT.

Estimated changes

Modified Mathlib/Order/Directed.lean

deleted theorem Antitone.directed_ge

deleted theorem Monotone.directed_ge

Modified Mathlib/Order/Hom/Basic.lean

deleted theorem OrderIso.symm_apply_le

deleted theorem OrderIso.symm_apply_lt

added theorem OrderIso.toRelIsoGT_symm

Modified Mathlib/Order/Shrink.lean

Modified Mathlib/Order/WithBot.lean

deleted theorem WithTop.coe_mono

deleted theorem WithTop.coe_strictMono

deleted theorem WithTop.monotone_iff

deleted theorem WithTop.monotone_map_iff

deleted theorem WithTop.strictAnti_iff

deleted theorem WithTop.strictMono_iff

deleted theorem WithTop.strictMono_map_iff

Modified Mathlib/Tactic/Translate/ToDual.lean