feat(algebra/group/defs): ext lemmas for (semi)groups and monoids (#8391)

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236476.20boolean_algebra.2Eto_boolean_ring/near/242118386)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Author: bryangingechen

src/algebra/group/defs.lean

@@ -7,7 +7,7 @@ import algebra.group.to_additive
 import tactic.basic
 
 /-!
-# Typeclasses for (semi)groups and monoid
+# Typeclasses for (semi)groups and monoids
 
 In this file we define typeclasses for algebraic structures with one binary operation.
 The classes are named `(add_)?(comm_)?(semigroup|monoid|group)`, where `add_` means that
@@ -62,10 +62,10 @@ def right_mul : G → G → G := λ g : G, λ x : G, x * g
 end has_mul
 
 /-- A semigroup is a type with an associative `(*)`. -/
-@[protect_proj, ancestor has_mul] class semigroup (G : Type u) extends has_mul G :=
+@[protect_proj, ancestor has_mul, ext] class semigroup (G : Type u) extends has_mul G :=
 (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
 /-- An additive semigroup is a type with an associative `(+)`. -/
-@[protect_proj, ancestor has_add] class add_semigroup (G : Type u) extends has_add G :=
+@[protect_proj, ancestor has_add, ext] class add_semigroup (G : Type u) extends has_add G :=
 (add_assoc : ∀ a b c : G, a + b + c = a + (b + c))
 attribute [to_additive] semigroup
 
@@ -85,12 +85,12 @@ instance semigroup.to_is_associative : is_associative G (*) :=
 end semigroup
 
 /-- A commutative semigroup is a type with an associative commutative `(*)`. -/
-@[protect_proj, ancestor semigroup]
+@[protect_proj, ancestor semigroup, ext]
 class comm_semigroup (G : Type u) extends semigroup G :=
 (mul_comm : ∀ a b : G, a * b = b * a)
 
 /-- A commutative additive semigroup is a type with an associative commutative `(+)`. -/
-@[protect_proj, ancestor add_semigroup]
+@[protect_proj, ancestor add_semigroup, ext]
 class add_comm_semigroup (G : Type u) extends add_semigroup G :=
 (add_comm : ∀ a b : G, a + b = b + a)
 attribute [to_additive] comm_semigroup
@@ -110,12 +110,12 @@ instance comm_semigroup.to_is_commutative : is_commutative G (*) :=
 end comm_semigroup
 
 /-- A `left_cancel_semigroup` is a semigroup such that `a * b = a * c` implies `b = c`. -/
-@[protect_proj, ancestor semigroup]
+@[protect_proj, ancestor semigroup, ext]
 class left_cancel_semigroup (G : Type u) extends semigroup G :=
 (mul_left_cancel : ∀ a b c : G, a * b = a * c → b = c)
 /-- An `add_left_cancel_semigroup` is an additive semigroup such that
 `a + b = a + c` implies `b = c`. -/
-@[protect_proj, ancestor add_semigroup]
+@[protect_proj, ancestor add_semigroup, ext]
 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
@@ -146,13 +146,13 @@ theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c :=
 end left_cancel_semigroup
 
 /-- A `right_cancel_semigroup` is a semigroup such that `a * b = c * b` implies `a = c`. -/
-@[protect_proj, ancestor semigroup]
+@[protect_proj, ancestor semigroup, ext]
 class right_cancel_semigroup (G : Type u) extends semigroup G :=
 (mul_right_cancel : ∀ a b c : G, a * b = c * b → a = c)
 
 /-- An `add_right_cancel_semigroup` is an additive semigroup such that
 `a + b = c + b` implies `a = c`. -/
-@[protect_proj, ancestor add_semigroup]
+@[protect_proj, ancestor add_semigroup, ext]
 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
@@ -198,6 +198,16 @@ class add_zero_class (M : Type u) extends has_zero M, has_add M :=
 
 attribute [to_additive] mul_one_class
 
+@[ext, to_additive]
+lemma mul_one_class.ext {M : Type u} : ∀ ⦃m₁ m₂ : mul_one_class M⦄, m₁.mul = m₂.mul → m₁ = m₂ :=
+begin
+  rintros ⟨one₁, mul₁, one_mul₁, mul_one₁⟩ ⟨one₂, mul₂, one_mul₂, mul_one₂⟩ (rfl : mul₁ = mul₂),
+  congr,
+  exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂),
+end
+
+attribute [ext] add_zero_class.ext
+
 section mul_one_class
 variables {M : Type u} [mul_one_class M]
 
@@ -352,6 +362,28 @@ class monoid (M : Type u) extends semigroup M, mul_one_class M :=
 
 export monoid (npow)
 
+@[ext, to_additive]
+lemma monoid.ext {M : Type*} ⦃m₁ m₂ : monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+begin
+  unfreezingI {
+    cases m₁ with mul₁ _ one₁ one_mul₁ mul_one₁ npow₁ npow_zero₁ npow_succ₁,
+    cases m₂ with mul₂ _ one₂ one_mul₂ mul_one₂ npow₂ npow_zero₂ npow_succ₂ },
+  change mul₁ = mul₂ at h_mul,
+  subst h_mul,
+  have h_one : one₁ = one₂,
+  { rw ←one_mul₂ one₁,
+    exact mul_one₁ one₂ },
+  subst h_one,
+  have h_npow : npow₁ = npow₂,
+  { ext n,
+    induction n with d hd,
+    { rw [npow_zero₁, npow_zero₂] },
+    { rw [npow_succ₁, npow_succ₂, hd] } },
+  subst h_npow,
+end
+
+attribute [ext] add_monoid.ext
+
 section monoid
 variables {M : Type u} [monoid M]
 
@@ -388,6 +420,20 @@ class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
 @[protect_proj, ancestor monoid comm_semigroup, to_additive]
 class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
 
+@[to_additive]
+lemma comm_monoid.to_monoid_injective {M : Type u} :
+  function.injective (@comm_monoid.to_monoid M) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  congr'; injection h,
+end
+
+@[ext, to_additive]
+lemma comm_monoid.ext {M : Type*} ⦃m₁ m₂ : comm_monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+comm_monoid.to_monoid_injective $ monoid.ext h_mul
+
+attribute [ext] add_comm_monoid.ext
+
 section left_cancel_monoid
 
 /-- An additive monoid in which addition is left-cancellative.
@@ -400,6 +446,21 @@ class add_left_cancel_monoid (M : Type u) extends add_left_cancel_semigroup M, a
 @[protect_proj, ancestor left_cancel_semigroup monoid, to_additive add_left_cancel_monoid]
 class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M
 
+@[to_additive]
+lemma left_cancel_monoid.to_monoid_injective {M : Type u} :
+  function.injective (@left_cancel_monoid.to_monoid M) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  congr'; injection h,
+end
+
+@[ext, to_additive]
+lemma left_cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : left_cancel_monoid M⦄
+  (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+left_cancel_monoid.to_monoid_injective $ monoid.ext h_mul
+
+attribute [ext] add_left_cancel_monoid.ext
+
 end left_cancel_monoid
 
 section right_cancel_monoid
@@ -414,6 +475,21 @@ class add_right_cancel_monoid (M : Type u) extends add_right_cancel_semigroup M,
 @[protect_proj, ancestor right_cancel_semigroup monoid, to_additive add_right_cancel_monoid]
 class right_cancel_monoid (M : Type u) extends right_cancel_semigroup M, monoid M
 
+@[to_additive]
+lemma right_cancel_monoid.to_monoid_injective {M : Type u} :
+  function.injective (@right_cancel_monoid.to_monoid M) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  congr'; injection h,
+end
+
+@[ext, to_additive]
+lemma right_cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : right_cancel_monoid M⦄
+  (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+right_cancel_monoid.to_monoid_injective $ monoid.ext h_mul
+
+attribute [ext] add_right_cancel_monoid.ext
+
 end right_cancel_monoid
 
 section cancel_monoid
@@ -429,6 +505,21 @@ class add_cancel_monoid (M : Type u)
 @[protect_proj, ancestor left_cancel_monoid right_cancel_monoid, to_additive add_cancel_monoid]
 class cancel_monoid (M : Type u) extends left_cancel_monoid M, right_cancel_monoid M
 
+@[to_additive]
+lemma cancel_monoid.to_left_cancel_monoid_injective {M : Type u} :
+  function.injective (@cancel_monoid.to_left_cancel_monoid M) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  congr'; injection h,
+end
+
+@[ext, to_additive]
+lemma cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : cancel_monoid M⦄
+  (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+cancel_monoid.to_left_cancel_monoid_injective $ left_cancel_monoid.ext h_mul
+
+attribute [ext] add_cancel_monoid.ext
+
 /-- Commutative version of add_cancel_monoid. -/
 @[protect_proj, ancestor add_left_cancel_monoid add_comm_monoid]
 class add_cancel_comm_monoid (M : Type u) extends add_left_cancel_monoid M, add_comm_monoid M
@@ -437,6 +528,21 @@ class add_cancel_comm_monoid (M : Type u) extends add_left_cancel_monoid M, add_
 @[protect_proj, ancestor left_cancel_monoid comm_monoid, to_additive add_cancel_comm_monoid]
 class cancel_comm_monoid (M : Type u) extends left_cancel_monoid M, comm_monoid M
 
+@[to_additive]
+lemma cancel_comm_monoid.to_comm_monoid_injective {M : Type u} :
+  function.injective (@cancel_comm_monoid.to_comm_monoid M) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  congr'; injection h,
+end
+
+@[ext, to_additive]
+lemma cancel_comm_monoid.ext {M : Type*} ⦃m₁ m₂ : cancel_comm_monoid M⦄
+  (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+cancel_comm_monoid.to_comm_monoid_injective $ comm_monoid.ext h_mul
+
+attribute [ext] add_cancel_comm_monoid.ext
+
 @[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 :=
@@ -485,9 +591,9 @@ class div_inv_monoid (G : Type u) extends monoid G, has_inv G, has_div G :=
 (gpow : ℤ → G → G := gpow_rec)
 (gpow_zero' : ∀ (a : G), gpow 0 a = 1 . try_refl_tac)
 (gpow_succ' :
-  ∀ (n : ℕ) (a : G), gpow (int.of_nat n.succ) a = a * gpow (int.of_nat n) a  . try_refl_tac)
+  ∀ (n : ℕ) (a : G), gpow (int.of_nat n.succ) a = a * gpow (int.of_nat n) a . try_refl_tac)
 (gpow_neg' :
-  ∀ (n : ℕ) (a : G), gpow (-[1+ n]) a = (gpow n.succ a) ⁻¹ . try_refl_tac)
+  ∀ (n : ℕ) (a : G), gpow (-[1+ n]) a = (gpow n.succ a)⁻¹ . try_refl_tac)
 
 export div_inv_monoid (gpow)
 
@@ -515,14 +621,63 @@ class sub_neg_monoid (G : Type u) extends add_monoid G, has_neg G, has_sub G :=
 (gsmul : ℤ → G → G := gsmul_rec)
 (gsmul_zero' : ∀ (a : G), gsmul 0 a = 0 . try_refl_tac)
 (gsmul_succ' :
-  ∀ (n : ℕ) (a : G), gsmul (int.of_nat n.succ) a = a + gsmul (int.of_nat n) a  . try_refl_tac)
+  ∀ (n : ℕ) (a : G), gsmul (int.of_nat n.succ) a = a + gsmul (int.of_nat n) a . try_refl_tac)
 (gsmul_neg' :
   ∀ (n : ℕ) (a : G), gsmul (-[1+ n]) a = - (gsmul n.succ a) . try_refl_tac)
 
 export sub_neg_monoid (gsmul)
 
 attribute [to_additive sub_neg_monoid] div_inv_monoid
 
+@[ext, to_additive]
+lemma div_inv_monoid.ext {M : Type*} ⦃m₁ m₂ : div_inv_monoid M⦄ (h_mul : m₁.mul = m₂.mul)
+  (h_inv : m₁.inv = m₂.inv) : m₁ = m₂ :=
+begin
+  let iM : div_inv_monoid M := m₁,
+  unfreezingI {
+    cases m₁ with mul₁ _ one₁ one_mul₁ mul_one₁ npow₁ npow_zero₁ npow_succ₁ inv₁ div₁
+      div_eq_mul_inv₁ gpow₁ gpow_zero'₁ gpow_succ'₁ gpow_neg'₁,
+    cases m₂ with mul₂ _ one₂ one_mul₂ mul_one₂ npow₂ npow_zero₂ npow_succ₂ inv₂ div₂
+      div_eq_mul_inv₂ gpow₂ gpow_zero'₂ gpow_succ'₂ gpow_neg'₂ },
+  change mul₁ = mul₂ at h_mul,
+  subst h_mul,
+  have h_one : one₁ = one₂,
+  { rw ←one_mul₂ one₁,
+    exact mul_one₁ one₂ },
+  subst h_one,
+  have h_npow : npow₁ = npow₂,
+  { ext n,
+    induction n with d hd,
+    { rw [npow_zero₁, npow_zero₂] },
+    { rw [npow_succ₁, npow_succ₂, hd] } },
+  subst h_npow,
+  change inv₁ = inv₂ at h_inv,
+  subst h_inv,
+  have h_div : div₁ = div₂,
+  { ext a b,
+    convert (rfl : a * b⁻¹ = a * b⁻¹),
+    { exact div_eq_mul_inv₁ a b },
+    { exact div_eq_mul_inv₂ a b } },
+  subst h_div,
+  have h_gpow_aux : ∀ n g, gpow₁ (int.of_nat n) g = gpow₂ (int.of_nat n) g,
+  { intros n g,
+    induction n with n IH,
+    { convert (rfl : (1 : M) = 1),
+      { exact gpow_zero'₁ g },
+      { exact gpow_zero'₂ g } },
+    { rw [gpow_succ'₁, gpow_succ'₂, IH] } },
+  have h_gpow : gpow₁ = gpow₂,
+  { ext z,
+    cases z with z z,
+    { exact h_gpow_aux z x },
+    { rw [gpow_neg'₁, gpow_neg'₂],
+      congr',
+      exact h_gpow_aux _ _ } },
+  subst h_gpow,
+end
+
+attribute [ext] sub_neg_monoid.ext
+
 @[to_additive]
 lemma div_eq_mul_inv {G : Type u} [div_inv_monoid G] :
   ∀ a b : G, a / b = a * b⁻¹ :=
@@ -602,6 +757,45 @@ instance group.to_cancel_monoid : cancel_monoid G :=
 
 end group
 
+@[to_additive]
+lemma group.to_div_inv_monoid_injective {G : Type*} :
+  function.injective (@group.to_div_inv_monoid G) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  replace h := div_inv_monoid.mk.inj h,
+  dsimp at h,
+  rcases h with ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩,
+  refl
+end
+
+@[ext, to_additive]
+lemma group.ext {G : Type*} ⦃g₁ g₂ : group G⦄ (h_mul : g₁.mul = g₂.mul) : g₁ = g₂ :=
+group.to_div_inv_monoid_injective $ div_inv_monoid.ext h_mul
+begin
+  let iG : group G := g₁,
+  unfreezingI {
+    cases g₁ with mul₁ _ one₁ one_mul₁ mul_one₁ npow₁ npow_zero'₁ npow_succ'₁ inv₁ div₁
+      div_eq_mul_inv₁ gpow₁ gpow_zero'₁ gpow_succ'₁ gpow_neg'₁ mul_left_inv₁,
+    cases g₂ with mul₂ _ one₂ one_mul₂ mul_one₂ npow₂ npow_zero'₂ npow_succ'₂ inv₂ div₂
+      div_eq_mul_inv₂ gpow₂ gpow_zero'₂ gpow_succ'₂ gpow_neg'₂ mul_left_inv₂, },
+  change mul₁ = mul₂ at h_mul,
+  subst h_mul,
+  have h_one : one₁ = one₂,
+  { rw ← mul_one₂ one₁,
+    exact one_mul₁ one₂ },
+  subst h_one,
+  have h_inv : inv₁ = inv₂,
+  { ext a,
+    -- this uses the group.to_cancel_monoid instance, so this lemma can't be moved higher
+    rw [← mul_left_inj a],
+    convert (rfl : (1 : G) = 1),
+    { exact mul_left_inv₁ a },
+    { exact mul_left_inv₂ a } },
+  exact h_inv
+end
+
+attribute [ext] add_group.ext
+
 /-- A commutative group is a group with commutative `(*)`. -/
 @[protect_proj, ancestor group comm_monoid]
 class comm_group (G : Type u) extends group G, comm_monoid G
@@ -611,6 +805,24 @@ class add_comm_group (G : Type u) extends add_group G, add_comm_monoid G
 attribute [to_additive] comm_group
 attribute [instance, priority 300] add_comm_group.to_add_comm_monoid
 
+@[to_additive]
+lemma comm_group.to_group_injective {G : Type u} :
+  function.injective (@comm_group.to_group G) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  replace h := group.mk.inj h,
+  dsimp at h,
+  rcases h with ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩,
+  refl
+end
+
+@[ext, to_additive]
+lemma comm_group.ext {G : Type*} ⦃g₁ g₂ : comm_group G⦄
+  (h_mul : g₁.mul = g₂.mul) : g₁ = g₂ :=
+comm_group.to_group_injective $ group.ext h_mul
+
+attribute [ext] add_comm_group.ext
+
 section comm_group
 
 variables {G : Type u} [comm_group G]

src/category_theory/preadditive/schur.lean

@@ -87,7 +87,7 @@ variables [is_alg_closed 𝕜] [linear 𝕜 C]
 -- To get around this, we use `convert I`,
 -- then check the various instances agree field-by-field,
 -- using `ext` equipped with the following extra lemmas:
-local attribute [ext] add_comm_group module distrib_mul_action mul_action has_scalar
+local attribute [ext] module distrib_mul_action mul_action has_scalar
 
 /--
 An auxiliary lemma for Schur's lemma.
@@ -109,7 +109,7 @@ begin
   { intro f,
     haveI : nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero,
     obtain ⟨c, nu⟩ := @exists_spectrum_of_is_alg_closed_of_finite_dimensional 𝕜 _ _ (End X) _ _ _
-      (by { convert I, ext; refl, ext; refl, }) (End.of f),
+      (by { convert I, ext, refl, ext, refl, }) (End.of f),
     use c,
     rw [is_unit_iff_is_iso, is_iso_iff_nonzero, ne.def, not_not, sub_eq_zero,
       algebra.algebra_map_eq_smul_one] at nu,

test/equiv_rw.lean

@@ -254,8 +254,6 @@ begin
 end :=
 rfl
 
-attribute [ext] semigroup
-
 lemma semigroup.id_map (α : Type) : semigroup.map (equiv.refl α) = id :=
 by { ext, refl, }