no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.263265
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
m : α → β
⊢ NeBot (comap m f) ↔ ∃ᶠ (y : β) in f, y ∈ range m
simp only [comap_neBot_iff, frequently_iff, mem_range, @and_comm (_ ∈ _), exists_exists_eq_and]