-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
this :
  Eq (α :=
    (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂)))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))) n)) X₂ ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁')))
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj (F.obj X₁')).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)))
      (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m))
        (F.obj X₁'))
      (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj X₁')) n)) X₂) ≫
        NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj (F.obj X₁')).obj X₂) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂)))))
rw :
  Eq (α :=
    (G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂)))
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        ((G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))).obj X₂))
      (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))) n)) X₂)
      (CategoryStruct.comp (Y := (shiftFunctor C₂ n ⋙ G.obj ((shiftFunctor C₁' m ⋙ F).obj X₁')).obj X₂)
          (NatTrans.app (Iso.inv (commShiftIso (G.obj ((shiftFunctor C₁' m ⋙ F).obj X₁')) n)) X₂)
          (NatTrans.app (G.map (NatTrans.app (Iso.hom (commShiftIso F m)) X₁'))
              (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂) ≫
            NatTrans.app (Iso.hom (commShiftIso (G.obj ((F ⋙ shiftFunctor C₁ m).obj X₁')) n)) X₂) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁'))))
    (CategoryStruct.comp (Y :=
      (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂))
      (NatTrans.app (G.map (NatTrans.app (Iso.hom (commShiftIso F m)) X₁'))
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂))
      (CategoryStruct.comp (Y :=
        obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
          ((G.obj (F.obj X₁')).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)))
        (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m))
          (F.obj X₁'))
        (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj X₁')) n)) X₂) ≫
          NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj (F.obj X₁')).obj X₂) ≫
            (↑(h.ε m n) : CatCenter D).app
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
                (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂))))))
⊢ Eq (α :=
    (G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂) ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂)))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))) n)) X₂ ≫
      CategoryStruct.comp (Y :=
        obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
          ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj X₂))
        (map (shiftFunctor D n) (NatTrans.app (G.map (NatTrans.app (Iso.hom (commShiftIso F m)) X₁')) X₂))
        (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁'))))
    (CategoryStruct.comp (Y :=
      (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂))
      (NatTrans.app (G.map (NatTrans.app (Iso.hom (commShiftIso F m)) X₁'))
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂))
      (CategoryStruct.comp (Y :=
        obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
          ((G.obj (F.obj X₁')).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)))
        (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m))
          (F.obj X₁'))
        (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj X₁')) n)) X₂) ≫
          NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj (F.obj X₁')).obj X₂) ≫
            (↑(h.ε m n) : CatCenter D).app
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
                (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂))))))

Tactic:
rw [NatTrans.shift_app (G.map ((F.commShiftIso m).hom.app X₁')) n X₂]

Premises used: CategoryTheory.Functor.map, CategoryTheory.NatTrans.shift_app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app