Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
inst✝⁹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁸ : AddMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : HasShift C A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift C B
inst✝² : HasShift D B
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a b : A
X : C
⊢ 𝟙 (G.obj (F.obj ((shiftFunctor C (a + b)).obj X))) ≫
      G.map
          (F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
        𝟙 (G.obj ((shiftFunctor D (a + b)).obj (F.obj X))) ≫
          (G.map ((shiftFunctorAdd D a b).hom.app (F.obj X)) ≫
              (commShiftIso G b).hom.app ((shiftFunctor D a).obj (F.obj X)) ≫
                (shiftFunctor E b).map ((commShiftIso G a).hom.app (F.obj X)) ≫
                  (shiftFunctorAdd E a b).inv.app (G.obj (F.obj X))) ≫
            𝟙 ((shiftFunctor E (a + b)).obj (G.obj (F.obj X))) =
    (F ⋙ G).map ((shiftFunctorAdd C a b).hom.app X) ≫
      (((shiftFunctor C b).associator F G).symm ≪≫
                isoWhiskerRight (commShiftIso F b) G ≪≫
                  F.associator (shiftFunctor D b) G ≪≫
                    F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm).hom.app
          ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map
            ((((shiftFunctor C a).associator F G).symm ≪≫
                    isoWhiskerRight (commShiftIso F a) G ≪≫
                      F.associator (shiftFunctor D a) G ≪≫
                        F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm).hom.app
              X) ≫
          (shiftFunctorAdd E a b).inv.app ((F ⋙ G).obj X)

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
inst✝⁹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁸ : AddMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : HasShift C A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift C B
inst✝² : HasShift D B
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a b : A
X : C
⊢ 𝟙 (G.obj (F.obj ((shiftFunctor C (a + b)).obj X))) ≫
      G.map
          (F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
        𝟙 (G.obj ((shiftFunctor D (a + b)).obj (F.obj X))) ≫
          (G.map ((shiftFunctorAdd D a b).hom.app (F.obj X)) ≫
              (commShiftIso G b).hom.app ((shiftFunctor D a).obj (F.obj X)) ≫
                (shiftFunctor E b).map ((commShiftIso G a).hom.app (F.obj X)) ≫
                  (shiftFunctorAdd E a b).inv.app (G.obj (F.obj X))) ≫
            𝟙 ((shiftFunctor E (a + b)).obj (G.obj (F.obj X))) =
    G.map (F.map ((shiftFunctorAdd C a b).hom.app X)) ≫
      (𝟙 (G.obj (F.obj ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)))) ≫
          G.map ((commShiftIso F b).hom.app ((shiftFunctor C a).obj X)) ≫
            𝟙 (G.obj ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj X)))) ≫
              (commShiftIso G b).hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
                𝟙 ((shiftFunctor E b).obj (G.obj (F.obj ((shiftFunctor C a).obj X))))) ≫
        (shiftFunctor E b).map
            (𝟙 (G.obj (F.obj ((shiftFunctor C a).obj X))) ≫
              G.map ((commShiftIso F a).hom.app X) ≫
                𝟙 (G.obj ((shiftFunctor D a).obj (F.obj X))) ≫
                  (commShiftIso G a).hom.app (F.obj X) ≫ 𝟙 ((shiftFunctor E a).obj (G.obj (F.obj X)))) ≫
          (shiftFunctorAdd E a b).inv.app (G.obj (F.obj X))