-- 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
X Y Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₁ :
  (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.hom (ρ_ Y) ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₂ :
  (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
          NatTrans.app (ihom.ev X) Y ≫
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ Y))
              (Iso.hom (ρ_ Y) ≫ f) =
    NatTrans.app (ihom.ev X) Y ≫ f
a₃ :
  Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
      Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
          Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
            NatTrans.app (ihom.ev X) Y ≫
              CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
                (Iso.inv (ρ_ Y)) (Iso.hom (ρ_ Y) ≫ f) =
    NatTrans.app (ihom.ev X) Y ≫ f
a₄ :
  Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
      Iso.hom (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
          Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
            NatTrans.app (ihom.ev X) Y ≫ f =
    NatTrans.app (ihom.ev X) Y ≫ f
a₅ :
  CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))
        (tensorUnit.{v, u} C (𝒞 := inst)))
      (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))))
      (Iso.hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))) ≫
        NatTrans.app (ihom.ev X) Y ≫ f) =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
have a₆ : Eq (α := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y) ⟶ Z) (NatTrans.app (ihom.ev X) Y ≫ f)
  (NatTrans.app (ihom.ev X) Y ≫ f)
Tactic: rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]