feat(group_theory/free_product): add (m)range_eq_supr (#12956)

and lemmas leading to it as inspired by the corresponding lemmas from
`free_groups.lean`.

As suggested by @ocfnash, polish the free group lemmas a bit as well.

src/group_theory/free_group.lean

@@ -456,32 +456,23 @@ lift.symm.injective $ funext h
 theorem lift.of_eq (x : free_group α) : lift of x = x :=
 monoid_hom.congr_fun (lift.apply_symm_apply (monoid_hom.id _)) x
 
-theorem lift.range_subset {s : subgroup β} (H : set.range f ⊆ s) :
-  set.range (lift f) ⊆ s :=
+theorem lift.range_le {s : subgroup β} (H : set.range f ⊆ s) :
+  (lift f).range ≤ s :=
 by rintros _ ⟨⟨L⟩, rfl⟩; exact list.rec_on L s.one_mem
 (λ ⟨x, b⟩ tl ih, bool.rec_on b
     (by simp at ih ⊢; from s.mul_mem
       (s.inv_mem $ H ⟨x, rfl⟩) ih)
     (by simp at ih ⊢; from s.mul_mem (H ⟨x, rfl⟩) ih))
 
-theorem closure_subset {G : Type*} [group G] {s : set G} {t : subgroup G}
-  (h : s ⊆ t) : subgroup.closure s ≤ t :=
+theorem lift.range_eq_closure :
+  (lift f).range = subgroup.closure (set.range f) :=
 begin
-  simp only [h, subgroup.closure_le],
+  apply le_antisymm (lift.range_le subgroup.subset_closure),
+  rw subgroup.closure_le,
+  rintros _ ⟨a, rfl⟩,
+  exact ⟨of a, by simp only [lift.of]⟩,
 end
 
-theorem lift.range_eq_closure :
-  set.range (lift f) = subgroup.closure (set.range f) :=
-set.subset.antisymm
-  (lift.range_subset subgroup.subset_closure)
-  begin
-    suffices : (subgroup.closure (set.range f)) ≤ monoid_hom.range (lift f),
-      simpa,
-    rw subgroup.closure_le,
-    rintros y ⟨x, hx⟩,
-    exact ⟨of x, by simpa⟩
-  end
-
 end lift
 
 section map

src/group_theory/free_product.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Wärn
+Authors: David Wärn, Joachim Breitner
 -/
 import algebra.free_monoid
 import group_theory.congruence
@@ -151,6 +151,25 @@ lemma of_left_inverse [decidable_eq ι] (i : ι) :
 lemma of_injective (i : ι) : function.injective ⇑(of : M i →* _) :=
 by { classical, exact (of_left_inverse i).injective }
 
+lemma lift_mrange_le {N} [monoid N] (f : Π i, M i →* N) {s : submonoid N}
+  (h : ∀ i, (f i).mrange ≤ s) : (lift f).mrange ≤ s :=
+begin
+  rintros _ ⟨x, rfl⟩,
+  induction x using free_product.induction_on with i x x y hx hy,
+  { exact s.one_mem, },
+  { simp only [lift_of, set_like.mem_coe], exact h i (set.mem_range_self x), },
+  { simp only [map_mul, set_like.mem_coe], exact s.mul_mem hx hy, },
+end
+
+lemma mrange_eq_supr {N} [monoid N] (f : Π i, M i →* N) :
+  (lift f).mrange = ⨆ i, (f i).mrange :=
+begin
+  apply le_antisymm (lift_mrange_le f (λ i, le_supr _ i)),
+  apply supr_le _,
+  rintros i _ ⟨x, rfl⟩,
+  exact ⟨of x, by simp only [lift_of]⟩
+end
+
 section group
 
 variables (G : ι → Type*) [Π i, group (G i)]
@@ -176,6 +195,25 @@ instance : group (free_product G) :=
   ..free_product.has_inv G,
   ..free_product.monoid G }
 
+lemma lift_range_le {N} [group N] (f : Π i, G i →* N) {s : subgroup N}
+  (h : ∀ i, (f i).range ≤ s) : (lift f).range ≤ s :=
+begin
+  rintros _ ⟨x, rfl⟩,
+  induction x using free_product.induction_on with i x x y hx hy,
+  { exact s.one_mem, },
+  { simp only [lift_of, set_like.mem_coe], exact h i (set.mem_range_self x), },
+  { simp only [map_mul, set_like.mem_coe], exact s.mul_mem hx hy, },
+end
+
+lemma range_eq_supr {N} [group N] (f : Π i, G i →* N) :
+  (lift f).range = ⨆ i, (f i).range :=
+begin
+  apply le_antisymm (lift_range_le _ f (λ i, le_supr _ i)),
+  apply supr_le _,
+  rintros i _ ⟨x, rfl⟩,
+  exact ⟨of x, by simp only [lift_of]⟩
+end
+
 end group
 
 namespace word