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