-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D c) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)))
    (F.map (map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X)) ≫
      ec.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)) ≫
        map (shiftFunctor D c) (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C ab c abc ⋯)) X) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ≫
        map (shiftFunctor D c)
            (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X) ≫
              eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                map (shiftFunctor D b) (ea.hom.app X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd' D a b ab hab)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D ab c abc ⋯)) (F.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc ⋯)) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        ec.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)) ≫
          map (shiftFunctor D c) (eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b c bc hbc))
                (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
              map (shiftFunctor D bc) (ea.hom.app X) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' D a bc abc ⋯)) (F.obj X))
have w : F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc sorry)) X) ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      ec.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)) ≫
        map (shiftFunctor D c) (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X)) ≫
          map (shiftFunctor D c)
              (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X) ≫
                eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                  map (shiftFunctor D b) (ea.hom.app X) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd' D a b ab hab)) (F.obj X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D ab c abc sorry)) (F.obj X) =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc sorry)) X) ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      ec.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)) ≫
        map (shiftFunctor D c) (eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D b ⋙ shiftFunctor D c) (ea.hom.app X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b c bc hbc))
                (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' D a bc abc sorry)) (F.obj X)
Tactic: rw [← NatTrans.naturality_assoc, ← this, Category.assoc, ← F.map_comp_assoc,
    shiftFunctorAdd'_assoc_hom_app a b c ab bc abc hab hbc h,
    Functor.map_comp_assoc, Category.assoc]