-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (w ◁
        Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      Iso.inv
          (α_ w
            (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y))
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) w (Functor.obj.{v, v, u, u} (ihom w) y))
              (w ◁
                curry
                  (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
                    NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ NatTrans.app (ihom.ev x) y))
              (NatTrans.app (ihom.ev w) y) ▷
            Functor.obj.{v, v, u, u} (ihom y) z ≫
          NatTrans.app (ihom.ev y) z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (w ◁
        Functor.obj.{v, v, u, u} (ihom w) x ◁
          curry
            (Iso.inv (α_ x (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
              NatTrans.app (ihom.ev x) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev y) z))
      (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)) ≫
        NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) z ≫ NatTrans.app (ihom.ev x) z))
have a : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) w
      (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
    z)
  (w ◁
      Iso.inv
        (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
    Iso.inv
        (α_ w (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y))
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
            NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ NatTrans.app (ihom.ev x) y) ▷
          Functor.obj.{v, v, u, u} (ihom y) z ≫
        NatTrans.app (ihom.ev y) z)
  (Iso.inv
      (α_ w (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ≫
    NatTrans.app (ihom.ev w) x ▷
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z) ≫
      Iso.inv (α_ x (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        NatTrans.app (ihom.ev x) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev y) z)
Tactic: rw [← uncurry_eq, uncurry_curry, associator_inv_naturality_right_assoc, whisker_exchange_assoc,
    ← uncurry_eq, uncurry_curry]