-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
inst_6 : HasZeroMorphisms.{v, u} C
h : ∀ (j : J), (T j).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (T j).mor₁ = 0
this : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃)
      (piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂))
    (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
          (Functor.map (shiftFunctor C (A := ℤ) 1)
            (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁))
          (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₂))))
    0
have h₁ : ∀ (j : J),
  Eq.{v + 1} (α :=
    (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂)
        (CategoryStruct.comp (Y :=
          piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
          (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
          (CategoryStruct.comp (Y :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
            (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
            (CategoryStruct.comp (Y :=
              Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₂))
              (Functor.map (shiftFunctor C (A := ℤ) 1)
                (Pi.lift fun (j : J) ↦ Pi.π (fun (j : J) ↦ (T j).obj₁) j ≫ (T j).mor₁))
              (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₂))))
        (Pi.π (fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) j) :
      (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) 0
        (Pi.π (fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₂) j) :
      (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₂)
Tactic: ext j