no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.169389
ι : Sort x
f : Filter α
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, not_imp]