awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      Functor.obj (C := Center.{v₁, u₁} C) (forget C) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)))
    (ε (forget C)) (𝟙 (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ η (forget C) = 𝟙 (Functor.obj (C := Center.{v₁, u₁} C) (forget C) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
⊢ μ (forget C) X Y =
    𝟙 (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget C) X) (Functor.obj (forget C) Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
⊢ δ (forget C) X Y = 𝟙 (Functor.obj (forget C) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Center.{v₁, u₁} C
f : A ⟶ B
i : IsIso f.f
change : IsIso (isoMk f).hom
⊢ IsIso f

Tactic:
change IsIso (isoMk f).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Center.isoMk, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Center.{v₁, u₁} C
f : A ⟶ B
i : IsIso f.f
⊢ IsIso (isoMk f).hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U : C
dsimp :
  Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      Iso.hom
          (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U) ≫
        Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
          Iso.inv
              (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
                X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
    (Iso.hom
          (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U) ≫
        X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
          Iso.inv
              (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
            (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
                Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
      U ◁
        Iso.hom
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
⊢ Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) Y X).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
          U).hom =
    ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
          U).hom ≫
      U ◁
        Iso.hom
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U : C
⊢ X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      (Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
                (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
              U ◁
                  Iso.hom
                    (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
                      (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
                Iso.inv
                  (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                    (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
        Iso.hom
          (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
    X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      Iso.inv
          (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
        (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Iso.hom
              (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
            U ◁
              Iso.hom
                (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) ⟶
      Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
        (Functor.obj (ofBraided C) (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Hom.f (ε (ofBraided C)))
    (𝟙 (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Hom.f (η (ofBraided C)) =
    𝟙
      (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
        (Functor.obj (ofBraided C) (MonoidalCategoryStruct.tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Hom.f (μ (ofBraided C) X Y) =
    𝟙
      (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (Functor.obj (ofBraided C) X)
          (Functor.obj (ofBraided C) Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Hom.f (δ (ofBraided C) X Y) =
    𝟙
      (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
        (Functor.obj (ofBraided C) (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X X' Y Y' Z : C
inst_2 : Closed.{v, u} A
⊢ Functor.IsLeftAdjoint.{v, v, u, u} (tensorLeft A)

Tactic:
(ihom.adjunction A).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X X' Y Y' Z : C
inst_2 : Closed.{v, u} A
⊢ Functor.IsRightAdjoint.{v, v, u, u} (ihom A)

Tactic:
(ihom.adjunction A).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.ihom.adjunction
-- 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 ⋙ tensorLeft A) (𝟭 C)) (Adjunction.counit (adjunction A))
    (ev A)

Tactic:
rfl

Premises used: CategoryTheory.ihom.ev, rfl
-- 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) (𝟭 C) (tensorLeft A ⋙ ihom A)) (Adjunction.unit (adjunction A))
    (coev A)

Tactic:
rfl

Premises used: CategoryTheory.ihom.coev, rfl
-- 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
X Y : C
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) X) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y)
    (A ◁ Functor.map (ihom A) f ≫ NatTrans.app (ev A) Y) (NatTrans.app (ev A) X ≫ f)

Tactic:
(ev A).naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.ihom.ev
-- 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
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ Functor.obj.{v, v, u, u} (tensorLeft A ⋙ ihom A) Y) (f ≫ NatTrans.app (coev A) Y)
    (NatTrans.app (coev A) X ≫ Functor.map (ihom A) (A ◁ f))

Tactic:
(coev A).naturality f

Premises used: CategoryTheory.ihom.coev, CategoryTheory.NatTrans.naturality
-- 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
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (tensorLeft A ⋙ ihom A) B))
      (A ◁ NatTrans.app (coev A) B) (NatTrans.app (ev A) (tensorObj.{v, u} (𝒞 := inst) A B)) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) A B)

Tactic:
(ihom.adjunction A).left_triangle_components _

Premises used: CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.left_triangle_components
-- 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
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) (Functor.obj.{v, v, u, u} (ihom A) B) ⟶
      Functor.obj.{v, v, u, u} (ihom A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
    (NatTrans.app (coev A) (Functor.obj.{v, v, u, u} (ihom A) B) ≫ Functor.map (ihom A) (NatTrans.app (ev A) B) :
      Functor.obj.{v, v, u, u} (𝟭 C) (Functor.obj.{v, v, u, u} (ihom A) B) ⟶
        Functor.obj.{v, v, u, u} (ihom A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
    (𝟙 (Functor.obj.{v, v, u, u} (ihom A) B) :
      Functor.obj.{v, v, u, u} (ihom A) B ⟶ Functor.obj.{v, v, u, u} (ihom A) B)

Tactic:
Adjunction.right_triangle_components (ihom.adjunction A) _

Premises used: CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A B X X' Y Y' Z : C
inst_2 : Closed.{v, u} A
⊢ PreservesColimits.{v, v, u, u} (tensorLeft A)

Tactic:
(ihom.adjunction A).leftAdjoint_preservesColimits

Premises used: CategoryTheory.Adjunction.leftAdjoint_preservesColimits, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X)
    ((Adjunction.homEquiv (ihom.adjunction A) Y X : (a : (tensorLeft A).obj Y ⟶ X) → Y ⟶ (ihom A).obj X) f :
      Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X)
    (curry f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.curry, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
⊢ (Equiv.symm (Adjunction.homEquiv (ihom.adjunction A) Y X) : (a : Y ⟶ (ihom A).obj X) → (tensorLeft A).obj Y ⟶ X) f =
    uncurry f

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.uncurry, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X X' Y : C
inst_2 : Closed.{v, u} A
f : X ⟶ X'
g : tensorObj.{v, u} (𝒞 := inst) A X' ⟶ Y
⊢ Eq (α := X ⟶ Functor.obj.{v, v, u, u} (ihom A) Y) (curry (A ◁ f ≫ g)) (f ≫ curry g)

Tactic:
Adjunction.homEquiv_naturality_left _ _ _

Premises used: CategoryTheory.MonoidalClosed.curry, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y Y' : C
inst_2 : Closed.{v, u} A
f : tensorObj.{v, u} (𝒞 := inst) A X ⟶ Y
g : Y ⟶ Y'
⊢ Eq (α := X ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (curry (f ≫ g)) (curry f ≫ Functor.map (ihom A) g)

Tactic:
Adjunction.homEquiv_naturality_right _ _ _

Premises used: CategoryTheory.MonoidalClosed.curry, CategoryTheory.Adjunction.homEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y Y' : C
inst_2 : Closed.{v, u} A
f : X ⟶ Functor.obj.{v, v, u, u} (ihom A) Y
g : Y ⟶ Y'
⊢ uncurry (f ≫ Functor.map (ihom A) g) = uncurry f ≫ g

Tactic:
Adjunction.homEquiv_naturality_right_symm _ _ _

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.Adjunction.homEquiv_naturality_right_symm
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X X' Y : C
inst_2 : Closed.{v, u} A
f : X ⟶ X'
g : X' ⟶ Functor.obj.{v, v, u, u} (ihom A) Y
⊢ uncurry (f ≫ g) = A ◁ f ≫ uncurry g

Tactic:
Adjunction.homEquiv_naturality_left_symm _ _ _

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.Adjunction.homEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : tensorObj.{v, u} (𝒞 := inst) A X ⟶ Y
⊢ uncurry (curry f) = f

Tactic:
(Closed.adj.homEquiv _ _).left_inv f

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.MonoidalClosed.curry, CategoryTheory.Adjunction.homEquiv, CategoryTheory.Closed.adj, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : X ⟶ Functor.obj.{v, v, u, u} (ihom A) Y
⊢ curry (uncurry f) = f

Tactic:
(Closed.adj.homEquiv _ _).right_inv f

Premises used: CategoryTheory.MonoidalClosed.uncurry, Equiv.right_inv, CategoryTheory.MonoidalClosed.curry, CategoryTheory.Adjunction.homEquiv, CategoryTheory.Closed.adj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
g : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
⊢ curry f = g ↔ f = uncurry g

Tactic:
Adjunction.homEquiv_apply_eq (ihom.adjunction A) f g

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.MonoidalClosed.curry, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.homEquiv_apply_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
f : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
g : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
⊢ g = curry f ↔ uncurry g = f

Tactic:
Adjunction.eq_homEquiv_apply (ihom.adjunction A) f g

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.Adjunction.eq_homEquiv_apply, CategoryTheory.MonoidalClosed.curry, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X
⊢ uncurry g = A ◁ g ≫ NatTrans.app (ihom.ev A) X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
⊢ Eq (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X) (curry g) (NatTrans.app (ihom.coev A) Y ≫ Functor.map (ihom A) g)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.curry, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
⊢ Function.Injective.{v + 1, v + 1} (α := tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X) (β :=
    Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X) curry

Tactic:
(Closed.adj.homEquiv _ _).injective

Premises used: CategoryTheory.MonoidalClosed.curry, CategoryTheory.ihom, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.homEquiv, Equiv.injective, CategoryTheory.Closed.adj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
⊢ Function.Injective.{v + 1, v + 1} (α := Y ⟶ Functor.obj.{v, v, u, u} (ihom A) X) uncurry

Tactic:
(Closed.adj.homEquiv _ _).symm.injective

Premises used: CategoryTheory.MonoidalClosed.uncurry, CategoryTheory.ihom, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm, CategoryTheory.Closed.adj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X : C
inst_2 : Closed.{v, u} A
⊢ uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom A) X)) = NatTrans.app (ihom.ev A) X

Tactic:
simp [uncurry_eq]

Premises used: CategoryTheory.MonoidalClosed.uncurry_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X : C
inst_2 : Closed.{v, u} A
rw :
  NatTrans.app (ihom.coev A) (Functor.obj.{v, v, u, u} (𝟭 C) X) ≫
      𝟙 (Functor.obj.{v, v, u, u} (ihom A) (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X))) =
    NatTrans.app (ihom.coev A) X
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) X ⟶
      Functor.obj.{v, v, u, u} (ihom A) (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X)))
    (curry (𝟙 (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X)))) (NatTrans.app (ihom.coev A) X)

Tactic:
rw [curry_eq, (ihom A).map_id (A ⊗ _)]

Premises used: CategoryTheory.MonoidalClosed.curry_eq, CategoryTheory.Functor.map_id, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.ihom
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X : C
inst_2 : Closed.{v, u} A
⊢ NatTrans.app (ihom.coev A) (Functor.obj.{v, v, u, u} (𝟭 C) X) ≫
      𝟙 (Functor.obj.{v, v, u, u} (ihom A) (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (𝟭 C) X))) =
    NatTrans.app (ihom.coev A) X

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A X Y : C
inst_2 : Closed.{v, u} A
g : tensorObj.{v, u} (𝒞 := inst) A Y ⟶ X
⊢ 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) =
    g

Tactic:
simp [curry_eq]

Premises used: CategoryTheory.MonoidalClosed.curry_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) Y) ⟶ Y') (uncurry (Functor.map (ihom A) g))
    (NatTrans.app (ihom.ev A) Y ≫ g)

Tactic:
apply curry_injective

Premises used: CategoryTheory.MonoidalClosed.curry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
A Y Y' : C
inst_2 : Closed.{v, u} A
g : Y ⟶ Y'
a :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y ≫ g))
a₁ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (curry (NatTrans.app (ihom.ev A) Y) ≫ Functor.map (ihom A) g)
a₂ : Functor.map (ihom A) g = curry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y))) ≫ Functor.map (ihom A) g
a₃ : Functor.map (ihom A) g = 𝟙 (Functor.obj.{v, v, u, u} (ihom A) Y) ≫ Functor.map (ihom A) g
a₄ a₅ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y') (Functor.map (ihom A) g)
    (Functor.map (ihom A) g)
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom A) Y ⟶ Functor.obj.{v, v, u, u} (ihom A) Y')
    (curry (uncurry (Functor.map (ihom A) g))) (curry (NatTrans.app (ihom.ev A) Y ≫ g))

Tactic:
rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_comp]

Premises used: CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalClosed.curry_natural_right, CategoryTheory.MonoidalClosed.curry_uncurry, CategoryTheory.Category.id_comp
-- 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 : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) X)
    (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 ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X)

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

Premises used: CategoryTheory.MonoidalCategory.tensoringLeft, CategoryTheory.Functor.map, CategoryTheory.conjugateEquiv_counit
-- 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 : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) B (Functor.obj.{v, v, u, u} (ihom A) X) ⟶ X) (uncurry (NatTrans.app (pre f) X))
    (f ▷ Functor.obj.{v, v, u, u} (ihom A) X ≫ NatTrans.app (ihom.ev A) X)

Tactic:
simp [uncurry_eq]

Premises used: CategoryTheory.MonoidalClosed.uncurry_eq