Commit 2025-11-21 05:52 337d737c

View on Github →

chore(Order/Basic): use @[to_dual] for Preorder/PartialOrder (#31852) This PR tags some part of Mathlib.Order.Basic with @[to_dual]. This PR adds a lot of new declarations in cases where there used to not be a dual declaration (and even a new simp lemma ne_iff_gt_iff_ge). The sections for pure LE/LT, and LinearOrder in this file are left to be tagged for future PRs.

Estimated changes

Modified Mathlib/Order/Basic.lean

deleted theorem LE.le.ge_iff_eq'

modified theorem LE.le.ge_iff_eq

deleted theorem LE.le.lt_iff_ne'

modified theorem LE.le.lt_iff_ne

deleted theorem LE.le.not_lt_iff_eq'

modified theorem LE.le.not_lt_iff_eq

deleted theorem LT.lt.ne'

deleted theorem Ne.lt_of_le'

deleted theorem eq_of_forall_ge_iff

deleted theorem eq_of_le_of_not_lt'

deleted theorem eq_or_lt_of_le'

deleted theorem forall_ge_iff_le

deleted theorem le_imp_eq_iff_le_imp_ge'

modified theorem le_imp_le_of_le_of_le

deleted theorem le_of_forall_ge

modified theorem le_of_subsingleton

modified theorem lt_imp_lt_of_le_of_le

modified theorem lt_self_iff_false

modified theorem ne_iff_lt_iff_le