feat: port GroupTheory.FreeProduct (#2979)

Mathlib.lean

@@ -1005,6 +1005,7 @@ import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeGroup
+import Mathlib.GroupTheory.FreeProduct
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.BigOperators
 import Mathlib.GroupTheory.GroupAction.ConjAct

Mathlib/Algebra/Algebra/Unitization.lean

@@ -651,7 +651,7 @@ theorem algHom_ext {φ ψ : Unitization R A →ₐ[S] B} (h : ∀ a : A, φ a =
 #align unitization.alg_hom_ext Unitization.algHom_ext
 
 /-- See note [partially-applied ext lemmas] -/
-@[ext 1001]
+@[ext 1100]
 theorem algHom_ext' {φ ψ : Unitization R A →ₐ[R] C}
     (h :
       φ.toNonUnitalAlgHom.comp (inrNonUnitalAlgHom R A) =

Mathlib/Algebra/Free.lean

@@ -81,7 +81,7 @@ noncomputable def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of
   FreeMagma.recOn x ih1 ih2
 #align free_magma.rec_on_mul FreeMagma.recOnMul
 
-@[to_additive (attr := ext 1001)]
+@[to_additive (attr := ext 1100)]
 theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
   (FunLike.ext _ _) fun x ↦ recOnMul x (congr_fun h) <| by intros ; simp only [map_mul, *]
 #align free_magma.hom_ext FreeMagma.hom_ext
@@ -394,7 +394,7 @@ section lift
 
 variable {β : Type v} [Semigroup β] (f : α →ₙ* β)
 
-@[to_additive (attr := ext 1001)]
+@[to_additive (attr := ext 1100)]
 theorem hom_ext {f g : AssocQuotient α →ₙ* β} (h : f.comp of = g.comp of) : f = g :=
   (FunLike.ext _ _) fun x => AssocQuotient.induction_on x <| FunLike.congr_fun h
 #align magma.assoc_quotient.hom_ext Magma.AssocQuotient.hom_ext
@@ -514,7 +514,7 @@ protected noncomputable def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1
       List.recOn s ih1 (fun hd tl ih f ↦ ih2 f ⟨hd, tl⟩ (ih1 f) (ih hd)) f
 #align free_semigroup.rec_on_mul FreeSemigroup.recOnMul
 
-@[to_additive (attr := ext 1001)]
+@[to_additive (attr := ext 1100)]
 theorem hom_ext {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
   (FunLike.ext _ _) fun x ↦
     FreeSemigroup.recOnMul x (congr_fun h) fun x y hx hy ↦ by simp only [map_mul, *]

Mathlib/Data/MvPolynomial/Basic.lean

@@ -455,7 +455,7 @@ theorem ringHom_ext {A : Type _} [Semiring A] {f g : MvPolynomial σ R →+* A}
 #align mv_polynomial.ring_hom_ext MvPolynomial.ringHom_ext
 
 /-- See note [partially-applied ext lemmas]. -/
-@[ext 1001]
+@[ext 1100]
 theorem ringHom_ext' {A : Type _} [Semiring A] {f g : MvPolynomial σ R →+* A}
     (hC : f.comp C = g.comp C) (hX : ∀ i, f (X i) = g (X i)) : f = g :=
   ringHom_ext (RingHom.ext_iff.1 hC) hX
@@ -471,7 +471,7 @@ theorem is_id (f : MvPolynomial σ R →+* MvPolynomial σ R) (hC : f.comp C = C
   hom_eq_hom f (RingHom.id _) hC hX p
 #align mv_polynomial.is_id MvPolynomial.is_id
 
-@[ext 1001]
+@[ext 1100]
 theorem algHom_ext' {A B : Type _} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B]
     {f g : MvPolynomial σ A →ₐ[R] B}
     (h₁ :
@@ -481,7 +481,7 @@ theorem algHom_ext' {A B : Type _} [CommSemiring A] [CommSemiring B] [Algebra R
   AlgHom.coe_ringHom_injective (MvPolynomial.ringHom_ext' (congr_arg AlgHom.toRingHom h₁) h₂)
 #align mv_polynomial.alg_hom_ext' MvPolynomial.algHom_ext'
 
-@[ext 1002]
+@[ext 1200]
 theorem algHom_ext {A : Type _} [Semiring A] [Algebra R A] {f g : MvPolynomial σ R →ₐ[R] A}
     (hf : ∀ i : σ, f (X i) = g (X i)) : f = g :=
   AddMonoidAlgebra.algHom_ext' (mulHom_ext' fun X : σ => MonoidHom.ext_mnat (hf X))

Mathlib/Data/Polynomial/AlgebraMap.lean

@@ -88,7 +88,7 @@ set_option linter.uppercaseLean3 false in
 
 /-- Extensionality lemma for algebra maps out of `A'[X]` over a smaller base ring than `A'`
 -/
-@[ext 1001]
+@[ext 1100]
 theorem algHom_ext' [Algebra R A'] [Algebra R B'] {f g : A'[X] →ₐ[R] B'}
     (h₁ : f.comp (IsScalarTower.toAlgHom R A' A'[X]) = g.comp (IsScalarTower.toAlgHom R A' A'[X]))
     (h₂ : f X = g X) : f = g :=
@@ -184,7 +184,7 @@ theorem adjoin_X : Algebra.adjoin R ({X} : Set R[X]) = ⊤ := by
 set_option linter.uppercaseLean3 false in
 #align polynomial.adjoin_X Polynomial.adjoin_X
 
-@[ext 1002]
+@[ext 1200]
 theorem algHom_ext {f g : R[X] →ₐ[R] A} (h : f X = g X) : f = g :=
   AlgHom.ext_of_adjoin_eq_top adjoin_X fun _p hp => (Set.mem_singleton_iff.1 hp).symm ▸ h
 #align polynomial.alg_hom_ext Polynomial.algHom_ext