-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₁ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₂ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₃ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    𝟙 ((F.shift a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₄ rw₅ :
  Eq (α := (shiftFunctor C n ⋙ F.shift a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ⟶ (F.shift a'').obj X)
    (NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X)
    (NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X)
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X

Tactic:
rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]

Premises used: CategoryTheory.Functor.shiftIso_add'_hom_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp