-- Module: Mathlib.CategoryTheory.Shift.Basic
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
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 ⋯ ≫
            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)))
⊢ 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)))

Tactic:
simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map,
    eqToHom_app]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.obj_μ_inv_app, CategoryTheory.Discrete.addMonoidal_associator