no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.62053
ι : Sort x
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ NeBot (f ⊔ g) ↔ NeBot f ∨ NeBot g
simp only [neBot_iff, not_and_or, Ne.def, sup_eq_bot_iff]