feat(algebra/order/monoid_lemmas): remove duplicates, add missing lem…

…mas, 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>

src/algebra/group_power/order.lean

@@ -54,7 +54,7 @@ begin
   induction l with l IH,
   { simpa using ha },
   { rw pow_succ,
-    exact one_lt_mul' ha IH }
+    exact one_lt_mul'' ha IH }
 end
 
 @[to_additive nsmul_neg]

src/algebra/order/group.lean

@@ -820,7 +820,7 @@ lemma div_le_inv_mul_iff [covariant_class α α (swap (*)) (≤)] :
   a / b ≤ a⁻¹ * b ↔ a ≤ b :=
 begin
   rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff],
-  exact ⟨λ h, not_lt.mp (λ k, not_lt.mpr h (mul_lt_mul''' k k)), λ h, mul_le_mul' h h⟩,
+  exact ⟨λ h, not_lt.mp (λ k, not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k)), λ h, mul_le_mul' h h⟩,
 end
 
 /-  What is the point of this lemma?  See comment about `div_le_inv_mul_iff` above. -/

src/algebra/order/monoid.lean

@@ -167,7 +167,7 @@ def function.injective.linear_ordered_comm_monoid [linear_ordered_comm_monoid α
   .. linear_order.lift f hf }
 
 lemma bit0_pos [ordered_add_comm_monoid α] {a : α} (h : 0 < a) : 0 < bit0 a :=
-add_pos h h
+add_pos' h h
 
 namespace units