no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.66086
ι : Sort x
f✝ g : Filter α
s t x : Set α
f : ι → Filter α
⊢ x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i
simp only [← Filter.mem_sets, iSup_sets_eq, iff_self_iff, mem_iInter]