case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj X = ↑X
⊢ (forget TopCat).map pullback.fst =
    ↑(homeoOfIso (asIso pullback.fst)) ∘
      (forget TopCat).map (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S))
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
⊢ Embedding ((forget TopCat).map pullback.fst)
convert (homeoOfIso (asIso (pullback.fst : pullback f (𝟙 S) ⟶ _))).embedding.comp
    (pullback_map_embedding_of_embeddings (i₁ := 𝟙 X)
      f g f (𝟙 _) (homeoOfIso (Iso.refl _)).embedding H (𝟙 _) rfl (by simp))
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj X = ↑X
⊢ (forget TopCat).map pullback.fst =
    (forget TopCat).map
      (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S) ≫
        (asIso pullback.fst).hom)
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj X = ↑X
⊢ (forget TopCat).map pullback.fst =
    ↑(homeoOfIso (asIso pullback.fst)) ∘
      (forget TopCat).map (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S))
erw [← coe_comp]
no goals
case h.e'_5.h
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj X = ↑X
⊢ (forget TopCat).map pullback.fst =
    (forget TopCat).map
      (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) (_ : f ≫ 𝟙 S = f ≫ 𝟙 S) (_ : g ≫ 𝟙 S = g ≫ 𝟙 S) ≫
        (asIso pullback.fst).hom)
simp
no goals
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : Embedding ((forget TopCat).map g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S
simp