-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
X : C
⊢ Eq (α :=
    G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
      G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X)))
    (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      H.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (CategoryStruct.comp (Y :=
            obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X)))
            (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso H a)) X))
            (map (shiftFunctor E b) (map (shiftFunctor E a) (e.inv.app X)) ≫
              map (shiftFunctor E b) (NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X)) ≫
                NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                  G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
    (G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
      e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (map (shiftFunctor E b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            CategoryStruct.comp (Y :=
              G.obj
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
              (NatTrans.app (Iso.inv (commShiftIso G b)) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
              (G.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (OfComp.iso e a)) X)) ≫
                G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
have w : Eq (α :=
  G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
    G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X)))
  ((F ⋙ G).map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor E b)
            (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X))
              (NatTrans.app (Iso.hom (commShiftIso H a)) X)
              (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X))) ≫
          NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
            G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))
  (G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
    e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor E b)
            (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)) ≫
          NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
            G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))
Tactic: simp only [← NatTrans.naturality_assoc, ← commShiftIso_inv_naturality_assoc,
      ← Functor.map_comp_assoc]