Commit 2023-09-14 10:14 9476eae9

chore(Co(ntra)variantClass): generalize and remove duplicates (#6677) 4 files have major changes: Algebra/CovariantAndContravariant.lean

• Add new theorem contravariant_le_iff_contravariant_lt_and_eq.
• Add covariantClass_le_of_lt generalizing and replacing Mul.to_covariantClass_left/right in Algebra/Order/Monoid/Defs.lean
• Replace CommSemigroup by IsSymmOp N N mu and replace CancelSemigroup by IsMulCancel, removing superfluous associativity assumption.
• new theorems covariant_lt_of_covariant_le_of_contravariant_eq and contravariant_le_of_contravariant_eq_and_lt that could replace eight instances when appropriate refactoring is in place.
• Golfs
• Fix changed names in other files. Algebra/Order/Monoid/Lemmas.lean
• Generalize mul_eq_mul_iff_eq_and_eq and remove the less general Left/Right.mul_eq_mul_iff_eq_and_eq.
• Move mul_le_mul_iff_of_ge.
• Introduce the more general Left/Right versions of min_le_max_of_mul_le_mul.
• Move min_lt_max_of_mul_lt_mul here from Algebra/GroupPower/Order.lean.
• Replace CommSemigroup by IsSymmOp. Algebra/Order/Monoid/Basic.lean
• Remove eq_and_eq_of_le_of_le_of_mul_le as it's just one direction of mul_le_mul_iff_of_ge but with more assumptions. Algebra/Order/Ring/Lemmas.lean
• Generalize two versions of mul_eq_mul_iff_eq_and_eq_of_pos
• Golfs Changes to Algebra/Group/UniqueProds.lean and Algebra/MonoidAlgebra/NoZeroDivisors.lean are in declarations that will be removed by #6723.