-- 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)) ≫
      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))
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)) ≫
      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))
Tactic: rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc]