-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
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_4, u_4, 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_4, v_3, u_4, u_3} 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 (α :=
    (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj (F.obj X₂') ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj (F.obj X₂') ⋙ shiftFunctor D m).obj X₁))
    (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n)) (F.obj X₂') ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (F.obj X₂')) m)) X₁))
    (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m))
        X₁ ≫
      map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂')) ≫
        Iso.inv (shiftComm ((G.obj X₁).obj (F.obj X₂')) m n) ≫
          (↑(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 X₁).obj (F.obj X₂')))))
⊢ Eq (α :=
    (shiftFunctor C₂' n ⋙
            (G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        X₂' ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj X₂' ⋙ shiftFunctor D m).obj X₁))
    (NatTrans.app
        (Iso.hom
          (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁))
            n))
        X₂' ≫
      map (shiftFunctor D n)
        (NatTrans.app (Iso.hom (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj X₂') m)) X₁))
    (NatTrans.app
        (Iso.hom
          (commShiftIso
            ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) m))
        X₁ ≫
      map (shiftFunctor D m)
          (NatTrans.app (Iso.hom (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj X₁) n)) X₂') ≫
        Iso.inv (shiftComm (((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj X₁).obj X₂') m n) ≫
          (↑(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 (whiskeringLeft C₂' C₂ D) F).obj X₁).obj X₂'))))
have dsimp : Eq (α :=
  (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
      (F.obj (obj.{v_4, v_4, u_4, u_4} (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 X₁).obj (F.obj X₂'))))
  ((𝟙
        ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
          (F.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂'))) ≫
      (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂') ≫
        𝟙
            ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
              (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) ≫
          NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n))
              (F.obj X₂') ≫
            𝟙
              (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) X₁)).obj (F.obj X₂')))) ≫
    map (shiftFunctor D n)
      (NatTrans.app (Iso.hom (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj X₂') m)) X₁))
  (CategoryStruct.comp (Y :=
    obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
      ((G.obj X₁).obj (F.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂'))))
    (NatTrans.app
      (Iso.hom
        (commShiftIso
          ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) m))
      X₁)
    (map (shiftFunctor D m)
        (𝟙 ((G.obj X₁).obj (F.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂'))) ≫
          (G.obj X₁).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂') ≫
            𝟙 ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) ≫
              NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂') ≫
                𝟙 (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.obj X₁).obj (F.obj X₂')))) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm D m n)) ((G.obj X₁).obj (F.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 X₁).obj (F.obj X₂'))))))
Tactic: dsimp [commShiftIso] at this ⊢