-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem ofEquiv_curry_def {X Y Z : C} (f : X ⊗ Y ⟶ Z) :
    letI := ofEquiv F adj
    MonoidalClosed.curry f =
      adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))
        (MonoidalClosed.curry (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z
        ((Iso.compInverseIso (H := adj.toEquivalence)
          (Functor.Monoidal.commTensorLeft F X)).hom.app Y ≫ f)))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 =>
          ((fun x x_2 =>
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm) f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ curry f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

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

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ (((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft
            (Functor.Monoidal.commTensorLeft F X).compInverseIso).homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm) f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

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

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 =>
          ((fun x x_2 =>
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm) f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ (((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft
            (Functor.Monoidal.commTensorLeft F X).compInverseIso).homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
dsimp only [Adjunction.ofNatIsoLeft]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((Adjunction.mkOfHomEquiv
            {
              homEquiv := fun X_1 Y =>
                (Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm).trans
                  ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv X_1 Y),
              homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }).homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((Adjunction.mkOfHomEquiv
            {
              homEquiv := fun X_1 Y =>
                (Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm).trans
                  ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv X_1 Y),
              homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }).homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
rw [Adjunction.mkOfHomEquiv_homEquiv]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ({
            homEquiv := fun X_1 Y =>
              (Adjunction.equivHomsetLeftOfNatIso (Functor.Monoidal.commTensorLeft F X).compInverseIso.symm).trans
                ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv X_1 Y),
            homEquiv_naturality_left_symm := ⋯, homEquiv_naturality_right := ⋯ }.homEquiv
        Y Z)
      f =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))