no goals
α : Type u
β : Type v
γ : Type ?u.52285
f✝ : Filter α
s : Set α
a : α
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂
simpa only [tendsto_iff_comap] using le_iff_ultrafilter