-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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))
⊢ 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)))
have 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) sorry))) (Iso.inv (diagonalObjPullbackFstIso f g)))
      (snd (fst f g) (fst f g)))
    (snd f g))
Tactic: ext