∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_3} A] (F : CategoryTheory.Functor C A) (M : Type u_5) [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''),
  ((CategoryTheory.shiftFunctor C (m + n)).associator (CategoryTheory.shiftFunctor C a) F).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C (m + n) a a'' ⋯).symm F =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n)
        ((CategoryTheory.shiftFunctor C a).comp F) ≪≫
      (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n)
          ((CategoryTheory.shiftFunctor C a).comp F) ≪≫
        (CategoryTheory.shiftFunctor C m).isoWhiskerLeft
            (((CategoryTheory.shiftFunctor C n).associator (CategoryTheory.shiftFunctor C a) F).symm ≪≫
              CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C n a a' ha').symm F) ≪≫
          ((CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C a') F).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C m a' a'' ha'').symm F