-- 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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v, u₂, u} D C
adj : F ⊣ G
inst_4 : F.Monoidal
inst_5 : F.IsEquivalence
inst_6 : MonoidalClosed.{v₂, u₂} D
X Y Z : C
f : tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry f)
    (((adj.homEquiv Y (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)) :
          Equiv.{v₂ + 1, v + 1} (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))
            (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))) :
        (a : F.obj Y ⟶ (ihom (F.obj X)).obj (F.obj Z)) → Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        (((adj.toEquivalence.symm.toAdjunction.homEquiv (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) Z :
              Equiv.{v + 1, v₂ + 1}
                (adj.toEquivalence.symm.functor.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ adj.toEquivalence.symm.inverse.obj Z)) :
            (a : adj.toEquivalence.symm.functor.obj (F.obj X ⊗ F.obj Y) ⟶ Z) →
              F.obj X ⊗ F.obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z)
          (NatTrans.app (Iso.hom (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y ≫ f))))
have change : Eq (α := Y ⟶ ((adj.toEquivalence.symm.inverse ⋙ ihom (F.obj X)) ⋙ G).obj Z)
  ((Adjunction.homEquiv
          (Adjunction.ofNatIsoLeft
            (adj.comp (Adjunction.comp (ihom.adjunction (F.obj X)) adj.toEquivalence.symm.toAdjunction))
            (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X)))
          Y Z :
        (a : (tensorLeft X).obj Y ⟶ Z) → Y ⟶ ((adj.toEquivalence.symm.inverse ⋙ ihom (F.obj X)) ⋙ G).obj Z)
      f :
    Y ⟶ ((adj.toEquivalence.symm.inverse ⋙ ihom (F.obj X)) ⋙ G).obj Z)
  (((adj.homEquiv Y (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)) :
          Equiv.{v₂ + 1, v + 1} (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))
            (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))) :
        (a : F.obj Y ⟶ (ihom (F.obj X)).obj (F.obj Z)) → Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        (((adj.toEquivalence.symm.toAdjunction.homEquiv (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) Z :
              Equiv.{v + 1, v₂ + 1}
                (adj.toEquivalence.symm.functor.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ adj.toEquivalence.symm.inverse.obj Z)) :
            (a : adj.toEquivalence.symm.functor.obj (F.obj X ⊗ F.obj Y) ⟶ Z) →
              F.obj X ⊗ F.obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z)
          (NatTrans.app (Iso.hom (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y ≫ f))) :
    Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))
Tactic: change ((adj.comp ((ihom.adjunction (F.obj X)).comp
      adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft _).homEquiv _ _ _ = _