Improve mapping out of a generated subgroup

theories/Algebra/Groups/Subgroup.v

@@ -557,20 +557,29 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H :
   : subgroup_generated X
   := (g; tr (sgt_in H)).
 
+(** The generated subgroup is the smallest subgroup containing the generating set. *)
+Definition subgroup_generated_rec {G : Group} (X : G -> Type) (S : Subgroup G)
+  (i : forall g, X g -> S g)
+  : forall g, subgroup_generated X g -> S g.
+Proof.
+  intros g; rapply Trunc_rec; intros p.
+  induction p as [g Xg | | g h p1 IHp1 p2 IHp2].
+  - by apply i.
+  - apply subgroup_in_unit.
+  - by apply subgroup_in_op_inv.
+Defined.
+
 (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
 Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
   (f : G $-> H) (preserves : forall g, X g -> Y (f g))
   : forall g, subgroup_generated X g -> subgroup_generated Y (f g).
 Proof.
-  intro g.
-  apply Trunc_functor.
-  intro p.
-  induction p as [g i | | g h p1 IHp1 p2 IHp2].
-  - apply sgt_in, preserves, i.
-  - rewrite grp_homo_unit.
-    apply sgt_unit.
-  - rewrite grp_homo_op, grp_homo_inv.
-    by apply sgt_op.
+  change (subgroup_generated Y (f ?g))
+    with (subgroup_preimage f (subgroup_generated Y) g).
+  apply subgroup_generated_rec.
+  intros g p.
+  apply tr, sgt_in.
+  by apply preserves.
 Defined.
 
 (** The product of two subgroups. *)