no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.472
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hg : Inducing g
hf : Inducing f
⊢ inst✝³ = TopologicalSpace.induced (g ∘ f) inst✝¹
rw [hf.induced, hg.induced, induced_compose]