[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ Homotopic (comp (toContinuousMap (Homeomorph.symm h)) (toContinuousMap h)) (ContinuousMap.id X)
[PROOFSTEP]
rw [symm_comp_toContinuousMap]
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ Homotopic (comp (toContinuousMap h) (toContinuousMap (Homeomorph.symm h))) (ContinuousMap.id Y)
[PROOFSTEP]
rw [toContinuousMap_comp_symm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₁.invFun h₂.invFun) (comp h₂.toFun h₁.toFun)) (ContinuousMap.id X)
[PROOFSTEP]
refine Homotopic.trans ?_ h₁.left_inv
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₁.invFun h₂.invFun) (comp h₂.toFun h₁.toFun)) (comp h₁.invFun h₁.toFun)
[PROOFSTEP]
exact ((Homotopic.refl _).hcomp h₂.left_inv).hcomp (Homotopic.refl _)
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₂.toFun h₁.toFun) (comp h₁.invFun h₂.invFun)) (ContinuousMap.id Z)
[PROOFSTEP]
refine Homotopic.trans ?_ h₂.right_inv
[GOAL]
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h₁ : X ≃ₕ Y
h₂ : Y ≃ₕ Z
⊢ Homotopic (comp (comp h₂.toFun h₁.toFun) (comp h₁.invFun h₂.invFun)) (comp h₂.toFun h₂.invFun)
[PROOFSTEP]
exact ((Homotopic.refl _).hcomp h₁.right_inv).hcomp (Homotopic.refl _)
