-- 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 : HasLimit (F ⋙ π₁)
inst_4 : HasLimit (F ⋙ π₂)
inst_5 : HasLimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
h₁ :
  Eq (α :=
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x).X₁ ⟶
      (F.obj x_1).X₁)
    (Hom.τ₁
      (Functor.map
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₁
      ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f))
h₂ :
  Eq (α :=
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x).X₂ ⟶
      (F.obj x_1).X₂)
    (Hom.τ₂
      (Functor.map
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₂
      ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f))
⊢ Eq (α :=
    obj
        (obj (const J)
          (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
            (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        x ⟶
      F.obj x_1)
    (Functor.map
        (obj (const J)
          (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
            (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        f ≫
      { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯, comm₂₃ := ⋯ })
    ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
      F.map f)
have h₃ : Eq (α :=
  (obj
        (obj (const J)
          (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
            (limMap (F.whiskerLeft π₂Toπ₃)) sorry))
        x).X₃ ⟶
    (F.obj x_1).X₃)
  (Hom.τ₃
    (Functor.map
        (obj (const J)
          (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
            (limMap (F.whiskerLeft π₂Toπ₃)) sorry))
        f ≫
      { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := sorry, comm₂₃ := sorry }))
  (Hom.τ₃
    ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := sorry, comm₂₃ := sorry } ≫
      F.map f))
Tactic: ext