Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  F.map ((shiftFunctor C c).map ((shiftFunctorAdd' C a b ab hab).hom.app X)) ≫
      ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor D c).map (F.map ((shiftFunctorAdd' C a b ab hab).inv.app X)) =
    ec.hom.app ((shiftFunctor C ab).obj X)
⊢ F.map ((shiftFunctorAdd' C ab c abc ⋯).hom.app X) ≫
      ec.hom.app ((shiftFunctor C ab).obj X) ≫
        (shiftFunctor D c).map
            (F.map ((shiftFunctorAdd' C a b ab hab).hom.app X) ≫
              eb.hom.app ((shiftFunctor C a).obj X) ≫
                (shiftFunctor D b).map (ea.hom.app X) ≫ (shiftFunctorAdd' D a b ab hab).inv.app (F.obj X)) ≫
          (shiftFunctorAdd' D ab c abc ⋯).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a bc abc ⋯).hom.app X) ≫
      F.map ((shiftFunctorAdd' C b c bc hbc).hom.app ((shiftFunctor C a).obj X)) ≫
        ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor D c).map (eb.hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctorAdd' D b c bc hbc).inv.app (F.obj ((shiftFunctor C a).obj X)) ≫
              (shiftFunctor D bc).map (ea.hom.app X) ≫ (shiftFunctorAdd' D a bc abc ⋯).inv.app (F.obj X)

Tactic:
rw [← NatTrans.naturality_assoc, ← this, Category.assoc, ← F.map_comp_assoc,
    shiftFunctorAdd'_assoc_hom_app a b c ab bc abc hab hbc h,
    Functor.map_comp_assoc, Category.assoc]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  F.map ((shiftFunctor C c).map ((shiftFunctorAdd' C a b ab hab).hom.app X)) ≫
      ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor D c).map (F.map ((shiftFunctorAdd' C a b ab hab).inv.app X)) =
    ec.hom.app ((shiftFunctor C ab).obj X)
⊢ F.map ((shiftFunctorAdd' C a bc abc ⋯).hom.app X) ≫
      F.map ((shiftFunctorAdd' C b c bc hbc).hom.app ((shiftFunctor C a).obj X)) ≫
        ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor D c).map (F.map ((shiftFunctorAdd' C a b ab hab).inv.app X)) ≫
            (shiftFunctor D c).map
                (F.map ((shiftFunctorAdd' C a b ab hab).hom.app X) ≫
                  eb.hom.app ((shiftFunctor C a).obj X) ≫
                    (shiftFunctor D b).map (ea.hom.app X) ≫ (shiftFunctorAdd' D a b ab hab).inv.app (F.obj X)) ≫
              (shiftFunctorAdd' D ab c abc ⋯).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a bc abc ⋯).hom.app X) ≫
      F.map ((shiftFunctorAdd' C b c bc hbc).hom.app ((shiftFunctor C a).obj X)) ≫
        ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor D c).map (eb.hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor D b ⋙ shiftFunctor D c).map (ea.hom.app X) ≫
              (shiftFunctorAdd' D b c bc hbc).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
                (shiftFunctorAdd' D a bc abc ⋯).inv.app (F.obj X)