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 X₁)) n).hom.app (F.obj X₂') ≫
      (shiftFunctor D n).map ((commShiftIso (G.flip.obj (F.obj X₂')) m).hom.app X₁) =
    (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj (F.obj X₂'))) m).hom.app X₁ ≫
      (shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app (F.obj X₂')) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj X₁).obj (F.obj X₂')) ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj (F.obj X₂'))))
⊢ ((((G.obj ((shiftFunctor C₁ m).obj X₁)).map ((commShiftIso F n).hom.app X₂') ≫
            (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj (F.obj X₂'))) m).hom.app X₁) ≫
          (shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app (F.obj X₂'))) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj X₁).obj (F.obj X₂'))) ≫
      (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj (F.obj X₂')))) =
    ((((commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj ((shiftFunctor C₂' n).obj X₂')) m).hom.app X₁ ≫
            (shiftFunctor D m).map ((G.obj X₁).map ((commShiftIso F n).hom.app X₂'))) ≫
          (shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app (F.obj X₂'))) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj X₁).obj (F.obj X₂'))) ≫
      (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj (F.obj X₂'))))

Tactic:
congr 3

Goal state after:
case e_a.e_a.e_a
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 X₁)) n).hom.app (F.obj X₂') ≫
      (shiftFunctor D n).map ((commShiftIso (G.flip.obj (F.obj X₂')) m).hom.app X₁) =
    (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj (F.obj X₂'))) m).hom.app X₁ ≫
      (shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app (F.obj X₂')) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj X₁).obj (F.obj X₂')) ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj (F.obj X₂'))))
⊢ (G.obj ((shiftFunctor C₁ m).obj X₁)).map ((commShiftIso F n).hom.app X₂') ≫
      (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj (F.obj X₂'))) m).hom.app X₁ =
    (commShiftIso ((G ⋙ (whiskeringLeft C₂' C₂ D).obj F).flip.obj ((shiftFunctor C₂' n).obj X₂')) m).hom.app X₁ ≫
      (shiftFunctor D m).map ((G.obj X₁).map ((commShiftIso F n).hom.app X₂'))