no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T1Space β
f : α → β
a : α
b : β
h : Tendsto f (𝓝 a) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
rwa [eq_of_tendsto_nhds h]