case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map (f ≫ g)) → OpenEmbedding ((forget TopCat).map g)

case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map g) → OpenEmbedding ((forget TopCat).map (f ≫ g))
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map (f ≫ g)) ↔ OpenEmbedding ((forget TopCat).map g)
constructor
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ((forget TopCat).map (f ≫ g))
⊢ OpenEmbedding ((forget TopCat).map g)
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map (f ≫ g)) → OpenEmbedding ((forget TopCat).map g)
intro h
case h.e'_5.h
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ((forget TopCat).map (f ≫ g))
e_1✝ : (forget TopCat).obj Y = ↑Y
⊢ (forget TopCat).map g = (forget TopCat).map (f ≫ g) ∘ ↑(homeoOfIso (asIso f).symm)
case mp
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ((forget TopCat).map (f ≫ g))
⊢ OpenEmbedding ((forget TopCat).map g)
convert h.comp (TopCat.homeoOfIso (asIso f).symm).openEmbedding
no goals
case h.e'_5.h
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : OpenEmbedding ((forget TopCat).map (f ≫ g))
e_1✝ : (forget TopCat).obj Y = ↑Y
⊢ (forget TopCat).map g = (forget TopCat).map (f ≫ g) ∘ ↑(homeoOfIso (asIso f).symm)
exact congrArg _ (IsIso.inv_hom_id_assoc f g).symm
no goals
case mpr
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ OpenEmbedding ((forget TopCat).map g) → OpenEmbedding ((forget TopCat).map (f ≫ g))
exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).openEmbedding