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))) =
    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))

Tactic:
simp only [comp_id, id_comp, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, comp_obj]

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.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)) ≫
      (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)) =
    G.map (F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (commShiftIso F b).hom.app ((shiftFunctor C a).obj X)) ≫
      (commShiftIso G b).hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor E b).map (G.map ((commShiftIso F a).hom.app X) ≫ (commShiftIso G a).hom.app (F.obj X)) ≫
          (shiftFunctorAdd E a b).inv.app (G.obj (F.obj X))