-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
lemma map_comp {a b c : M} (f : ShiftedHom X Y a) (g : ShiftedHom Y Z b)
    (h : b + a = c) (F : C ⥤ D) [F.CommShift M] :
    (f.comp g h).map F = (f.map F).comp (g.map F) h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ (f.comp g h).map F = (f.map F).comp (g.map F) h

Tactic:
dsimp [comp, map]

Result:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map (f ≫ (shiftFunctor C a).map g ≫ (shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    (F.map f ≫ (F.commShiftIso a).hom.app Y) ≫
      (shiftFunctor D a).map (F.map g ≫ (F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map f ≫
      F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    F.map f ≫
      (shiftFunctor C a ⋙ F).map g ≫
        (F.commShiftIso a).hom.app ((shiftFunctor C b).obj Z) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)

Tactic:
simp only [Functor.comp_map, F.commShiftIso_add' h, Functor.CommShift.isoAdd'_hom_app,
  ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.comp_obj, comp_id, assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map (f ≫ (shiftFunctor C a).map g ≫ (shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    (F.map f ≫ (F.commShiftIso a).hom.app Y) ≫
      (shiftFunctor D a).map (F.map g ≫ (F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)

Tactic:
simp only [Functor.map_comp, assoc]

Result:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map f ≫
      F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    F.map f ≫
      (F.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map (F.map g) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map f ≫
      F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    F.map f ≫
      (F.commShiftIso a).hom.app Y ≫
        (shiftFunctor D a).map (F.map g) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)

Tactic:
erw [← NatTrans.naturality_assoc]

Result:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : C ⥤ D
inst✝ : F.CommShift M
⊢ F.map f ≫
      F.map ((shiftFunctor C a).map g) ≫ F.map ((shiftFunctorAdd' C b a c h).inv.app Z) ≫ (F.commShiftIso c).hom.app Z =
    F.map f ≫
      (shiftFunctor C a ⋙ F).map g ≫
        (F.commShiftIso a).hom.app ((shiftFunctor C b).obj Z) ≫
          (shiftFunctor D a).map ((F.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (F.obj Z)