-- 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 (α :=
    (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₂')) ⟶
      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₂'))))
    (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₁))
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((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.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₂')) ≫
        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₂'))))))
⊢ 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₂'))))))
have simp : 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₂'))))
  (CategoryStruct.comp (Y :=
    (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₂')))
    ((G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).map (NatTrans.app (Iso.hom (commShiftIso F n)) 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 ⋙ 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₁)
    (CategoryStruct.comp (Y :=
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m)
        ((G.obj X₁).obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))))
      (map (shiftFunctor D m) ((G.obj X₁).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂')))
      (map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (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: simp only [Category.comp_id, Category.id_comp, Category.assoc, map_comp]