-- Module: Mathlib.CategoryTheory.Triangulated.Basic
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₂
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₂)
⊢ 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

Tactic:
ext j