no goals
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hn : Normal (normalizer ↑P)
⊢ Normal ↑P
rw [← normalizer_eq_top, ← normalizer_sup_eq_top' P le_normalizer, sup_idem]