-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (Functor.map (shiftFunctor D b) (Functor.map (shiftFunctor D a) (τ.app X)) ≫
        app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X) :
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X) :
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (F₁.map (app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      app (Iso.hom (Functor.commShiftIso F₁ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₁ a)) X) ≫
          app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
    (F₁.map (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (app (Iso.hom (Functor.commShiftIso F₁ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)))
          (Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₁ a)) X))
          (Functor.map (shiftFunctor D b) (Functor.map (shiftFunctor D a) (τ.app X)) ≫
            CategoryStruct.comp (Y :=
              Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
                (F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
              (Functor.map (shiftFunctor D b) (app (Iso.inv (Functor.commShiftIso F₂ a)) X))
              (app (Iso.inv (Functor.commShiftIso F₂ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                F₂.map (Iso.inv (Iso.app (shiftFunctorAdd C a b) X)) ≫
                  F₂.map (app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
                    CategoryStruct.comp (Y :=
                      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
                        (F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
                      (app (Iso.hom (Functor.commShiftIso F₂ b))
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
                      (Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₂ a)) X) ≫
                        app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))))))
⊢ Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b))) X ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ (a + b))) X)

Tactic:
simp only [Functor.commShiftIso_add, Functor.CommShift.isoAdd_hom_app,
      ← NatTrans.naturality_2 τ ((shiftFunctorAdd C a b).app X),
      Functor.comp_obj, hb.app_shift_assoc, ha.app_shift, assoc,
      (shiftFunctor D b).map_comp_assoc]

Premises used: CategoryTheory.Functor.CommShift.isoAdd_hom_app, CategoryTheory.Functor.comp_obj, CategoryTheory.NatTrans.naturality_2, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.commShiftIso_add, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorAdd, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.CommShiftCore.app_shift, CategoryTheory.Iso.app, CategoryTheory.NatTrans.CommShiftCore.app_shift_assoc