no goals
α : Type ?u.3470
β : Type u_2
γ : Type u_3
δ : Type ?u.3479
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
ι : Type u_1
f : ι → β
g : β → γ
a : Filter ι
b : β
hg : Inducing g
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (g ∘ f) a (𝓝 (g b))
rw [hg.nhds_eq_comap, tendsto_comap_iff]