-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
a b : A
X : C
⊢ 𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X))) ≫
      G.map
          (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
            CategoryStruct.comp (Y :=
              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.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
              (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))) ≫
        𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))) ≫
          (G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X)) ≫
              CategoryStruct.comp (Y :=
                obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b)
                  (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
                (NatTrans.app (Iso.hom (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
                (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X)) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj X)))) ≫
            𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (a + b)) (G.obj (F.obj X))) =
    G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
      (𝟙 (G.obj (F.obj (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)))) ≫
          G.map (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            𝟙
                (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.hom (commShiftIso G b)) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
                𝟙
                  (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b)
                    (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))) ≫
        map (shiftFunctor E b)
            (𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
              G.map (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
                𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
                  NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X) ≫
                    𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (G.obj (F.obj X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj X))
have w : Eq (α :=
  G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
    obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (a + b)) (G.obj (F.obj X)))
  (CategoryStruct.comp (Y :=
    G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
    (G.map
      (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X)))
    (CategoryStruct.comp (Y :=
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
      (NatTrans.app (Iso.hom (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
      (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj 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))))
    (G.map
      (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        NatTrans.app (Iso.hom (commShiftIso F 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) (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
      (NatTrans.app (Iso.hom (commShiftIso G b)) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (map (shiftFunctor E b)
          (CategoryStruct.comp (Y := G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
            (G.map (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (G.obj (F.obj X)))))
Tactic: simp only [comp_id, id_comp, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, comp_obj]