-- 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 :
          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 ⋯ ≫ 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)))
  (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 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))) :
    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: simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map,
    eqToHom_app]