Commit 2022-05-28 15:49 249f1072

feat(algebra/order/monoid_lemmas): remove duplicates, add missing lemmas, fix inconsistencies (#13494) Changes in the order: mul_lt_mul''' has asymmetric typeclass assumptions. So I did the following 3 changes. Rename mul_lt_mul''' to left.mul_lt_mul Make an alias mul_lt_mul''' of mul_lt_mul_of_lt_of_lt Add right.mul_lt_mul Move le_mul_of_one_le_left' and mul_le_of_le_one_left' together with similar lemmas. Move lt_mul_of_one_lt_left' together with similar lemmas. Add mul_lt_of_lt_one_right' and mul_lt_of_lt_one_left'. These are analogs of other lemmas. Following are changes of lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c, b ≤ c → 1 ≤ a → b ≤ c * a, a ≤ 1 → b ≤ c → a * b ≤ c and 1 ≤ a → b ≤ c → b ≤ a * c. With the following changes, these 4 sections will be very similar. For b ≤ c → a ≤ 1 → b * a ≤ c: Remove alias mul_le_of_le_of_le_one ← mul_le_one'. This naming is not consistent with left.mul_lt_one. Add mul_lt_of_lt_of_lt_one'. Add left.mul_le_one. Add left.mul_lt_one_of_le_of_lt. Add left.mul_lt_one_of_lt_of_le. Add left.mul_lt_one'. For b ≤ c → 1 ≤ a → b ≤ c * a: Rename le_mul_of_le_of_le_one to le_mul_of_le_of_one_le. Remove lt_mul_of_lt_of_one_le'. It's exactly the same as lt_mul_of_lt_of_one_le. Rename one_le_mul_right to left.one_le_mul. Rename one_le_mul to left.one_le_mul. Rename one_lt_mul_of_lt_of_le' to left.one_lt_mul_of_lt_of_le'. Add left.one_lt_mul. Rename one_lt_mul' to left.one_lt_mul'. For a ≤ 1 → b ≤ c → a * b ≤ c: Add mul_lt_of_lt_one_of_lt'. Add right.mul_le_one. Add right.mul_lt_one_of_lt_of_le. Add right.mul_lt_one'. For 1 ≤ a → b ≤ c → b ≤ a * c: Rename lt_mul_of_one_lt_of_lt to lt_mul_of_one_lt_of_lt'. Add lt_mul_of_one_lt_of_lt. Add right.one_lt_mul_of_lt_of_le. Rename one_lt_mul_of_le_of_lt' to right.one_lt_mul_of_le_of_lt. Add right.one_lt_mul'. Then create aliases for all left lemmas in these 4 sections. Rename mul_eq_mul_iff_eq_and_eq to left.mul_eq_mul_iff_eq_and_eq. Add right.mul_eq_mul_iff_eq_and_eq. Make an alias mul_eq_mul_iff_eq_and_eq of left.mul_eq_mul_iff_eq_and_eq. Same for additive version. However, the implicit parameter inconsistency has not been resolved. It affects too many files.