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