chore(Algebra/Group/Subgroup/Basic): automated extraction from leanprover-community#38864 (leanprover-community#40842)

This PR was automatically created from PR leanprover-community#38864 by @xroblot via a [review comment](leanprover-community#38864 (comment)) by @tb65536.

Co-authored-by: xroblot <46200072+xroblot@users.noreply.github.com>

Author: mathlib-splicebot[bot]

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -939,6 +939,15 @@ theorem Normal.of_map_subtype {K : Subgroup G} {L : Subgroup K}
     (n : (Subgroup.map K.subtype L).Normal) : L.Normal :=
   n.of_map_injective K.subtype_injective
 
+theorem normal_comap_iff_of_surjective {f : G →* N} (hf : Function.Surjective f) {H : Subgroup N} :
+    (H.comap f).Normal ↔ H.Normal := by
+  rw [← normalizer_eq_top_iff, ← comap_normalizer_eq_of_surjective H hf, ← comap_top f,
+    (comap_injective hf).eq_iff, normalizer_eq_top_iff]
+
+theorem _root_.MulEquiv.normal_map_iff {f : G ≃* G'} {H : Subgroup G} :
+    (H.map (f : G →* G')).Normal ↔ H.Normal := by
+  rw [map_equiv_eq_comap_symm, normal_comap_iff_of_surjective f.symm.surjective]
+
 section SubgroupNormal
 
 @[to_additive]