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₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ (forget TopCat).map (limit.π (cospan f g) WalkingCospan.one) =
    (forget TopCat).map g ∘ (forget TopCat).map pullback.snd
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
⊢ OpenEmbedding ((forget TopCat).map (limit.π (cospan f g) WalkingCospan.one))
convert H₂.comp (snd_openEmbedding_of_left_openEmbedding H₁ g)
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₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ (forget TopCat).map (limit.π (cospan f g) WalkingCospan.one) = (forget TopCat).map (pullback.snd ≫ g)
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₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ (forget TopCat).map (limit.π (cospan f g) WalkingCospan.one) =
    (forget TopCat).map g ∘ (forget TopCat).map pullback.snd
erw [← coe_comp]
case h.e'_5.h.e_a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ limit.π (cospan f g) WalkingCospan.one = pullback.snd ≫ g
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₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ (forget TopCat).map (limit.π (cospan f g) WalkingCospan.one) = (forget TopCat).map (pullback.snd ≫ g)
congr
no goals
case h.e'_5.h.e_a
J : Type v
inst✝ : SmallCategory J
X✝ Y✝ Z : TopCat
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : OpenEmbedding ((forget TopCat).map f)
H₂ : OpenEmbedding ((forget TopCat).map g)
e_2✝ : (forget TopCat).obj ((cospan f g).obj WalkingCospan.one) = (forget TopCat).obj S
⊢ limit.π (cospan f g) WalkingCospan.one = pullback.snd ≫ g
exact (limit.w _ WalkingCospan.Hom.inr).symm