Commit 2024-10-08 06:33 8f68ff90

View on Github →

feat: LawfulOrd and LinearOrder (#12082)

depends on: #12068
depends on: leanprover/std4#730 This adds the necessary instances for types from Mathlib to play well with the new classes from Std. This solves one of the mathlibSorry's from the EmptyHexagon project.

Estimated changes

Modified Mathlib/Data/Prod/Lex.lean

added theorem Ord.lex_eq

added theorem Prod.Lex.compare_def

added theorem lexOrd_eq

Modified Mathlib/Order/Defs.lean

added theorem cmp_eq_compare

added theorem cmp_eq_compareOfLessAndEq

Modified Mathlib/Order/Synonym.lean

Modified Mathlib/Order/ULift.lean

added theorem ULift.down_beq

added theorem ULift.up_beq