no goals
α : Type u_1
β : Type u_2
γ : Type ?u.57703
δ : Type ?u.57706
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ Inducing (↑(Homeomorph.symm h) ∘ ↑h)
simp only [symm_comp_self, inducing_id]