feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups on those types (leanprover-community#34624)

feat(GroupTheory/FreeGroup/Basic): adds the theorem that if `α` and `β` are arbitrary types and there is a surjection between them, then the induced FreeGroup.map is also surjective.

This is a dependency of a larger PR to formalize finitely presented groups leanprover-community#34236.

Author: homeowmorphism

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -9,7 +9,7 @@ public import Mathlib.Algebra.Group.Pi.Basic
 public import Mathlib.Algebra.Group.Subgroup.Ker
 public import Mathlib.Data.List.Chain
 public import Mathlib.Algebra.Group.Int.Defs
-public import Mathlib.Algebra.BigOperators.Group.List.Defs
+public import Mathlib.Algebra.BigOperators.Group.List.Basic
 public import Mathlib.Algebra.Group.Nat.Defs
 
 /-!
@@ -782,8 +782,19 @@ theorem map.unique (g : FreeGroup α →* FreeGroup β)
           FreeGroup.map f (FreeGroup.of x * FreeGroup.mk t) by simp [g.map_mul, hg, ih])
 
 @[to_additive]
-theorem map_eq_lift : map f x = lift (of ∘ f) x :=
-  Eq.symm <| map.unique _ fun x => by simp
+theorem map_eq_lift : map f = lift (of ∘ f) := by
+  ext; simp
+
+@[to_additive]
+theorem range_map : (map f).range = Subgroup.closure (of '' Set.range f) := by
+  rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]
+
+/-- If `α` and `β` are arbitrary types and there is a surjection between them,
+then the induced map on their free groups is also surjective. -/
+@[to_additive /-- If `α` and `β` are arbitrary types and there is a surjection between them,
+then the induced map on their additive free groups is also surjective. -/]
+theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map f) := by
+  rw [← MonoidHom.range_eq_top, range_map, hf.range_eq, Set.image_univ, closure_range_of]
 
 /-- Equivalent types give rise to multiplicatively equivalent free groups.