mathlib3

47ed97f3 - feat(algebra/ordered_monoid_lemmas + fixes): consistent use of `covariant` and `contravariant` in `ordered_monoid_lemmas` (#7876)

feat(algebra/ordered_monoid_lemmas + fixes): consistent use of `covariant` and `contravariant` in `ordered_monoid_lemmas` (#7876) This PR breaks off a part of PR #7645. Here, I start using more consistently `covariant_class` and `contravariant_class` in the file `algebra/ordered_monoid_lemmas`. This PR is simply intended as a stepping stone to merging the bigger one (#7645) and receiving "personalized comments on it! Summary of changes: -- New lemmas * `@[to_additive add_nonneg] lemma one_le_mul_right` * `@[to_additive] lemma le_mul_of_le_of_le_one` * `@[to_additive] lemma mul_lt_mul_of_lt_of_lt` * `@[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one` * `@[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one` * `@[to_additive] lemma left.mul_lt_one_of_lt_of_lt_one` * `@[to_additive] lemma right.mul_lt_one_of_lt_of_lt_one` * `@[to_additive right.add_nonneg] lemma right.one_le_mul` * `@[to_additive right.pos_add] lemma right.one_lt_mul` -- Lemmas that have merged with their unprimed versions due to diminished typeclass assumptions * `@[to_additive] lemma lt_mul_of_one_le_of_lt'` * `@[to_additive] lemma lt_mul_of_one_lt_of_lt'` * `@[to_additive] lemma mul_le_of_le_of_le_one'` * `@[to_additive] lemma mul_le_of_le_one_of_le'` * `@[to_additive] lemma mul_lt_of_lt_of_le_one'` * `@[to_additive] lemma mul_lt_of_lt_of_lt_one'` * `@[to_additive] lemma mul_lt_of_lt_one_of_lt'` * the three lemmas * * `@[to_additive] lemma mul_lt_of_le_one_of_lt'`, * * `mul_lt_one_of_le_one_of_lt_one`, * * `mul_lt_one_of_le_one_of_lt_one'` all merged into `mul_lt_of_le_one_of_lt` -- Lemma `@[to_additive] lemma mul_lt_one` broke into * `@[to_additive] lemma left.mul_lt_one` * `@[to_additive] lemma right.mul_lt_one` depending on typeclass assumptions -- Lemmas that became a direct application of another lemma * `@[to_additive] lemma mul_lt_one_of_lt_one_of_le_one` and `mul_lt_one_of_lt_one_of_le_one'` are applications of `mul_lt_of_lt_of_le_one` * `@[to_additive] lemma mul_lt_one'` is an application of `mul_lt_of_lt_of_lt_one` -- Lemma `@[to_additive] lemma mul_eq_one_iff_eq_one_of_one_le` changed name to `mul_eq_one_iff_eq_one_of_one_le`. The multiplicative version is never used. The additive version, `add_eq_zero_iff_eq_zero_of_nonneg` is used: I changed the occurrences in favour of the shorter name. -- Lemma `@[to_additive add_nonpos] lemma mul_le_one'` continues as ```lean alias mul_le_of_le_of_le_one ← mul_le_one' attribute [to_additive add_nonpos] mul_le_one' ``` <!-- Name changes: * lemma `mul_le_of_le_one_of_le'` became `mul_le_of_le_one_of_le`; * lemma `lt_mul_of_one_le_of_lt'` became `lt_mul_of_one_le_of_lt`; * lemma `add_eq_zero_iff_eq_zero_of_nonneg` became `add_eq_zero_iff'`. (Really, the lemmas above are the ones that were used outside of the PR: the two `mul` ones have a corresponding `to_additive` version and the `add` one is the `to_additive` version of `mul_eq_one_iff_eq_one_of_one_le`.) -->