∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a''),
  CochainComplex.ShiftSequence.shiftIso C (m + n) a a'' ⋯ =
    CategoryTheory.Functor.isoWhiskerRight
        (CategoryTheory.shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) m n)
        (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a) ≪≫
      (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) m).associator
          (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n)
          (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a) ≪≫
        (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) m).isoWhiskerLeft
            (CochainComplex.ShiftSequence.shiftIso C n a a' ha') ≪≫
          CochainComplex.ShiftSequence.shiftIso C m a' a'' ha''