no goals
α✝ : Type u
β : Type v
γ : Type w
δ : Type ?u.273604
ι✝ : Sort x
f✝ f₁ f₂ : Filter α✝
g g₁ g₂ : Filter β
m : α✝ → β
m' : β → γ
s : Set α✝
t : Set β
ι : Type u_1
α : ι → Type u_2
inst✝ : ∀ (j : ι), Nonempty (α j)
i : ι
f : Filter (α i)
⊢ NeBot (comap (eval i) f) ↔ NeBot f
simp [comap_eval_neBot_iff', *]