chore(group_theory/*): Golf using subgroup.subtype_injective (#16941)

This PR uses the recently added `subgroup.subtype_injective` to golf a few lines.

src/group_theory/schur_zassenhaus.lean

@@ -206,7 +206,7 @@ begin
   have key := step2 h1 h2 h3 (K.map N.subtype) K.map_subtype_le,
   rw ← map_bot N.subtype at key,
   conv at key { congr, skip, to_rhs, rw [←N.subtype_range, N.subtype.range_eq_map] },
-  have inj := map_injective (show function.injective N.subtype, from subtype.coe_injective),
+  have inj := map_injective N.subtype_injective,
   rwa [inj.eq_iff, inj.eq_iff] at key,
 end
 

src/group_theory/solvable.lean

@@ -136,7 +136,7 @@ lemma solvable_of_solvable_injective (hf : function.injective f) [h : is_solvabl
 solvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot_iff.mpr hf).symm ▸ bot_le)
 
 instance subgroup_solvable_of_solvable (H : subgroup G) [h : is_solvable G] : is_solvable H :=
-solvable_of_solvable_injective (show function.injective (subtype H), from subtype.val_injective)
+solvable_of_solvable_injective H.subtype_injective
 
 lemma solvable_of_surjective (hf : function.surjective f) [h : is_solvable G] :
   is_solvable G' :=

src/group_theory/subgroup/basic.lean

@@ -2417,7 +2417,7 @@ end
 @[to_additive] lemma closure_preimage_eq_top (s : set G) :
   closure ((closure s).subtype ⁻¹' s) = ⊤ :=
 begin
-  apply map_injective (show function.injective (closure s).subtype, from subtype.coe_injective),
+  apply map_injective (closure s).subtype_injective,
   rwa [monoid_hom.map_closure, ←monoid_hom.range_eq_map, subtype_range,
     set.image_preimage_eq_of_subset],
   rw [coe_subtype, subtype.range_coe_subtype],

src/group_theory/sylow.lean

@@ -165,7 +165,7 @@ sylow.fintype_of_ker_is_p_group (is_p_group.ker_is_p_group_of_injective hf)
 
 /-- If `H` is a subgroup of `G`, then `fintype (sylow p G)` implies `fintype (sylow p H)`. -/
 noncomputable instance (H : subgroup G) [fintype (sylow p G)] : fintype (sylow p H) :=
-sylow.fintype_of_injective (show function.injective H.subtype, from subtype.coe_injective)
+sylow.fintype_of_injective H.subtype_injective
 
 /-- If `H` is a subgroup of `G`, then `finite (sylow p G)` implies `finite (sylow p H)`. -/
 instance (H : subgroup G) [finite (sylow p G)] : finite (sylow p H) :=