no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.174182
ι : Sort x
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ (b : β), fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x
simp only [Filter.Frequently, eventually_iSup, not_forall]