no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160738
ι : Sort x
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x => p x) x
⊢ False
simpa only [and_not_self_iff, exists_false] using H hp