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