no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.173757
ι : Sort x
p : α → Prop
fs : Set (Filter α)
⊢ (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f, f ∈ fs ∧ ∃ᶠ (x : α) in f, p x
simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]