no goals
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p { x // x ∈ P }
Q : Sylow p G
⊢ Q ∈ fixedPoints { x // x ∈ P } (Sylow p G) ↔ P ≤ ↑Q
rw [P.sylow_mem_fixedPoints_iff, ← inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]