Commit 2023-05-16 13:10 3eaefa47

View on Github →

fix: re-port Init/Algebra/Order (#4000) The ad-hoc port was added in #18, but the #aligns were all missing and two defs were incorrectly promoted to an instance. The absense of these instances reveals some missing instances that need to be added (and were found via unfolding in Lean 3).

Estimated changes

modified theorem eq_or_lt_of_not_lt
modified theorem ge_trans
modified theorem gt_irrefl
modified theorem gt_trans
modified theorem le_iff_lt_or_eq
modified theorem le_imp_le_of_lt_imp_lt
modified theorem le_not_le_of_lt
modified theorem le_of_eq
modified theorem le_of_eq_or_lt
modified theorem le_of_lt_or_eq
modified theorem le_of_not_ge
modified theorem le_of_not_gt
modified theorem le_of_not_le
modified theorem le_of_not_lt
modified theorem le_or_gt
modified theorem le_refl
added def ltByCases
modified theorem lt_asymm
deleted def lt_by_cases
modified theorem lt_iff_le_not_le
modified theorem lt_iff_not_ge
modified theorem lt_irrefl
modified theorem lt_of_le_not_le
modified theorem lt_of_le_of_ne
modified theorem lt_of_not_ge
modified theorem lt_or_eq_of_le
modified theorem lt_or_ge
modified theorem ne_of_gt
modified theorem ne_of_lt
modified theorem not_le
modified theorem not_le_of_gt
modified theorem not_lt
modified theorem not_lt_of_ge
modified theorem not_lt_of_gt