no goals
α : Type u_1
β : Type u_2
γ : Type ?u.20338
ι : Sort ?u.20341
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hm : Monotone g
⊢ NeBot (Filter.lift f g) ↔ ∀ (s : Set α), s ∈ f → NeBot (g s)
simp only [neBot_iff, Ne.def, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists, not_and]