case h
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ normalizer ↑P
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
⊢ stabilizer G P = normalizer ↑P
ext
no goals
case h
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ normalizer ↑P
simp [Sylow.smul_eq_iff_mem_normalizer]