-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
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 : Y ⟶ Functor.obj.{v, v, u, u} (ihom X) Z
change :
  Eq (α := Functor.obj.{v, v, u, u} (tensorLeft X) Y ⟶ Z)
    ((Equiv.symm
            (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 : Y ⟶ ((adj.toEquivalence.symm.inverse ⋙ ihom (F.obj X)) ⋙ G).obj Z) → (tensorLeft X).obj Y ⟶ Z)
        f :
      Functor.obj.{v, v, u, u} (tensorLeft X) Y ⟶ Z)
    (CategoryStruct.comp (Y := ((F ⋙ tensorLeft (F.obj X)) ⋙ adj.toEquivalence.inverse).obj Y)
        (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
        (((Equiv.symm (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z) :
              Equiv.{v₂ + 1, v + 1} ((F ⋙ tensorLeft (F.obj X)).obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z)
                (adj.toEquivalence.symm.functor.obj ((F ⋙ tensorLeft (F.obj X)).obj Y) ⟶ Z)) :
            (a : (F ⋙ tensorLeft (F.obj X)).obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z) →
              adj.toEquivalence.symm.functor.obj ((F ⋙ tensorLeft (F.obj X)).obj Y) ⟶ Z)
          (uncurry
            (((Equiv.symm
                    (adj.homEquiv Y
                      (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z))) :
                  Equiv.{v + 1, v₂ + 1}
                    (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z)))
                    (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z))) :
                (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))) →
                  F.obj Y ⟶ (ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))
              f))) :
      Functor.obj.{v, v, u, u} (tensorLeft X) Y ⟶ Z)
⊢ uncurry f =
    CategoryStruct.comp (Y := ((F ⋙ tensorLeft (F.obj X)) ⋙ adj.toEquivalence.inverse).obj Y)
      (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
      (((Equiv.symm (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z) :
            Equiv.{v₂ + 1, v + 1} ((F ⋙ tensorLeft (F.obj X)).obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z)
              (adj.toEquivalence.symm.functor.obj ((F ⋙ tensorLeft (F.obj X)).obj Y) ⟶ Z)) :
          (a : (F ⋙ tensorLeft (F.obj X)).obj Y ⟶ adj.toEquivalence.symm.inverse.obj Z) →
            adj.toEquivalence.symm.functor.obj ((F ⋙ tensorLeft (F.obj X)).obj Y) ⟶ Z)
        (uncurry
          (((Equiv.symm
                  (adj.homEquiv Y
                    (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z))) :
                Equiv.{v + 1, v₂ + 1}
                  (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z)))
                  (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (adj.toEquivalence.symm.inverse.obj Z))) :
              (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))) →
                F.obj Y ⟶ (ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))
            f)))

Tactic:
change (((adj.comp ((ihom.adjunction (F.obj X)).comp
      adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft _).homEquiv _ _).symm _ = _

Premises used: CategoryTheory.ihom.adjunction, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.symm, CategoryTheory.Adjunction.toEquivalence, DFunLike.coe, CategoryTheory.Adjunction.comp, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.obj, CategoryTheory.Adjunction.ofNatIsoLeft