feat(group_theory/free_product): is_free_group_free_product_of_is_fre…

…e_group (#12125)

src/group_theory/free_product.lean

@@ -5,6 +5,7 @@ Authors: David Wärn
 -/
 import algebra.free_monoid
 import group_theory.congruence
+import group_theory.is_free_group
 import data.list.chain
 /-!
 # The free product of groups or monoids
@@ -327,4 +328,19 @@ instance : decidable_eq (free_product M) := word.equiv.decidable_eq
 
 end word
 
+/-- The free product of free groups is itself a free group -/
+@[simps]
+instance {ι : Type*} (G : ι → Type*) [∀ i, group (G i)] [hG : ∀ i, is_free_group (G i)] :
+  is_free_group (free_product G) :=
+{ generators := Σ i, is_free_group.generators (G i),
+  of := λ x, free_product.of (is_free_group.of x.2),
+  unique_lift' :=
+  begin
+    introsI X _ f,
+    refine ⟨free_product.lift (λ i, is_free_group.lift (λ x, f ⟨i, x⟩)), _ ⟩,
+    split,
+    { simp, },
+    { intros g hfg, ext i x, simpa using hfg ⟨i, x⟩, }
+  end, }
+
 end free_product