X Y : TopCat
f : X ≅ Y
⊢ Iso.mk
      (Homeomorph.toContinuousMap
        (Homeomorph.mk
          { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
            left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
            right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))
      (Homeomorph.toContinuousMap
        (Homeomorph.symm
          (Homeomorph.mk
            { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
              left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
              right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))) =
    f
X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f
dsimp [homeoOfIso, isoOfHomeo]
case w.w
X Y : TopCat
f : X ≅ Y
x✝ : (forget TopCat).obj X
⊢ (forget TopCat).map
      (Iso.mk
          (Homeomorph.toContinuousMap
            (Homeomorph.mk
              { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
                left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
                right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))
          (Homeomorph.toContinuousMap
            (Homeomorph.symm
              (Homeomorph.mk
                { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
                  left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
                  right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) })))).hom
      x✝ =
    (forget TopCat).map f.hom x✝
X Y : TopCat
f : X ≅ Y
⊢ Iso.mk
      (Homeomorph.toContinuousMap
        (Homeomorph.mk
          { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
            left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
            right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))
      (Homeomorph.toContinuousMap
        (Homeomorph.symm
          (Homeomorph.mk
            { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
              left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
              right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))) =
    f
ext
no goals
case w.w
X Y : TopCat
f : X ≅ Y
x✝ : (forget TopCat).obj X
⊢ (forget TopCat).map
      (Iso.mk
          (Homeomorph.toContinuousMap
            (Homeomorph.mk
              { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
                left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
                right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) }))
          (Homeomorph.toContinuousMap
            (Homeomorph.symm
              (Homeomorph.mk
                { toFun := (forget TopCat).map f.hom, invFun := (forget TopCat).map f.inv,
                  left_inv := (_ : ∀ (x : ↑X), (forget TopCat).map f.inv ((forget TopCat).map f.hom x) = x),
                  right_inv := (_ : ∀ (x : ↑Y), (forget TopCat).map f.hom ((forget TopCat).map f.inv x) = x) })))).hom
      x✝ =
    (forget TopCat).map f.hom x✝
rfl