∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X.mor₂)
          (n.negOnePow •
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.mor₃)
              ((CategoryTheory.shiftFunctorComm C 1 n).hom.app X.obj₁))).mor₂
      ((CategoryTheory.shiftFunctor C n).map f.hom₃) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map f.hom₂)
      (CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y.mor₂)
          (n.negOnePow •
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map Y.mor₃)
              ((CategoryTheory.shiftFunctorComm C 1 n).hom.app Y.obj₁))).mor₂