-- 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₁)).map (NatTrans.app (Iso.hom (commShiftIso F n)) 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₂')))))
    ((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 ⋙ 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₁).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₂')))))
have e_a : 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 m)
      ((G.obj 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.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.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) ((G.obj X₁).map (NatTrans.app (Iso.hom (commShiftIso F n)) X₂')))
Tactic: congr 3