-- 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
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
        (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
        ((Equiv.symm
              ((fun (x x_1 : C) ↦
                  (Equiv.trans
                      ((fun (x : D) (x_2 : C) ↦
                          (Equiv.trans
                              (adj.toEquivalence.symm.toAdjunction.homEquiv
                                (Functor.obj.{v₂, v₂, u₂, u₂} (tensorLeft (F.obj X)) x) x_2)
                              (Adjunction.homEquiv (ihom.adjunction (F.obj X)) x (F.obj x_2)) :
                            Equiv.{v + 1, v₂ + 1} (G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (tensorLeft (F.obj X)) x) ⟶ x_2)
                              (x ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj x_2))))
                        (F.obj x) x_1)
                      (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)) :
                    ((tensorLeft (F.obj X) ⋙ G).obj (F.obj x) ⟶ x_1) ≃ (x ⟶ G.obj ((F ⋙ ihom (F.obj X)).obj x_1))))
                Y Z) :
            (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z))) → G.obj (F.obj X ⊗ F.obj Y) ⟶ Z)
          f) :
      tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
        (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
        (((Equiv.symm
                (adj.toEquivalence.symm.toAdjunction.homEquiv (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
                  Z) :
              Equiv.{v₂ + 1, v + 1} (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Z)
                (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z)) :
            (a : F.obj X ⊗ F.obj Y ⟶ F.obj Z) → G.obj (F.obj X ⊗ F.obj Y) ⟶ Z)
          (uncurry
            (((Equiv.symm (adj.homEquiv Y (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))) :
                  Equiv.{v + 1, v₂ + 1} (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))
                    (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))) :
                (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z))) → F.obj Y ⟶ (ihom (F.obj X)).obj (F.obj Z))
              f))) :
      tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
        (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
        ((Equiv.symm
              (Adjunction.homEquiv
                (adj.comp (Adjunction.comp (ihom.adjunction (F.obj X)) adj.toEquivalence.symm.toAdjunction)) Y Z) :
            (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z))) → G.obj (F.obj X ⊗ F.obj Y) ⟶ Z)
          f) :
      tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
        (NatTrans.app (Iso.inv (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y)
        (((Equiv.symm
                (adj.toEquivalence.symm.toAdjunction.homEquiv (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
                  Z) :
              Equiv.{v₂ + 1, v + 1} (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Z)
                (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z)) :
            (a : F.obj X ⊗ F.obj Y ⟶ F.obj Z) → G.obj (F.obj X ⊗ F.obj Y) ⟶ Z)
          (uncurry
            (((Equiv.symm (adj.homEquiv Y (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))) :
                  Equiv.{v + 1, v₂ + 1} (Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))
                    (F.obj Y ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z))) :
                (a : Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z))) → F.obj Y ⟶ (ihom (F.obj X)).obj (F.obj Z))
              f))) :
      tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z)

Tactic:
rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]

Premises used: CategoryTheory.Adjunction.comp_homEquiv