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