G : Type u_1
G' : Type ?u.553569
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.553578
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
H✝ H : Subgroup G
h : Normal H
f : G →* N
hf : Surjective ↑f
⊢ Subgroup.map f (normalizer H) ≤ normalizer (Subgroup.map f H)
G : Type u_1
G' : Type ?u.553569
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.553578
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
H✝ H : Subgroup G
h : Normal H
f : G →* N
hf : Surjective ↑f
⊢ Normal (Subgroup.map f H)
rw [← normalizer_eq_top, ← top_le_iff, ← f.range_top_of_surjective hf, f.range_eq_map, ←
  normalizer_eq_top.2 h]
no goals
G : Type u_1
G' : Type ?u.553569
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.553578
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
H✝ H : Subgroup G
h : Normal H
f : G →* N
hf : Surjective ↑f
⊢ Subgroup.map f (normalizer H) ≤ normalizer (Subgroup.map f H)
exact le_normalizer_map _