-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma map_shiftFunctorComm_hom_app [F.CommShift B] (X : C) (a b : B) :
    F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app (X⟦a⟧) ≫
      ((F.commShiftIso a).hom.app X)⟦b⟧' ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫
      ((F.commShiftIso b).inv.app X)⟦a⟧' ≫ (F.commShiftIso a).inv.app (X⟦b⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd C a b).inv.app X ≫ (shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (F.commShiftIso (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Tactic:
rw [Functor.map_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ F.map ((shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (F.commShiftIso (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫
        (shiftFunctorComm D a b).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Tactic:
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add a b)) X

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq : (F.commShiftIso (a + b)).hom.app X = (CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b)).hom.app X
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫
        (shiftFunctorComm D a b).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫
        ((shiftFunctorAdd' D a b (a + b) ⋯).inv.app (F.obj X) ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X)) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Tactic:
simp only [Functor.map_comp, shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc,
  ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map (((shiftFunctorAdd C a b).symm ≪≫ shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (F.commShiftIso (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫
        ((shiftFunctorAdd' D a b (a + b) ⋯).symm ≪≫ shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)

Tactic:
dsimp

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫
        ((shiftFunctorAdd' D a b (a + b) ⋯).inv.app (F.obj X) ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X)) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)