∀ {C : Type u_1} {D : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_3} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F.CommShift A] (a b : A),
  (CategoryTheory.shiftFunctor C (a + b)).isoWhiskerLeft e.symm ≪≫
      CategoryTheory.Functor.commShiftIso F (a + b) ≪≫
        CategoryTheory.Functor.isoWhiskerRight e (CategoryTheory.shiftFunctor D (a + b)) =
    CategoryTheory.Functor.CommShift.isoAdd
      ((CategoryTheory.shiftFunctor C a).isoWhiskerLeft e.symm ≪≫
        CategoryTheory.Functor.commShiftIso F a ≪≫
          CategoryTheory.Functor.isoWhiskerRight e (CategoryTheory.shiftFunctor D a))
      ((CategoryTheory.shiftFunctor C b).isoWhiskerLeft e.symm ≪≫
        CategoryTheory.Functor.commShiftIso F b ≪≫
          CategoryTheory.Functor.isoWhiskerRight e (CategoryTheory.shiftFunctor D b))