awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : B ⟶ A
X Y : C
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
rw :
  uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    f ▷ Y ≫ g
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (B ◁ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
        (B ◁ NatTrans.app (pre f) X))
      (NatTrans.app (ihom.ev B) X) =
    f ▷ Y ≫ g
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom B) X))
        (B ◁ NatTrans.app (pre f) X) (NatTrans.app (ihom.ev B) X)) =
    f ▷ Y ≫ g
rw₄ :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X)) (B ◁ curry g)
      (f ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X) =
    f ▷ Y ≫ g
rw₅ :
  f ▷ Y ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) X)) (A ◁ curry g)
        (NatTrans.app (ihom.ev A) X) =
    f ▷ Y ≫ g
rw₆ rw₇ : f ▷ Y ≫ g = f ▷ Y ≫ g
⊢ uncurry (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (pre f) X)) =
    uncurry (curry (f ▷ Y ≫ g))

Tactic:
rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev, CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : B ⟶ A
⊢ Eq (α := Functor.obj.{v, v, u, u} (𝟭 C) X ⟶ Functor.obj.{v, v, u, u} (ihom B) (tensorObj.{v, u} (𝒞 := inst) A X))
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (tensorLeft A ⋙ ihom A) X) (NatTrans.app (ihom.coev A) X)
      (NatTrans.app (pre f) (tensorObj.{v, u} (𝒞 := inst) A X)))
    (NatTrans.app (ihom.coev B) X ≫ Functor.map (ihom B) (f ▷ X))

Tactic:
unit_conjugateEquiv _ _ ((tensoringLeft C).map f) X

Premises used: CategoryTheory.MonoidalCategory.tensoringLeft, CategoryTheory.unit_conjugateEquiv, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X Y : C
inst_2 : Closed.{v, u} A
inst_3 : Closed.{v, u} B
f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
g : B ⟶ A
rw : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (curry (g ▷ Y ≫ uncurry f))
rw₁ :
  Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X)
    (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom A) X) (curry (uncurry f)) (NatTrans.app (pre g) X))
rw₂ rw₃ : Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (f ≫ NatTrans.app (pre g) X) (f ≫ NatTrans.app (pre g) X)
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom B) X) (curry (uncurry (f ≫ NatTrans.app (pre g) X)))
    (curry (g ▷ Y ≫ uncurry f))

Tactic:
rw [curry_uncurry, ← curry_pre_app, curry_uncurry]

Premises used: CategoryTheory.MonoidalClosed.curry_pre_app, CategoryTheory.MonoidalClosed.curry_uncurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
rw :
  Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
    ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A) : (a : tensorLeft A ⟶ tensorLeft A) → ihom A ⟶ ihom A)
        (𝟙 (Functor.obj (tensoringLeft C) A)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
    (𝟙 (ihom A) : Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A)) (pre (𝟙 A)) (𝟙 (ihom A))

Tactic:
rw [pre, Functor.map_id]

Premises used: CategoryTheory.MonoidalClosed.pre, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
⊢ Eq (α := Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
    ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A) : (a : tensorLeft A ⟶ tensorLeft A) → ihom A ⟶ ihom A)
        (𝟙 (Functor.obj (tensoringLeft C) A)) :
      Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))
    (𝟙 (ihom A) : Quiver.Hom (V := Functor.{v, v, u, u} C C) (ihom A) (ihom A))

Tactic:
apply conjugateEquiv_id

Premises used: CategoryTheory.conjugateEquiv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
inst_2 : Closed.{v, u} W
inst_3 : Closed.{v, u} X
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom X) Y ⟶ Functor.obj.{v, v, u, u} (ihom W) Z)
    (NatTrans.app (pre f) Y ≫ Functor.map (ihom W) g) (Functor.map (ihom X) g ≫ NatTrans.app (pre f) Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X_1 X' Y Y' Z : C
inst_2 : Closed.{v, u} A
inst_3 : MonoidalClosed.{v, u} C
X : Cᵒᵖ
dsimp : Functor.IsRightAdjoint.{v, v, u, u} (ihom (Opposite.unop X))
⊢ Functor.IsRightAdjoint.{v, v, u, u} (Functor.obj internalHom X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X_1 X' Y Y' Z : C
inst_2 : Closed.{v, u} A
inst_3 : MonoidalClosed.{v, u} C
X : Cᵒᵖ
⊢ Functor.IsRightAdjoint.{v, v, u, u} (ihom (Opposite.unop X))

Tactic:
infer_instance
-- 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 : tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z
⊢ Eq.{v + 1} (α := Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.obj Z)))
    (((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 : G.obj (F.obj X ⊗ F.obj Y) ⟶ Z) → Y ⟶ G.obj ((ihom (F.obj X)).obj (F.obj Z)))
        (NatTrans.app (Iso.hom (Iso.compInverseIso (Functor.Monoidal.commTensorLeft F X))) Y ≫ f :
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z) :
      Y ⟶ G.obj (Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj X)) (F.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} (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶ Z)
                  (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ F.obj Z)) :
              (a : G.obj (F.obj X ⊗ F.obj Y) ⟶ Z) → F.obj X ⊗ F.obj Y ⟶ F.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:
rfl
-- 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
⊢ 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)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x : C
inst_2 : Closed.{v, u} x
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom x) x) (id x)
    (curry (Iso.hom (ρ_ x)))

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.id, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
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
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ⟶
      z)
    (compTranspose x y z)
    (Iso.inv (α_ x (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      NatTrans.app (ihom.ev x) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev y) z)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.compTranspose, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
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
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z) ⟶
      Functor.obj.{v, v, u, u} (ihom x) z)
    (comp x y z) (curry (compTranspose x y z))

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.comp, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
a :
  uncurry
      (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫ id x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ comp x x y) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
⊢ Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫ id x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ comp x x y =
    𝟙 (Functor.obj.{v, v, u, u} (ihom x) y)

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
a :
  uncurry
      (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
          (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
⊢ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
        (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom x) y)

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
a :
  NatTrans.app (ihom.ev x) y ≫
      Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (𝟭 C) y)) ≫
        Functor.obj.{v, v, u, u} (𝟭 C) y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
⊢ uncurry
      (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) y))
          (Functor.obj.{v, v, u, u} (ihom x) y ◁ id y) (comp x y y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))

Tactic:
rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, compTranspose_eq,
    associator_inv_naturality_right_assoc, ← rightUnitor_tensor_inv_assoc,
    whisker_exchange_assoc, ← rightUnitor_inv_naturality_assoc, ← uncurry_id_eq_ev y y]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc, CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc, CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalClosed.comp_eq, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.MonoidalClosed.compTranspose_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
a :
  NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
⊢ NatTrans.app (ihom.ev x) y ≫
      Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (𝟭 C) y)) ≫
        Functor.obj.{v, v, u, u} (𝟭 C) y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))

Tactic:
simp only [Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
a :
  NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ uncurry (id y ≫ 𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))
⊢ NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ y ◁ id y ≫ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))

Tactic:
rw [← uncurry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_left
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
x y : C
inst_2 : Closed.{v, u} x
inst_3 : Closed.{v, u} y
⊢ NatTrans.app (ihom.ev x) y ≫ Iso.inv (ρ_ y) ≫ uncurry (id y ≫ 𝟙 (Functor.obj.{v, v, u, u} (ihom y) y)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom x) y))

Tactic:
simp [id_eq, uncurry_id_eq_ev]

Premises used: CategoryTheory.MonoidalClosed.id_eq, CategoryTheory.MonoidalClosed.uncurry_id_eq_ev
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (uncurry
      (Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z))
    (uncurry (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ⟶
      Functor.obj.{v, v, u, u} (ihom w) z)
    (Iso.inv
        (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
          (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z)
    (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z)

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (w ◁
        Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) w
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)))
        (w ◁ curry (compTranspose w x y) ▷ Functor.obj.{v, v, u, u} (ihom y) z) (uncurry (curry (compTranspose w y z))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (w ◁ Functor.obj.{v, v, u, u} (ihom w) x ◁ curry (compTranspose x y z)) (uncurry (curry (compTranspose w x z))))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (uncurry
      (Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
        comp w x y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ comp w y z))
    (uncurry (Functor.obj.{v, v, u, u} (ihom w) x ◁ comp x y z ≫ comp w x z))

Tactic:
simp only [uncurry_natural_left, comp_eq]

Premises used: CategoryTheory.MonoidalClosed.comp_eq, CategoryTheory.MonoidalClosed.uncurry_natural_left
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (w ◁
        Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) w
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)))
        (w ◁ curry (compTranspose w x y) ▷ Functor.obj.{v, v, u, u} (ihom y) z) (compTranspose w y z))
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (w ◁ Functor.obj.{v, v, u, u} (ihom w) x ◁ curry (compTranspose x y z)) (compTranspose w x z))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x)
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom y) z))) ⟶
      z)
    (w ◁
        Iso.inv
          (α_ (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)
            (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) w
          (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)))
        (w ◁ curry (compTranspose w x y) ▷ Functor.obj.{v, v, u, u} (ihom y) z) (uncurry (curry (compTranspose w y z))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) w
        (tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (w ◁ Functor.obj.{v, v, u, u} (ihom w) x ◁ curry (compTranspose x y z)) (uncurry (curry (compTranspose w x z))))

Tactic:
rw [uncurry_curry, uncurry_curry]

Premises used: CategoryTheory.MonoidalClosed.uncurry_curry