refactor(algebra/group/defs): use is_left_cancel_mul etc (#17884)

urkud · urkud · commit 2e0975f6a25d · 2022-12-10T19:33:30.000Z
The Lean 4 version is here: leanprover-community/mathlib4#945.
diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean
@@ -133,6 +133,57 @@ class is_cancel_add (G : Type u) [has_add G]
 
 attribute [to_additive] is_cancel_mul
 
+section is_left_cancel_mul
+variables [is_left_cancel_mul G] {a b c : G}
+
+@[to_additive]
+lemma mul_left_cancel : a * b = a * c → b = c :=
+is_left_cancel_mul.mul_left_cancel a b c
+
+@[to_additive]
+lemma mul_left_cancel_iff : a * b = a * c ↔ b = c :=
+⟨mul_left_cancel, congr_arg _⟩
+
+@[to_additive]
+theorem mul_right_injective (a : G) : function.injective ((*) a) :=
+λ b c, mul_left_cancel
+
+@[simp, to_additive]
+theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
+(mul_right_injective a).eq_iff
+
+@[to_additive]
+theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
+(mul_right_injective a).ne_iff
+
+end is_left_cancel_mul
+
+section is_right_cancel_mul
+
+variables [is_right_cancel_mul G] {a b c : G}
+
+@[to_additive]
+lemma mul_right_cancel : a * b = c * b → a = c :=
+is_right_cancel_mul.mul_right_cancel a b c
+
+@[to_additive]
+lemma mul_right_cancel_iff : b * a = c * a ↔ b = c :=
+⟨mul_right_cancel, congr_arg _⟩
+
+@[to_additive]
+theorem mul_left_injective (a : G) : function.injective (λ x, x * a) :=
+λ b c, mul_right_cancel
+
+@[simp, to_additive]
+theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
+(mul_left_injective a).eq_iff
+
+@[to_additive]
+theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
+(mul_left_injective a).ne_iff
+
+end is_right_cancel_mul
+
 end has_mul
 
 /-- A semigroup is a type with an associative `(*)`. -/
@@ -185,11 +236,7 @@ instance comm_semigroup.to_is_commutative : is_commutative G (*) :=
 `is_right_cancel_add G`."]
 lemma comm_semigroup.is_right_cancel_mul.to_is_left_cancel_mul (G : Type u) [comm_semigroup G]
   [is_right_cancel_mul G] : is_left_cancel_mul G :=
-{ mul_left_cancel := λ a b c h,
-  begin
-    rw [mul_comm a b, mul_comm a c] at h,
-    exact is_right_cancel_mul.mul_right_cancel _ _ _ h
-  end }
+⟨λ a b c h, mul_right_cancel $ (mul_comm _ _).trans (h.trans $ mul_comm _ _)⟩
 
 /-- Any `comm_semigroup G` that satisfies `is_left_cancel_mul G` also satisfies
 `is_right_cancel_mul G`. -/
@@ -198,37 +245,23 @@ lemma comm_semigroup.is_right_cancel_mul.to_is_left_cancel_mul (G : Type u) [com
 `is_left_cancel_add G`."]
 lemma comm_semigroup.is_left_cancel_mul.to_is_right_cancel_mul (G : Type u) [comm_semigroup G]
   [is_left_cancel_mul G] : is_right_cancel_mul G :=
-{ mul_right_cancel := λ a b c h,
-  begin
-    rw [mul_comm a b, mul_comm c b] at h,
-    exact is_left_cancel_mul.mul_left_cancel _ _ _ h
-  end }
+⟨λ a b c h, mul_left_cancel $ (mul_comm _ _).trans (h.trans $ mul_comm _ _)⟩
 
 /-- Any `comm_semigroup G` that satisfies `is_left_cancel_mul G` also satisfies
 `is_cancel_mul G`. -/
 @[to_additive add_comm_semigroup.is_left_cancel_add.to_is_cancel_add "Any `add_comm_semigroup G`
 that satisfies `is_left_cancel_add G` also satisfies `is_cancel_add G`."]
 lemma comm_semigroup.is_left_cancel_mul.to_is_cancel_mul (G : Type u) [comm_semigroup G]
   [is_left_cancel_mul G] : is_cancel_mul G :=
-{ mul_left_cancel := is_left_cancel_mul.mul_left_cancel,
-  mul_right_cancel := λ a b c h,
-  begin
-    rw [mul_comm a b, mul_comm c b] at h,
-    exact is_left_cancel_mul.mul_left_cancel _ _ _ h
-  end }
+{ .. ‹is_left_cancel_mul G›, .. comm_semigroup.is_left_cancel_mul.to_is_right_cancel_mul G }
 
 /-- Any `comm_semigroup G` that satisfies `is_right_cancel_mul G` also satisfies
 `is_cancel_mul G`. -/
 @[to_additive add_comm_semigroup.is_right_cancel_add.to_is_cancel_add "Any `add_comm_semigroup G`
 that satisfies `is_right_cancel_add G` also satisfies `is_cancel_add G`."]
 lemma comm_semigroup.is_right_cancel_mul.to_is_cancel_mul (G : Type u) [comm_semigroup G]
   [is_right_cancel_mul G] : is_cancel_mul G :=
-{ mul_left_cancel := λ a b c h,
-  begin
-    rw [mul_comm a b, mul_comm a c] at h,
-    exact is_right_cancel_mul.mul_right_cancel _ _ _ h
-  end,
-  mul_right_cancel := is_right_cancel_mul.mul_right_cancel }
+{ .. ‹is_right_cancel_mul G›, .. comm_semigroup.is_right_cancel_mul.to_is_left_cancel_mul G }
 
 end comm_semigroup
 
@@ -243,37 +276,12 @@ class add_left_cancel_semigroup (G : Type u) extends add_semigroup G :=
 (add_left_cancel : ∀ a b c : G, a + b = a + c → b = c)
 attribute [to_additive add_left_cancel_semigroup] left_cancel_semigroup
 
-section left_cancel_semigroup
-variables [left_cancel_semigroup G] {a b c : G}
-
-@[to_additive]
-lemma mul_left_cancel : a * b = a * c → b = c :=
-left_cancel_semigroup.mul_left_cancel a b c
-
-@[to_additive]
-lemma mul_left_cancel_iff : a * b = a * c ↔ b = c :=
-⟨mul_left_cancel, congr_arg _⟩
-
-@[to_additive]
-theorem mul_right_injective (a : G) : function.injective ((*) a) :=
-λ b c, mul_left_cancel
-
-@[simp, to_additive]
-theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
-(mul_right_injective a).eq_iff
-
-@[to_additive]
-theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
-(mul_right_injective a).ne_iff
-
 /-- Any `left_cancel_semigroup` satisfies `is_left_cancel_mul`. -/
 @[priority 100, to_additive "Any `add_left_cancel_semigroup` satisfies `is_left_cancel_add`."]
 instance left_cancel_semigroup.to_is_left_cancel_mul (G : Type u) [left_cancel_semigroup G] :
   is_left_cancel_mul G :=
 { mul_left_cancel := left_cancel_semigroup.mul_left_cancel }
 
-end left_cancel_semigroup
-
 /-- A `right_cancel_semigroup` is a semigroup such that `a * b = c * b` implies `a = c`. -/
 @[protect_proj, ancestor semigroup, ext]
 class right_cancel_semigroup (G : Type u) extends semigroup G :=
@@ -286,37 +294,12 @@ class add_right_cancel_semigroup (G : Type u) extends add_semigroup G :=
 (add_right_cancel : ∀ a b c : G, a + b = c + b → a = c)
 attribute [to_additive add_right_cancel_semigroup] right_cancel_semigroup
 
-section right_cancel_semigroup
-variables [right_cancel_semigroup G] {a b c : G}
-
-@[to_additive]
-lemma mul_right_cancel : a * b = c * b → a = c :=
-right_cancel_semigroup.mul_right_cancel a b c
-
-@[to_additive]
-lemma mul_right_cancel_iff : b * a = c * a ↔ b = c :=
-⟨mul_right_cancel, congr_arg _⟩
-
-@[to_additive]
-theorem mul_left_injective (a : G) : function.injective (λ x, x * a) :=
-λ b c, mul_right_cancel
-
-@[simp, to_additive]
-theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
-(mul_left_injective a).eq_iff
-
-@[to_additive]
-theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c :=
-(mul_left_injective a).ne_iff
-
 /-- Any `right_cancel_semigroup` satisfies `is_right_cancel_mul`. -/
 @[priority 100, to_additive "Any `add_right_cancel_semigroup` satisfies `is_right_cancel_add`."]
-instance right_cancel_semigroup.to_is_right_cancel_mul (G : Type u)
-  [right_cancel_semigroup G] : is_right_cancel_mul G :=
+instance right_cancel_semigroup.to_is_right_cancel_mul (G : Type u) [right_cancel_semigroup G] :
+  is_right_cancel_mul G :=
 { mul_right_cancel := right_cancel_semigroup.mul_right_cancel }
 
-end right_cancel_semigroup
-
 /-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
 `1 * a = a` and `a * 1 = a` for all `a : M`. -/
 @[ancestor has_one has_mul]
@@ -362,8 +345,6 @@ instance mul_one_class.to_is_right_id : is_right_id M (*) 1 :=
 
 end mul_one_class
 
-
-
 section
 variables {M : Type u}
 
@@ -580,8 +561,7 @@ class cancel_comm_monoid (M : Type u) extends left_cancel_monoid M, comm_monoid
 @[priority 100, to_additive] -- see Note [lower instance priority]
 instance cancel_comm_monoid.to_cancel_monoid (M : Type u) [cancel_comm_monoid M] :
   cancel_monoid M :=
-{ mul_right_cancel := λ a b c h, mul_left_cancel $ by rw [mul_comm, h, mul_comm],
-  .. ‹cancel_comm_monoid M› }
+{ .. ‹cancel_comm_monoid M›, .. comm_semigroup.is_left_cancel_mul.to_is_right_cancel_mul M }
 
 /-- Any `cancel_monoid M` satisfies `is_cancel_mul M`. -/
 @[priority 100, to_additive "Any `add_cancel_monoid M` satisfies `is_cancel_add M`."]
diff --git a/src/algebra/group/type_tags.lean b/src/algebra/group/type_tags.lean
@@ -124,21 +124,35 @@ instance [add_comm_semigroup α] : comm_semigroup (multiplicative α) :=
 { mul_comm := @add_comm _ _,
   ..multiplicative.semigroup }
 
+instance [has_mul α] [is_left_cancel_mul α] : is_left_cancel_add (additive α) :=
+{ add_left_cancel := @mul_left_cancel α _ _ }
+
+instance [has_add α] [is_left_cancel_add α] : is_left_cancel_mul (multiplicative α) :=
+{ mul_left_cancel := @add_left_cancel α _ _ }
+
+instance [has_mul α] [is_right_cancel_mul α] : is_right_cancel_add (additive α) :=
+{ add_right_cancel := @mul_right_cancel α _ _ }
+
+instance [has_add α] [is_right_cancel_add α] : is_right_cancel_mul (multiplicative α) :=
+{ mul_right_cancel := @add_right_cancel α _ _ }
+
+instance [has_mul α] [is_cancel_mul α] : is_cancel_add (additive α) :=
+{ ..additive.is_left_cancel_add, ..additive.is_right_cancel_add }
+
+instance [has_add α] [is_cancel_add α] : is_cancel_mul (multiplicative α) :=
+{ ..multiplicative.is_left_cancel_mul, ..multiplicative.is_right_cancel_mul }
+
 instance [left_cancel_semigroup α] : add_left_cancel_semigroup (additive α) :=
-{ add_left_cancel := @mul_left_cancel _ _,
-  ..additive.add_semigroup }
+{ ..additive.add_semigroup, ..additive.is_left_cancel_add }
 
 instance [add_left_cancel_semigroup α] : left_cancel_semigroup (multiplicative α) :=
-{ mul_left_cancel := @add_left_cancel _ _,
-  ..multiplicative.semigroup }
+{ ..multiplicative.semigroup, ..multiplicative.is_left_cancel_mul }
 
 instance [right_cancel_semigroup α] : add_right_cancel_semigroup (additive α) :=
-{ add_right_cancel := @mul_right_cancel _ _,
-  ..additive.add_semigroup }
+{ ..additive.add_semigroup, ..additive.is_right_cancel_add }
 
 instance [add_right_cancel_semigroup α] : right_cancel_semigroup (multiplicative α) :=
-{ mul_right_cancel := @add_right_cancel _ _,
-  ..multiplicative.semigroup }
+{ ..multiplicative.semigroup, ..multiplicative.is_right_cancel_mul }
 
 instance [has_one α] : has_zero (additive α) := ⟨additive.of_mul 1⟩
 
diff --git a/src/data/nat/modeq.lean b/src/data/nat/modeq.lean
@@ -323,9 +323,9 @@ end
 
 lemma div_mod_eq_mod_mul_div (a b c : ℕ) : a / b % c = a % (b * c) / b :=
 if hb0 : b = 0 then by simp [hb0]
-else by rw [← @add_right_cancel_iff _ _ (c * (a / b / c)), mod_add_div, nat.div_div_eq_div_mul,
-  ← mul_right_inj' hb0, ← @add_left_cancel_iff _ _ (a % b), mod_add_div,
-  mul_add, ← @add_left_cancel_iff _ _ (a % (b * c) % b), add_left_comm,
+else by rw [← @add_right_cancel_iff _ _ _ (c * (a / b / c)), mod_add_div, nat.div_div_eq_div_mul,
+  ← mul_right_inj' hb0, ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div,
+  mul_add, ← @add_left_cancel_iff _ _ _ (a % (b * c) % b), add_left_comm,
   ← add_assoc (a % (b * c) % b), mod_add_div, ← mul_assoc, mod_add_div, mod_mul_right_mod]
 
 lemma add_mod_add_ite (a b c : ℕ) :
@@ -342,7 +342,7 @@ else
           exact add_lt_add (nat.mod_lt _ (nat.pos_of_ne_zero hc0))
             (nat.mod_lt _ (nat.pos_of_ne_zero hc0))),
       have h0 : 0 <  (a % c + b % c) / c, from nat.div_pos h (nat.pos_of_ne_zero hc0),
-      rw [← @add_right_cancel_iff _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
+      rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
         mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm] },
     { rw [nat.mod_eq_of_lt (lt_of_not_ge h), add_zero] }
   end
@@ -358,7 +358,7 @@ by rw [← add_mod_add_ite, if_pos hc]
 lemma add_div {a b c : ℕ} (hc0 : 0 < c) : (a + b) / c = a / c + b / c +
   if c ≤ a % c + b % c then 1 else 0 :=
 begin
-  rw [← mul_right_inj' hc0.ne', ← @add_left_cancel_iff _ _ ((a + b) % c + a % c + b % c)],
+  rw [← mul_right_inj' hc0.ne', ← @add_left_cancel_iff _ _ _ ((a + b) % c + a % c + b % c)],
   suffices : (a + b) % c + c * ((a + b) / c) + a % c + b % c =
     a % c + c * (a / c) + (b % c + c * (b / c)) + c * (if c ≤ a % c + b % c then 1 else 0) +
       (a + b) % c,
diff --git a/src/data/nat/order/lemmas.lean b/src/data/nat/order/lemmas.lean
@@ -61,7 +61,7 @@ end
 
 protected lemma div_eq_zero_iff {a b : ℕ} (hb : 0 < b) : a / b = 0 ↔ a < b :=
 ⟨λ h, by rw [← mod_add_div a b, h, mul_zero, add_zero]; exact mod_lt _ hb,
-  λ h, by rw [← mul_right_inj' hb.ne', ← @add_left_cancel_iff _ _ (a % b), mod_add_div,
+  λ h, by rw [← mul_right_inj' hb.ne', ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div,
     mod_eq_of_lt h, mul_zero, add_zero]⟩
 
 protected lemma div_eq_zero {a b : ℕ} (hb : a < b) : a / b = 0 :=
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
@@ -850,7 +850,7 @@ noncomputable def linear_equiv.quot_equiv_of_equiv
   (f₁ : p ≃ₗ[K] q) (f₂ : V ≃ₗ[K] V₂) : (V ⧸ p) ≃ₗ[K] (V₂ ⧸ q) :=
 linear_equiv.of_finrank_eq _ _
 begin
-  rw [← @add_right_cancel_iff _ _ (finrank K p), submodule.finrank_quotient_add_finrank,
+  rw [← @add_right_cancel_iff _ _ _ (finrank K p), submodule.finrank_quotient_add_finrank,
       linear_equiv.finrank_eq f₁, submodule.finrank_quotient_add_finrank,
       linear_equiv.finrank_eq f₂],
 end
diff --git a/src/set_theory/game/impartial.lean b/src/set_theory/game/impartial.lean
@@ -143,11 +143,11 @@ lemma add_self : G + G ≈ 0 :=
 
 /-- This lemma doesn't require `H` to be impartial. -/
 lemma equiv_iff_add_equiv_zero (H : pgame) : H ≈ G ↔ H + G ≈ 0 :=
-by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_right_cancel_iff _ _ (-⟦G⟧)], simpa }
+by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_right_cancel_iff _ _ _ (-⟦G⟧)], simpa }
 
 /-- This lemma doesn't require `H` to be impartial. -/
 lemma equiv_iff_add_equiv_zero' (H : pgame) : G ≈ H ↔ G + H ≈ 0 :=
-by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_left_cancel_iff _ _ (-⟦G⟧), eq_comm], simpa }
+by { rw [equiv_iff_game_eq, equiv_iff_game_eq, ←@add_left_cancel_iff _ _ _ (-⟦G⟧), eq_comm], simpa }
 
 lemma le_zero_iff {G : pgame} [G.impartial] : G ≤ 0 ↔ 0 ≤ G :=
 by rw [←zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
diff --git a/src/set_theory/ordinal/natural_ops.lean b/src/set_theory/ordinal/natural_ops.lean
@@ -312,12 +312,12 @@ theorem nadd_le_nadd_iff_right : ∀ a {b c}, b ♯ a ≤ c ♯ a ↔ b ≤ c :=
 @_root_.add_le_add_iff_right nat_ordinal _ _ _ _
 
 theorem nadd_left_cancel : ∀ {a b c}, a ♯ b = a ♯ c → b = c :=
-@_root_.add_left_cancel nat_ordinal _
+@_root_.add_left_cancel nat_ordinal _ _
 theorem nadd_right_cancel : ∀ {a b c}, a ♯ b = c ♯ b → a = c :=
-@_root_.add_right_cancel nat_ordinal _
+@_root_.add_right_cancel nat_ordinal _ _
 theorem nadd_left_cancel_iff : ∀ {a b c}, a ♯ b = a ♯ c ↔ b = c :=
-@add_left_cancel_iff nat_ordinal _
+@add_left_cancel_iff nat_ordinal _ _
 theorem nadd_right_cancel_iff : ∀ {a b c}, b ♯ a = c ♯ a ↔ b = c :=
-@add_right_cancel_iff nat_ordinal _
+@add_right_cancel_iff nat_ordinal _ _
 
 end ordinal
