-- 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 (α :=
    (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₂)))))
⊢ 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₂))))
have simp : 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: simp only [Category.comp_id, Category.id_comp, map_comp, Category.assoc]