From 4ed70f0af9ce161ae8168988a85b8ead2413394e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 19 Apr 2023 15:41:33 +0000
Subject: [PATCH 1/2] feat(algebra/*): morphisms from closures are equal if
 they agree on generators

---
 src/algebra/star/subalgebra.lean              | 21 +++++++++++++++++++
 src/group_theory/subgroup/basic.lean          | 21 +++++++++++++++++++
 src/group_theory/submonoid/operations.lean    | 19 +++++++++++++++++
 src/group_theory/subsemigroup/basic.lean      |  2 +-
 src/group_theory/subsemigroup/operations.lean | 18 ++++++++++++++++
 src/linear_algebra/span.lean                  | 17 +++++++++++++++
 src/ring_theory/adjoin/basic.lean             | 18 ++++++++++++++++
 7 files changed, 115 insertions(+), 1 deletion(-)

diff --git a/src/algebra/star/subalgebra.lean b/src/algebra/star/subalgebra.lean
index 7356d1122fe09..3a5ae3cebd569 100644
--- a/src/algebra/star/subalgebra.lean
+++ b/src/algebra/star/subalgebra.lean
@@ -394,6 +394,7 @@ le_antisymm (subalgebra.star_closure_le_iff.2 $ subset_adjoin R (S : set A))
 
 /-- If some predicate holds for all `x ∈ (s : set A)` and this predicate is closed under the
 `algebra_map`, addition, multiplication and star operations, then it holds for `a ∈ adjoin R s`. -/
+@[elab_as_eliminator]
 lemma adjoin_induction {s : set A} {p : A → Prop} {a : A} (h : a ∈ adjoin R s)
   (Hs : ∀ (x : A), x ∈ s → p x) (Halg : ∀ (r : R), p (algebra_map R A r))
   (Hadd : ∀ (x y : A), p x → p y → p (x + y)) (Hmul : ∀ (x y : A), p x → p y → p (x * y))
@@ -401,6 +402,7 @@ lemma adjoin_induction {s : set A} {p : A → Prop} {a : A} (h : a ∈ adjoin R
 algebra.adjoin_induction h (λ x hx, hx.elim (λ hx, Hs x hx) (λ hx, star_star x ▸ Hstar _ (Hs _ hx)))
   Halg Hadd Hmul
 
+@[elab_as_eliminator]
 lemma adjoin_induction₂ {s : set A} {p : A → A → Prop} {a b : A} (ha : a ∈ adjoin R s)
   (hb : b ∈ adjoin R s) (Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y)
   (Halg : ∀ (r₁ r₂ : R), p (algebra_map R A r₁) (algebra_map R A r₂))
@@ -425,6 +427,7 @@ begin
 end
 
 /-- The difference with `star_subalgebra.adjoin_induction` is that this acts on the subtype. -/
+@[elab_as_eliminator]
 lemma adjoin_induction' {s : set A} {p : adjoin R s → Prop} (a : adjoin R s)
   (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_adjoin R s h⟩)
   (Halg : ∀ r, p (algebra_map R _ r)) (Hadd : ∀ x y, p x → p y → p (x + y))
@@ -442,6 +445,24 @@ begin
     λ x hx, exists.elim hx (λ hx' hx, ⟨star_mem hx', Hstar _ hx⟩)]
 end
 
+/-- Two algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext] lemma _root_.star_alg_hom.adjoin_ext {s : set A} ⦃f g : adjoin R s →⋆ₐ[R] B⦄
+  (h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g :=
+begin
+  ext x,
+  refine adjoin_induction' x _ _ _ _ _,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intro r,
+    exact (alg_hom_class.commutes f _).trans (alg_hom_class.commutes g _).symm },
+  { intros x y hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros x y hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 variables (R)
 
 /-- If all elements of `s : set A` commute pairwise and also commute pairwise with elements of
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index b18053c47065b..df57a7f518fe4 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -787,6 +787,27 @@ begin
     (λ x ⟨hx', hx⟩, ⟨_, Hinv _ _ hx⟩),
 end
 
+/-- Two group morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive group morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.monoid_hom.closure_ext {s : set G} ⦃f g : closure s →* G'⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_one.trans g.map_one.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+  { intros x hx hfg,
+    exact (map_inv f _).trans ((congr_arg (has_inv.inv) hfg).trans (map_inv g _).symm) },
+end
+
 /-- An induction principle for closure membership for predicates with two arguments. -/
 @[elab_as_eliminator, to_additive "An induction principle for additive closure membership, for
 predicates with two arguments."]
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
index 6226d6e25dc76..294cc58edc591 100644
--- a/src/group_theory/submonoid/operations.lean
+++ b/src/group_theory/submonoid/operations.lean
@@ -617,6 +617,25 @@ noncomputable def equiv_map_of_injective
   (f : M →* N) (hf : function.injective f) (x : S) :
   (equiv_map_of_injective S f hf x : N) = f x := rfl
 
+/-- Two monoid morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive monoid morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.monoid_hom.mclosure_ext {s : set M} ⦃f g : closure s →* N⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_one.trans g.map_one.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp, to_additive]
 lemma closure_closure_coe_preimage {s : set M} : closure ((coe : closure s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
diff --git a/src/group_theory/subsemigroup/basic.lean b/src/group_theory/subsemigroup/basic.lean
index a380ec63b600b..69605c9dac637 100644
--- a/src/group_theory/subsemigroup/basic.lean
+++ b/src/group_theory/subsemigroup/basic.lean
@@ -53,7 +53,7 @@ variables {M : Type*} {N : Type*}
 variables {A : Type*}
 
 section non_assoc
-variables [has_mul M] {s : set M}
+variables [has_mul M] [has_mul N] {s : set M}
 variables [has_add A] {t : set A}
 
 /-- `mul_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(*)` -/
diff --git a/src/group_theory/subsemigroup/operations.lean b/src/group_theory/subsemigroup/operations.lean
index 3046644562618..f7c06f46983d0 100644
--- a/src/group_theory/subsemigroup/operations.lean
+++ b/src/group_theory/subsemigroup/operations.lean
@@ -462,6 +462,24 @@ noncomputable def equiv_map_of_injective
   (f : M →ₙ* N) (hf : function.injective f) (x : S) :
   (equiv_map_of_injective S f hf x : N) = f x := rfl
 
+/-- Two semigroup morphisms from a closure are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext, to_additive "Two additive semigroup morphisms from a closure are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]"]
+lemma _root_.mul_hom.closure_ext {s : set M} ⦃f g : closure s →ₙ* N⦄
+  (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine closure_induction' _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp, to_additive]
 lemma closure_closure_coe_preimage {s : set M} : closure ((coe : closure s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean
index 54c850ab6fabd..4f50e29441f41 100644
--- a/src/linear_algebra/span.lean
+++ b/src/linear_algebra/span.lean
@@ -138,6 +138,23 @@ begin
     ⟨smul_mem _ _ hx', H2 r _ _ hx⟩)
 end
 
+/-- Two linear maps from a span are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext] lemma _root_.linear_map.span_ext {s : set M} ⦃f g : span R s →ₛₗ[σ₁₂] M₂⦄
+  (h : f ∘ set.inclusion subset_span = g ∘ set.inclusion subset_span) : f = g :=
+begin
+  ext ⟨x, hx⟩,
+  refine span_induction' _ _ _ _ hx,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { exact f.map_zero.trans g.map_zero.symm },
+  { intros x hx y hy hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros a x hx hfg,
+    exact (map_smulₛₗ f _ _).trans ((congr_arg ((•) (σ₁₂ a)) hfg).trans (map_smulₛₗ g _ _).symm) },
+end
+
 @[simp] lemma span_span_coe_preimage : span R ((coe : span R s → M) ⁻¹' s) = ⊤ :=
 eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
   refine span_induction' (λ x hx, _) _ (λ x y _ _, _) (λ r x _, _) hx,
diff --git a/src/ring_theory/adjoin/basic.lean b/src/ring_theory/adjoin/basic.lean
index 1e8853cbe9fbf..a3fe9753cca19 100644
--- a/src/ring_theory/adjoin/basic.lean
+++ b/src/ring_theory/adjoin/basic.lean
@@ -109,6 +109,24 @@ subtype.rec_on x $ λ x hx, begin
     exists.elim hy $ λ hy' hy, ⟨subalgebra.mul_mem _ hx' hy', Hmul _ _ hx hy⟩),
 end
 
+/-- Two algebra morphisms from `algebra.adjoin` are equal if they agree on the generators.
+
+See note [partially-applied ext lemmas]-/
+@[ext] lemma _root_.alg_hom.adjoin_ext {s : set A} ⦃f g : adjoin R s →ₐ[R] B⦄
+  (h : f ∘ set.inclusion subset_adjoin = g ∘ set.inclusion subset_adjoin) : f = g :=
+begin
+  ext x,
+  refine adjoin_induction' _ _ _ _ x,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intro r,
+    exact (f.commutes _).trans (g.commutes _).symm },
+  { intros x y hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros x y hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+end
+
 @[simp] lemma adjoin_adjoin_coe_preimage {s : set A} :
   adjoin R ((coe : adjoin R s → A) ⁻¹' s) = ⊤ :=
 begin

From 7012ca7cebf26fad11e37d59b3715ca1334d7a7f Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 19 Apr 2023 17:52:33 +0000
Subject: [PATCH 2/2] deduplicate, fix names

---
 src/algebra/star/subalgebra.lean              | 52 +++++++++----------
 src/group_theory/subgroup/basic.lean          |  2 +-
 src/group_theory/submonoid/operations.lean    |  2 +-
 src/group_theory/subsemigroup/operations.lean |  2 +-
 src/linear_algebra/span.lean                  |  2 +-
 5 files changed, 29 insertions(+), 31 deletions(-)

diff --git a/src/algebra/star/subalgebra.lean b/src/algebra/star/subalgebra.lean
index 3a5ae3cebd569..f99493dd443c6 100644
--- a/src/algebra/star/subalgebra.lean
+++ b/src/algebra/star/subalgebra.lean
@@ -445,24 +445,6 @@ begin
     λ x hx, exists.elim hx (λ hx' hx, ⟨star_mem hx', Hstar _ hx⟩)]
 end
 
-/-- Two algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the generators.
-
-See note [partially-applied ext lemmas]-/
-@[ext] lemma _root_.star_alg_hom.adjoin_ext {s : set A} ⦃f g : adjoin R s →⋆ₐ[R] B⦄
-  (h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g :=
-begin
-  ext x,
-  refine adjoin_induction' x _ _ _ _ _,
-  { intros x hx,
-    exact (congr_fun h ⟨x, hx⟩ : _) },
-  { intro r,
-    exact (alg_hom_class.commutes f _).trans (alg_hom_class.commutes g _).symm },
-  { intros x y hfgx hfgy,
-    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
-  { intros x y hfgx hfgy,
-    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
-end
-
 variables (R)
 
 /-- If all elements of `s : set A` commute pairwise and also commute pairwise with elements of
@@ -631,18 +613,34 @@ lemma map_adjoin [star_module R B] (f : A →⋆ₐ[R] B) (s : set A) :
 galois_connection.l_comm_of_u_comm set.image_preimage (gc_map_comap f) star_subalgebra.gc
   star_subalgebra.gc (λ _, rfl)
 
-lemma ext_adjoin {s : set A} [star_alg_hom_class F R (adjoin R s) B] {f g : F}
-  (h : ∀ x : adjoin R s, (x : A) ∈ s → f x = g x) : f = g :=
+/-- Two star algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the
+generators -/
+lemma _root_.star_alg_hom_class.ext_adjoin
+  {s : set A} [star_alg_hom_class F R (adjoin R s) B] ⦃f g : F⦄
+  (h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g :=
 begin
-  refine fun_like.ext f g (λ a, adjoin_induction' a (λ x hx, _) (λ r, _) (λ x y hx hy, _)
-    (λ x y hx hy, _) (λ x hx, _)),
-  { exact h ⟨x, subset_adjoin R s hx⟩ hx },
-  { simp only [alg_hom_class.commutes] },
-  { rw [map_add, map_add, hx, hy] },
-  { rw [map_mul, map_mul, hx, hy] },
-  { rw [map_star, map_star, hx] },
+  refine fun_like.ext _ _ (λ x, _),
+  refine adjoin_induction' x _ _ _ _ _,
+  { intros x hx,
+    exact (congr_fun h ⟨x, hx⟩ : _) },
+  { intro r,
+    exact (alg_hom_class.commutes f _).trans (alg_hom_class.commutes g _).symm },
+  { intros x y hfgx hfgy,
+    exact (map_add f _ _).trans ((congr_arg2 (+) hfgx hfgy).trans (map_add g _ _).symm) },
+  { intros x y hfgx hfgy,
+    exact (map_mul f _ _).trans ((congr_arg2 (*) hfgx hfgy).trans (map_mul g _ _).symm) },
+  { intros x hfg,
+    exact (map_star f _).trans ((congr_arg star hfg).trans (map_star g _).symm) },
 end
 
+/-- Two star algebra morphisms from `star_subalgebra.adjoin` are equal if they agree on the
+generators.
+
+See note [partially-applied ext lemmas]. -/
+@[ext] lemma ext_adjoin {s : set A} ⦃f g : adjoin R s →⋆ₐ[R] B⦄
+  (h : f ∘ set.inclusion (subset_adjoin _ _) = g ∘ set.inclusion (subset_adjoin _ _)) : f = g :=
+star_alg_hom_class.ext_adjoin h
+
 lemma ext_adjoin_singleton {a : A} [star_alg_hom_class F R (adjoin R ({a} : set A)) B] {f g : F}
   (h : f ⟨a, self_mem_adjoin_singleton R a⟩ = g ⟨a, self_mem_adjoin_singleton R a⟩) : f = g :=
 ext_adjoin $ λ x hx, (show x = ⟨a, self_mem_adjoin_singleton R a⟩,
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index df57a7f518fe4..aa578ae6d7a44 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -794,7 +794,7 @@ See note [partially-applied ext lemmas]-/
 generators.
 
 See note [partially-applied ext lemmas]"]
-lemma _root_.monoid_hom.closure_ext {s : set G} ⦃f g : closure s →* G'⦄
+lemma _root_.monoid_hom.ext_closure {s : set G} ⦃f g : closure s →* G'⦄
   (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
 begin
   ext ⟨x, hx⟩,
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
index 294cc58edc591..685a7388cd66a 100644
--- a/src/group_theory/submonoid/operations.lean
+++ b/src/group_theory/submonoid/operations.lean
@@ -624,7 +624,7 @@ See note [partially-applied ext lemmas]-/
 generators.
 
 See note [partially-applied ext lemmas]"]
-lemma _root_.monoid_hom.mclosure_ext {s : set M} ⦃f g : closure s →* N⦄
+lemma _root_.monoid_hom.ext_mclosure {s : set M} ⦃f g : closure s →* N⦄
   (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
 begin
   ext ⟨x, hx⟩,
diff --git a/src/group_theory/subsemigroup/operations.lean b/src/group_theory/subsemigroup/operations.lean
index f7c06f46983d0..3871b5b92565a 100644
--- a/src/group_theory/subsemigroup/operations.lean
+++ b/src/group_theory/subsemigroup/operations.lean
@@ -469,7 +469,7 @@ See note [partially-applied ext lemmas]-/
 generators.
 
 See note [partially-applied ext lemmas]"]
-lemma _root_.mul_hom.closure_ext {s : set M} ⦃f g : closure s →ₙ* N⦄
+lemma _root_.mul_hom.ext_closure {s : set M} ⦃f g : closure s →ₙ* N⦄
   (h : f ∘ set.inclusion subset_closure = g ∘ set.inclusion subset_closure) : f = g :=
 begin
   ext ⟨x, hx⟩,
diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean
index 4f50e29441f41..bb501ddd5221c 100644
--- a/src/linear_algebra/span.lean
+++ b/src/linear_algebra/span.lean
@@ -141,7 +141,7 @@ end
 /-- Two linear maps from a span are equal if they agree on the generators.
 
 See note [partially-applied ext lemmas]-/
-@[ext] lemma _root_.linear_map.span_ext {s : set M} ⦃f g : span R s →ₛₗ[σ₁₂] M₂⦄
+@[ext] lemma _root_.linear_map.ext_span {s : set M} ⦃f g : span R s →ₛₗ[σ₁₂] M₂⦄
   (h : f ∘ set.inclusion subset_span = g ∘ set.inclusion subset_span) : f = g :=
 begin
   ext ⟨x, hx⟩,