-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
h₁ :
  Eq (α :=
    (F.obj x).X₁ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₁)
    (Hom.τ₁
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₁
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))
h₂ :
  Eq (α :=
    (F.obj x).X₂ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₂)
    (Hom.τ₂
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₂
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))
⊢ Eq (α :=
    F.obj x ⟶
      obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        x_1)
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
        comm₂₃ := ⋯ })
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        f)
have h₃ : Eq (α :=
  (F.obj x).X₃ ⟶
    (obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        x_1).X₃)
  (Hom.τ₃
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := sorry,
        comm₂₃ := sorry }))
  (Hom.τ₃
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := sorry, comm₂₃ := sorry } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        f))
Tactic: ext