no goals
C : Type u_2
inst✝⁵ : Category C
X✝ Y✝ Z✝ : C
inst✝⁴ : HasPullbacks C
S T : C
f✝ : X✝ ⟶ T
g✝ : Y✝ ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f✝ g✝
inst✝¹ : HasPullback (f✝ ≫ i) (g✝ ≫ i)
inst✝ :
  HasPullback (diagonal i)
    (map (f✝ ≫ i) (g✝ ≫ i) i i f✝ g✝ (𝟙 S) (_ : (f✝ ≫ i) ≫ 𝟙 S = f✝ ≫ i) (_ : (g✝ ≫ i) ≫ 𝟙 S = g✝ ≫ i))
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ diagonal fst =
    (pullbackSymmetry f (Over.mk g).hom).hom ≫
      ((baseChange f).map (Over.homMk (diagonal g))).left ≫ (diagonalObjPullbackFstIso f g).inv
apply pullback.hom_ext <;> apply pullback.hom_ext <;> dsimp <;> simp