no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.110309
ι : Sort x
f✝ g : Filter α
s t : Set α
f : ι → Filter α
inst✝ : Nonempty ι
hd : Directed (fun x x_1 => x ≥ x_1) f
⊢ ¬NeBot (iInf f) → ¬∀ (i : ι), NeBot (f i)
simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
mem_iInf_of_directed hd] using id