no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.95811
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
f : ι → Filter α
h : Directed (fun x x_1 => x ≥ x_1) f
inst✝ : Nonempty ι
s : Set α
⊢ s ∈ iInf f ↔ ∃ i, s ∈ f i
simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]