-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
w :
  ∀ (X : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category)
              (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
                (obj (Discrete.functor h.F) { as := m₂ : Discrete A }))
              (obj (Discrete.functor h.F) { as := m₃ : Discrete A })).obj
          X ⟶
        (obj (Discrete.functor h.F)
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
                (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ : Discrete A }
                  { as := m₃ : Discrete A }))).obj
          X)
      (NatTrans.app
        (MonoidalCategoryStruct.whiskerRight
            (Iso.hom (Iso.symm (h.add { as := m₁ : Discrete A }.as { as := m₂ : Discrete A }.as)))
            (obj (Discrete.functor h.F) { as := m₃ : Discrete A }) ≫
          Iso.hom
              (Iso.symm
                (h.add
                  (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
                      { as := m₂ : Discrete A }).as
                  { as := m₃ : Discrete A }.as)) ≫
            map (Discrete.functor h.F)
              (Iso.hom (MonoidalCategoryStruct.associator { as := m₁ } { as := m₂ } { as := m₃ })))
        X)
      (NatTrans.app
        (Iso.hom
            (MonoidalCategoryStruct.associator (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
              (obj (Discrete.functor h.F) { as := m₂ : Discrete A })
              (obj (Discrete.functor h.F) { as := m₃ : Discrete A })) ≫
          MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
              (Iso.hom (Iso.symm (h.add { as := m₂ : Discrete A }.as { as := m₃ : Discrete A }.as))) ≫
            Iso.hom
              (Iso.symm
                (h.add { as := m₁ }.as
                  (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ } { as := m₃ }).as)))
        X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := category)
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
          (obj (Discrete.functor h.F) { as := m₂ : Discrete A }))
        (obj (Discrete.functor h.F) { as := m₃ : Discrete A }) ⟶
      obj (Discrete.functor h.F)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ : Discrete A }
            { as := m₃ : Discrete A })))
    (MonoidalCategoryStruct.whiskerRight
        (Iso.hom (Iso.symm (h.add { as := m₁ : Discrete A }.as { as := m₂ : Discrete A }.as)))
        (obj (Discrete.functor h.F) { as := m₃ : Discrete A }) ≫
      Iso.hom
          (Iso.symm
            (h.add
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₁ : Discrete A }
                  { as := m₂ : Discrete A }).as
              { as := m₃ : Discrete A }.as)) ≫
        map (Discrete.functor h.F) (Iso.hom (MonoidalCategoryStruct.associator { as := m₁ } { as := m₂ } { as := m₃ })))
    (Iso.hom
        (MonoidalCategoryStruct.associator (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
          (obj (Discrete.functor h.F) { as := m₂ : Discrete A })
          (obj (Discrete.functor h.F) { as := m₃ : Discrete A })) ≫
      MonoidalCategoryStruct.whiskerLeft (obj (Discrete.functor h.F) { as := m₁ : Discrete A })
          (Iso.hom (Iso.symm (h.add { as := m₂ : Discrete A }.as { as := m₃ : Discrete A }.as))) ≫
        Iso.hom
          (Iso.symm
            (h.add { as := m₁ }.as
              (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := m₂ } { as := m₃ }).as)))

Tactic:
ext X