no goals
α : Type u_2
β : Type u_1
γ : Type ?u.70207
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
g : β ≃ₜ γ
⊢ ContinuousMap.comp (toContinuousMap f) (toContinuousMap (Homeomorph.symm f)) = ContinuousMap.id β
rw [← coe_trans, symm_trans_self, coe_refl]