mathlib

249f1072 - feat(algebra/order/monoid_lemmas): remove duplicates, add missing lemmas, fix inconsistencies (#13494)

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. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>