no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.4384
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Inducing f
x : α
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]