no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42346
ι : Sort ?u.42349
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
hh : Monotone h
⊢ (∀ (s : Set α), s ∈ f → NeBot (𝓟 (h s))) ↔ ∀ (s : Set α), s ∈ f → Set.Nonempty (h s)
simp only [principal_neBot_iff]