∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X₁ X₂ X₃ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₂₃ : X₃ ⟶ Z₂₃}
  {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} {v₁₃ : X₃ ⟶ Z₁₃}
  {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃).mor₁
      (CategoryTheory.CategoryStruct.id X₃) =
    CategoryTheory.CategoryStruct.comp u₁₂ (CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃).mor₁