-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
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
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)) ≫
        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))
⊢ 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)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) w
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)))
        (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) ▷
            Functor.obj.{v, v, u, u} (ihom y) z)
        (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
          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))

Tactic:
rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc