feat(group_theory): generalize normal_map (#17808)

src/group_theory/quotient_group.lean

@@ -489,13 +489,8 @@ variables (M : subgroup G) [nM : M.normal]
 
 include nM nN
 
-@[to_additive quotient_add_group.map_normal]
-instance map_normal : (M.map (quotient_group.mk' N)).normal :=
-{ conj_mem := begin
-    rintro _ ⟨x, hx, rfl⟩ y,
-    refine induction_on' y (λ y, ⟨y * x * y⁻¹, subgroup.normal.conj_mem nM x hx y, _⟩),
-    simp only [mk'_apply, coe_mul, coe_inv]
-  end }
+@[to_additive] instance map_normal : (M.map (quotient_group.mk' N)).normal :=
+nM.map _ mk_surjective
 
 variables (h : N ≤ M)
 

src/group_theory/subgroup/basic.lean

@@ -2230,6 +2230,15 @@ namespace subgroup
 
 variables {N : Type*} [group N] (H : subgroup G)
 
+@[to_additive]
+lemma normal.map {H : subgroup G} (h : H.normal) (f : G →* N) (hf : function.surjective f) :
+  (H.map f).normal :=
+begin
+  rw [← normalizer_eq_top, ← top_le_iff, ← f.range_top_of_surjective hf, f.range_eq_map,
+    ← normalizer_eq_top.2 h],
+  exact le_normalizer_map _
+end
+
 @[to_additive] lemma map_eq_bot_iff {f : G →* N} : H.map f = ⊥ ↔ H ≤ f.ker :=
 (gc_map_comap f).l_eq_bot