no goals
ι : Type ?u.1622
α : Type u_1
β : Type ?u.1628
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ Set.Infinite {x | p x}
simp only [Filter.Frequently, Filter.Eventually, mem_cofinite, compl_setOf, not_not,
  Set.Infinite]