feat(GroupTheory): add lemmas about Submonoid.closure and CoprodI (…

…#12391)

- Add `CoprodI.lift_comp_of`, `CoprodI.lift_comp_of'`,
  `CoprodI.lift_of'`, `CoprodI.iSup_mrange_of`,
  `CoprodI.mclosure_iUnion_range_of`, `CoprodI.induction_left`
- Add `MonoidHom.mrange_id`, `MonoidHom.mclosure_range`,
  as well as additive versions.

Mathlib/GroupTheory/CoprodI.lean

@@ -6,6 +6,7 @@ Authors: David Wärn, Joachim Breitner
 import Mathlib.Algebra.FreeMonoid.Basic
 import Mathlib.GroupTheory.Congruence
 import Mathlib.GroupTheory.FreeGroup.IsFreeGroup
+import Mathlib.GroupTheory.Submonoid.Membership
 import Mathlib.Data.List.Chain
 import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.Data.Set.Pointwise.SMul
@@ -173,24 +174,22 @@ def lift : (∀ i, M i →* N) ≃ (CoprodI M →* N) where
 #align free_product.lift Monoid.CoprodI.lift
 
 @[simp]
-theorem lift_of {N} [Monoid N] (fi : ∀ i, M i →* N) {i} (m : M i) : lift fi (of m) = fi i m := by
-  conv_rhs => rw [← lift.symm_apply_apply fi, lift_symm_apply, MonoidHom.comp_apply]
+theorem lift_comp_of {N} [Monoid N] (fi : ∀ i, M i →* N) i : (lift fi).comp of = fi i :=
+  congr_fun (lift.symm_apply_apply fi) i
+
+@[simp]
+theorem lift_of {N} [Monoid N] (fi : ∀ i, M i →* N) {i} (m : M i) : lift fi (of m) = fi i m :=
+  DFunLike.congr_fun (lift_comp_of ..) m
 #align free_product.lift_of Monoid.CoprodI.lift_of
 
-@[elab_as_elim]
-theorem induction_on {C : CoprodI M → Prop} (m : CoprodI M) (h_one : C 1)
-    (h_of : ∀ (i) (m : M i), C (of m)) (h_mul : ∀ x y, C x → C y → C (x * y)) : C m := by
-  let S : Submonoid (CoprodI M) :=
-    { carrier := setOf C
-      mul_mem' := h_mul _ _
-      one_mem' := h_one }
-  have : C _ := Subtype.prop (lift (fun i => of.codRestrict S (h_of i)) m)
-  convert this
-  change MonoidHom.id _ m = S.subtype.comp _ m
-  congr
-  ext i
-  rfl
-#align free_product.induction_on Monoid.CoprodI.induction_on
+@[simp]
+theorem lift_comp_of' {N} [Monoid N] (f : CoprodI M →* N) :
+    lift (fun i ↦ f.comp (of (i := i))) = f :=
+  lift.apply_symm_apply f
+
+@[simp]
+theorem lift_of' : lift (fun i ↦ (of : M i →* CoprodI M)) = .id (CoprodI M) :=
+  lift_comp_of' (.id _)
 
 theorem of_leftInverse [DecidableEq ι] (i : ι) :
     Function.LeftInverse (lift <| Pi.mulSingle i (MonoidHom.id (M i))) of := fun x => by
@@ -201,25 +200,44 @@ theorem of_injective (i : ι) : Function.Injective (of : M i →* _) := by
   classical exact (of_leftInverse i).injective
 #align free_product.of_injective Monoid.CoprodI.of_injective
 
-theorem lift_mrange_le {N} [Monoid N] (f : ∀ i, M i →* N) {s : Submonoid N}
-    (h : ∀ i, MonoidHom.mrange (f i) ≤ s) : MonoidHom.mrange (lift f) ≤ s := by
-  rintro _ ⟨x, rfl⟩
-  induction' x using CoprodI.induction_on with i x x y hx hy
-  · exact s.one_mem
-  · simp only [lift_of, SetLike.mem_coe]
-    exact h i (Set.mem_range_self x)
-  · simp only [map_mul, SetLike.mem_coe]
-    exact s.mul_mem hx hy
-#align free_product.lift_mrange_le Monoid.CoprodI.lift_mrange_le
-
 theorem mrange_eq_iSup {N} [Monoid N] (f : ∀ i, M i →* N) :
     MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i) := by
-  apply le_antisymm (lift_mrange_le f fun i => le_iSup (fun i => MonoidHom.mrange (f i)) i)
-  apply iSup_le _
-  rintro i _ ⟨x, rfl⟩
-  exact ⟨of x, by simp only [lift_of]⟩
+  rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
+    range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]
+  simp only [MonoidHom.mclosure_range]
 #align free_product.mrange_eq_supr Monoid.CoprodI.mrange_eq_iSup
 
+theorem lift_mrange_le {N} [Monoid N] (f : ∀ i, M i →* N) {s : Submonoid N} :
+    MonoidHom.mrange (lift f) ≤ s ↔ ∀ i, MonoidHom.mrange (f i) ≤ s := by
+  simp [mrange_eq_iSup]
+#align free_product.lift_mrange_le Monoid.CoprodI.lift_mrange_le
+
+@[simp]
+theorem iSup_mrange_of : ⨆ i, MonoidHom.mrange (of : M i →* CoprodI M) = ⊤ := by
+  simp [← mrange_eq_iSup]
+
+@[simp]
+theorem mclosure_iUnion_range_of :
+    Submonoid.closure (⋃ i, Set.range (of : M i →* CoprodI M)) = ⊤ := by
+  simp [Submonoid.closure_iUnion]
+
+@[elab_as_elim]
+theorem induction_left {C : CoprodI M → Prop} (m : CoprodI M) (one : C 1)
+    (mul : ∀ {i} (m : M i) x, C x → C (of m * x)) : C m := by
+  induction m using Submonoid.induction_of_closure_eq_top_left mclosure_iUnion_range_of with
+  | one => exact one
+  | mul x hx y ihy =>
+    obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
+    exact mul m y ihy
+
+@[elab_as_elim]
+theorem induction_on {C : CoprodI M → Prop} (m : CoprodI M) (h_one : C 1)
+    (h_of : ∀ (i) (m : M i), C (of m)) (h_mul : ∀ x y, C x → C y → C (x * y)) : C m := by
+  induction m using CoprodI.induction_left with
+  | one => exact h_one
+  | mul m x hx => exact h_mul _ _ (h_of _ _) hx
+#align free_product.induction_on Monoid.CoprodI.induction_on
+
 section Group
 
 variable (G : ι → Type*) [∀ i, Group (G i)]

Mathlib/GroupTheory/Submonoid/Operations.lean

@@ -979,6 +979,10 @@ theorem mrange_eq_map (f : F) : mrange f = (⊤ : Submonoid M).map f :=
 #align monoid_hom.mrange_eq_map MonoidHom.mrange_eq_map
 #align add_monoid_hom.mrange_eq_map AddMonoidHom.mrange_eq_map
 
+@[to_additive (attr := simp)]
+theorem mrange_id : mrange (MonoidHom.id M) = ⊤ := by
+  simp [mrange_eq_map]
+
 @[to_additive]
 theorem map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = mrange (comp g f) := by
   simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f
@@ -1019,6 +1023,10 @@ theorem map_mclosure (f : F) (s : Set M) : (closure s).map f = closure (f '' s)
 #align monoid_hom.map_mclosure MonoidHom.map_mclosure
 #align add_monoid_hom.map_mclosure AddMonoidHom.map_mclosure
 
+@[to_additive (attr := simp)]
+theorem mclosure_range (f : F) : closure (Set.range f) = mrange f := by
+  rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]
+
 /-- Restriction of a monoid hom to a submonoid of the domain. -/
 @[to_additive "Restriction of an `AddMonoid` hom to an `AddSubmonoid` of the domain."]
 def restrict {N S : Type*} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N)