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

Tactic:
simp only [comp_obj, CommShift.isoAdd_hom_app,
  ← cancel_epi (F.map ((shiftFunctorAdd C a b).inv.app X)), Category.assoc,
  ← F.map_comp_assoc, Iso.inv_hom_id_app, F.map_id, Category.id_comp, F.map_comp] at eq

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) ≫
        (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 ((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)

Tactic:
simp only [NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' (add_comm b a))) X,
  CommShift.isoAdd'_hom_app, Category.assoc, Iso.inv_hom_id_app_assoc,
  ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
  Functor.map_id, Category.id_comp, comp_obj, Category.comp_id]

Result:
no goals

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) ≫
        (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:
simp only [shiftFunctorComm_eq D 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 ((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)

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

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