no goals
α : Type u_1
β : Type ?u.104073
γ : Type ?u.104076
ι : Type ?u.104079
ι' : Sort ?u.104082
f : Filter α
inst✝ : IsCountablyGenerated f
x : ℕ → Set α
hx : HasAntitoneBasis f x
⊢ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s
simp [hx.1.mem_iff]