no goals
α : Type u_1
β : Type ?u.711
γ : Type ?u.714
δ : Type ?u.717
inst✝ : TopologicalSpace α
z : α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓝[s] z, p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s
simp only [Filter.Frequently, eventually_nhdsWithin_iff, not_and']