Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: 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✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
this :
  (commShiftIso (G.obj ((shiftFunctor C₁ m).obj (F.obj X₁'))) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
      (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))
⊢ (commShiftIso (G.obj (F.obj ((shiftFunctor C₁' m).obj X₁'))) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((G.map ((commShiftIso F m).hom.app X₁')).app X₂) ≫
        (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (G.map ((commShiftIso F m).hom.app X₁')).app ((shiftFunctor C₂ n).obj X₂) ≫
      (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
        (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
          (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
            (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))

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

Goal state after:
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✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
this :
  (commShiftIso (G.obj ((shiftFunctor C₁ m).obj (F.obj X₁'))) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
      (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))
⊢ (commShiftIso (G.obj (F.obj ((shiftFunctor C₁' m).obj X₁'))) n).hom.app X₂ ≫
      ((commShiftIso (G.obj ((shiftFunctor C₁' m ⋙ F).obj X₁')) n).inv.app X₂ ≫
          (G.map ((commShiftIso F m).hom.app X₁')).app ((shiftFunctor C₂ n).obj X₂) ≫
            (commShiftIso (G.obj ((F ⋙ shiftFunctor C₁ m).obj X₁')) n).hom.app X₂) ≫
        (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (G.map ((commShiftIso F m).hom.app X₁')).app ((shiftFunctor C₂ n).obj X₂) ≫
      (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
        (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
          (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
            (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))