-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h₀ :
  Eq (α := pullback f g ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (fst (fst f g) (fst f g)) ≫
      fst f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (fst (fst f g) (fst f g)))
      (fst f g))
h₁ :
  Eq (α := pullback f g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (fst (fst f g) (fst f g)) ≫
      snd f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (fst (fst f g) (fst f g)))
      (snd f g))
h₂ :
  Eq (α := pullback f g ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (snd (fst f g) (fst f g)) ≫
      fst f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (snd (fst f g) (fst f g)))
      (fst f g))
h₃ :
  Eq (α := pullback f g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (snd (fst f g) (fst f g)) ≫
      snd f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (snd (fst f g) (fst f g)))
      (snd f g))
⊢ Eq (α := pullback f g ⟶ diagonalObj (X := pullback f g) (fst f g)) (diagonal (fst f g))
    (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
      CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
        (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯))) (Iso.inv (diagonalObjPullbackFstIso f g)))

Tactic:
ext