no goals
ι : Sort ?u.5011
α : Type u_1
β : Type u_2
X : Type ?u.5020
Y : Type ?u.5023
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ (s : Set β), s ∈ lb → ∀ᶠ (a : α) in la, s ∈ f a
simp only [nhds_eq', tendsto_lift', mem_setOf_eq]