-- 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} (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)
        (CategoryStruct.comp (Y :=
          obj.{v, v, u, u}
            (obj (shiftMonoidalFunctor C A)
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A)
                (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
                  { as := a₂ : Discrete A })
                { as := a₃ : Discrete A }))
            X)
          (NatTrans.app
            (LaxMonoidal.μ (shiftMonoidalFunctor C A)
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ } { as := a₂ }) { as := a₃ })
            X)
          (eqToHom ⋯ ≫
            NatTrans.app
                (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
                  (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₂ } { as := a₃ }))
                X ≫
              NatTrans.app
                (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ : Discrete 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 ⋯ ≫ 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)))
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)))
  (eqToHom sorry ≫
    NatTrans.app
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₂ } { as := a₃ }))
        X ≫
      NatTrans.app (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ : Discrete A } { as := a₃ : Discrete A })
        (obj.{v, v, u, u} (obj (shiftMonoidalFunctor C A) { as := a₁ : Discrete A }) X))
  (eqToHom sorry ≫
    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))
      (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₁ : Discrete A } ⋙
              obj (shiftMonoidalFunctor C A) { as := a₂ + 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)))
Tactic: erw [δ_μ_app_assoc, Category.assoc]