no goals
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = ⊤
rw [← Sylow.normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
  inf_of_le_left hP]