-- 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
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
⊢ 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)))
have 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)
Tactic: ext X