-- 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_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 (α :=
    (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj X₂ ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj X₂ ⋙ shiftFunctor D m).obj (F.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₁')))
    (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₂) ≫
        Iso.inv (shiftComm ((G.obj (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 (F.obj X₁')).obj X₂))))
⊢ Eq (α :=
    (shiftFunctor C₂ n ⋙ (F ⋙ G).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁')).obj X₂ ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) (((F ⋙ G).flip.obj X₂ ⋙ shiftFunctor D m).obj X₁'))
    (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁')) n)) X₂ ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).flip.obj X₂) m)) X₁'))
    (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m)) X₁' ≫
      map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).obj X₁') n)) X₂) ≫
        Iso.inv (shiftComm (((F ⋙ G).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) (((F ⋙ G).obj X₁').obj X₂))))
have dsimp : 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₂ ≫
    map (shiftFunctor D n)
      (𝟙 ((G.obj (F.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁'))).obj X₂) ≫
        NatTrans.app (G.map (NatTrans.app (Iso.hom (commShiftIso F m)) X₁')) X₂ ≫
          𝟙 ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj X₂) ≫
            NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁') ≫
              𝟙 (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂))))
  ((𝟙
        ((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₂)) ≫
      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₂) ≫
        𝟙
            ((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 (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m))
              (F.obj X₁') ≫
            𝟙
              (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₂)))) ≫
    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: dsimp [commShiftIso] at this ⊢