no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.161697
ι : Sort x
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ NeBot f
simp [Filter.Frequently, -not_eventually, eventually_false_iff_eq_bot, neBot_iff]