no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.163984
ι : Sort x
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x
simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]