[GOAL]
⊢ ConcreteCategory TopCat
[PROOFSTEP]
dsimp [TopCat]
[GOAL]
⊢ ConcreteCategory (Bundled TopologicalSpace)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ Homeomorph.toContinuousMap f ≫ Homeomorph.toContinuousMap (Homeomorph.symm f) = 𝟙 X
[PROOFSTEP]
ext
[GOAL]
case w
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : (forget TopCat).obj X
⊢ ↑(Homeomorph.toContinuousMap f ≫ Homeomorph.toContinuousMap (Homeomorph.symm f)) x✝ = ↑(𝟙 X) x✝
[PROOFSTEP]
exact f.symm_apply_apply _
[GOAL]
X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ Homeomorph.toContinuousMap (Homeomorph.symm f) ≫ Homeomorph.toContinuousMap f = 𝟙 Y
[PROOFSTEP]
ext
[GOAL]
case w
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : (forget TopCat).obj Y
⊢ ↑(Homeomorph.toContinuousMap (Homeomorph.symm f) ≫ Homeomorph.toContinuousMap f) x✝ = ↑(𝟙 Y) x✝
[PROOFSTEP]
exact f.apply_symm_apply _
[GOAL]
X Y : TopCat
f : X ≅ Y
x : ↑X
⊢ ↑f.inv (↑f.hom x) = x
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : X ≅ Y
x : ↑Y
⊢ ↑f.hom (↑f.inv x) = x
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ homeoOfIso (isoOfHomeo f) = f
[PROOFSTEP]
dsimp [homeoOfIso, isoOfHomeo]
[GOAL]
X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ Homeomorph.mk
      { toFun := ↑(Homeomorph.toContinuousMap f), invFun := ↑(Homeomorph.toContinuousMap (Homeomorph.symm f)),
        left_inv :=
          (_ :
            ∀ (x : ↑X),
              ↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).2
                  (↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).1 x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : ↑Y),
              ↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).1
                  (↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).2 x) =
                x) } =
    f
[PROOFSTEP]
ext
[GOAL]
case H
X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : ↑X
⊢ ↑(Homeomorph.mk
          { toFun := ↑(Homeomorph.toContinuousMap f), invFun := ↑(Homeomorph.toContinuousMap (Homeomorph.symm f)),
            left_inv :=
              (_ :
                ∀ (x : ↑X),
                  ↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).2
                      (↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).1 x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑Y),
                  ↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).1
                      (↑(Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))).2 x) =
                    x) })
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f
[PROOFSTEP]
dsimp [homeoOfIso, isoOfHomeo]
[GOAL]
X Y : TopCat
f : X ≅ Y
⊢ Iso.mk
      (Homeomorph.toContinuousMap
        (Homeomorph.mk
          { toFun := ↑f.hom, invFun := ↑f.inv, left_inv := (_ : ∀ (x : ↑X), ↑f.2 (↑f.1 x) = x),
            right_inv := (_ : ∀ (x : ↑Y), ↑f.1 (↑f.2 x) = x) }))
      (Homeomorph.toContinuousMap
        (Homeomorph.symm
          (Homeomorph.mk
            { toFun := ↑f.hom, invFun := ↑f.inv, left_inv := (_ : ∀ (x : ↑X), ↑f.2 (↑f.1 x) = x),
              right_inv := (_ : ∀ (x : ↑Y), ↑f.1 (↑f.2 x) = x) }))) =
    f
[PROOFSTEP]
ext
[GOAL]
case w.w
X Y : TopCat
f : X ≅ Y
x✝ : (forget TopCat).obj X
⊢ ↑(Iso.mk
            (Homeomorph.toContinuousMap
              (Homeomorph.mk
                { toFun := ↑f.hom, invFun := ↑f.inv, left_inv := (_ : ∀ (x : ↑X), ↑f.2 (↑f.1 x) = x),
                  right_inv := (_ : ∀ (x : ↑Y), ↑f.1 (↑f.2 x) = x) }))
            (Homeomorph.toContinuousMap
              (Homeomorph.symm
                (Homeomorph.mk
                  { toFun := ↑f.hom, invFun := ↑f.inv, left_inv := (_ : ∀ (x : ↑X), ↑f.2 (↑f.1 x) = x),
                    right_inv := (_ : ∀ (x : ↑Y), ↑f.1 (↑f.2 x) = x) })))).hom
      x✝ =
    ↑f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding ↑f
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ OpenEmbedding ((forget TopCat).map (f ≫ g)) ↔ OpenEmbedding ↑f
[PROOFSTEP]
exact openEmbedding_iff_comp_isIso f g
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ↑(f ≫ g) ↔ OpenEmbedding ↑g
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ↑(f ≫ g) → OpenEmbedding ↑g
[PROOFSTEP]
intro h
[GOAL]
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ↑(f ≫ g)
⊢ OpenEmbedding ↑g
[PROOFSTEP]
convert h.comp (TopCat.homeoOfIso (asIso f).symm).openEmbedding
[GOAL]
case h.e'_5.h
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ↑(f ≫ g)
e_1✝ : (forget TopCat).obj Y = ↑Y
⊢ ↑g = ↑(f ≫ g) ∘ ↑(homeoOfIso (asIso f).symm)
[PROOFSTEP]
exact congrArg _ (IsIso.inv_hom_id_assoc f g).symm
[GOAL]
case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ↑g → OpenEmbedding ↑(f ≫ g)
[PROOFSTEP]
exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).openEmbedding
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding ↑g
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map (f ≫ g)) ↔ OpenEmbedding ↑g
[PROOFSTEP]
exact openEmbedding_iff_isIso_comp f g
