-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[simp, reassoc]
lemma map_shiftFunctorCompIsoId_hom_app [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) :
    F.map ((shiftFunctorCompIsoId C a b h).hom.app X) =
      (F.commShiftIso b).hom.app (X⟦a⟧) ≫ ((F.commShiftIso a).hom.app X)⟦b⟧' ≫
        (shiftFunctorCompIsoId D a b h).hom.app (F.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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ F.map ((shiftFunctorCompIsoId C a b h).hom.app X) =
    (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)

Tactic:
dsimp [shiftFunctorCompIsoId]

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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' h)) 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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq : (F.commShiftIso 0).hom.app X = (CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)).hom.app X
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).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 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
rw [← cancel_epi (F.map ((shiftFunctorAdd' C a b 0 h).hom.app X)), ← reassoc_of% eq, F.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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).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 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      F.map ((shiftFunctorAdd' C a b 0 h).inv.app X) ≫ F.map ((shiftFunctorZero C A).hom.app X) =
    F.map ((shiftFunctorZero C A).hom.app X) ≫
      (shiftFunctorZero D A).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).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 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      F.map ((shiftFunctorAdd' C a b 0 h).inv.app X) ≫ F.map ((shiftFunctorZero C A).hom.app X) =
    F.map ((shiftFunctorZero C A).hom.app X) ≫
      (shiftFunctorZero D A).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
simp only [Iso.inv_hom_id_app, id_obj, Category.comp_id, ← F.map_comp_assoc, Iso.hom_inv_id_app,
  F.map_id, Category.id_comp]

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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq : (F.commShiftIso 0).hom.app X = (CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)).hom.app X
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
simp only [commShiftIso_zero, comp_obj, CommShift.isoZero_hom_app,
  CommShift.isoAdd'_hom_app] 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
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).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 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).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 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)