refactor(algebra/order/with_zero): Generalize lemmas (#16240)

Generalize the lemmas introduced in #15644 to monoids + covariant classes.

src/algebra/order/monoid_lemmas.lean

@@ -758,6 +758,31 @@ iff.intro
    and.intro ‹a = 1› ‹b = 1›)
   (assume ⟨ha', hb'⟩, by rw [ha', hb', mul_one])
 
+section left
+variables [covariant_class α α (*) (≤)] {a b : α}
+
+@[to_additive eq_zero_of_add_nonneg_left]
+lemma eq_one_of_one_le_mul_left (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : a = 1 :=
+ha.eq_of_not_lt $ λ h, hab.not_lt $ mul_lt_one_of_lt_of_le h hb
+
+@[to_additive]
+lemma eq_one_of_mul_le_one_left (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : a = 1 :=
+ha.eq_of_not_gt $ λ h, hab.not_lt $ one_lt_mul_of_lt_of_le' h hb
+
+end left
+
+section right
+variables [covariant_class α α (swap (*)) (≤)] {a b : α}
+
+@[to_additive eq_zero_of_add_nonneg_right]
+lemma eq_one_of_one_le_mul_right (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : b = 1 :=
+hb.eq_of_not_lt $ λ h, hab.not_lt $ right.mul_lt_one_of_le_of_lt ha h
+
+@[to_additive]
+lemma eq_one_of_mul_le_one_right (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : b = 1 :=
+hb.eq_of_not_gt $ λ h, hab.not_lt $ right.one_lt_mul_of_le_of_lt ha h
+
+end right
 end partial_order
 
 section linear_order

src/algebra/order/with_zero.lean

@@ -111,8 +111,12 @@ variables [linear_ordered_comm_group_with_zero α]
 lemma zero_lt_one₀ : (0 : α) < 1 :=
 lt_of_le_of_ne zero_le_one zero_ne_one
 
+-- TODO: Do we really need the following two?
+
+/-- Alias of `mul_le_one'` for unification. -/
 lemma mul_le_one₀ (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1 := mul_le_one' ha hb
 
+/-- Alias of `one_le_mul'` for unification. -/
 lemma one_le_mul₀ (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b := one_le_mul ha hb
 
 lemma le_of_le_mul_right (h : c ≠ 0) (hab : a * c ≤ b * c) : a ≤ b :=
@@ -202,22 +206,6 @@ by rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
 lemma div_le_iff₀ (hc : c ≠ 0) : a / c ≤ b ↔ a ≤ b*c :=
 by rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
 
-lemma eq_one_of_mul_eq_one_left (ha : a ≤ 1) (hb : b ≤ 1) (hab : a * b = 1) : a = 1 :=
-le_antisymm ha $ (inv_le_one₀ $ left_ne_zero_of_mul_eq_one hab).mp $
-  eq_inv_of_mul_eq_one_right hab ▸ hb
-
-lemma eq_one_of_mul_eq_one_right (ha : a ≤ 1) (hb : b ≤ 1) (hab : a * b = 1) : b = 1 :=
-le_antisymm hb $ (inv_le_one₀ $ right_ne_zero_of_mul_eq_one hab).mp $
-  eq_inv_of_mul_eq_one_left hab ▸ ha
-
-lemma eq_one_of_mul_eq_one_left' (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b = 1) : a = 1 :=
-le_antisymm
-  ((one_le_inv₀ $ left_ne_zero_of_mul_eq_one hab).mp $ eq_inv_of_mul_eq_one_right hab ▸ hb) ha
-
-lemma eq_one_of_mul_eq_one_right' (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b = 1) : b = 1 :=
-le_antisymm
-  ((one_le_inv₀ $ right_ne_zero_of_mul_eq_one hab).mp $ eq_inv_of_mul_eq_one_left hab ▸ ha) hb
-
 /-- `equiv.mul_left₀` as an order_iso on a `linear_ordered_comm_group_with_zero.`.
 
 Note that `order_iso.mul_left₀` refers to the `linear_ordered_field` version. -/