-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    ((eqToHom ⋯ ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
have w : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + a₃ : Discrete A }) X ⟶
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
      (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X)))
  (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ : Discrete A }) X))
      (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }) X :
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + a₃ : Discrete A }) X ⟶
          obj.{v, v, u, u}
            (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ : Discrete A } ⋙
              obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
            X)
      (map (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
          (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }) X) :
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
            (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ : Discrete A }) X) ⟶
          obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
            (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ : Discrete A })
              (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))) :
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + a₃ : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X)))
  (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ + a₃ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))
      (eqToHom sorry ≫ NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }) X :
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + a₃ : Discrete A }) X ⟶
          obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ + a₃ : Discrete A })
            (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))
      (NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X) :
        obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ + a₃ : Discrete A })
            (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X) ⟶
          obj.{v, v, u, u}
            (obj (shiftMonoidalFunctor C A) { as := a₂ : Discrete A } ⋙
              obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
            (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X)) :
    obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ + a₂ + a₃ : Discrete A }) X ⟶
      obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₃ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₂ : Discrete A })
          (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X)))
Tactic: dsimp [shiftFunctorAdd, shiftFunctor]