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
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
              (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
                NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ NatTrans.app (ihom.ev x) y) ▷
            Functor.obj.{v, v, u, u} (ihom y) z)
        (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) y) (Functor.obj.{v, v, u, u} (ihom y) z)) ≫
          NatTrans.app (ihom.ev w) y ▷ Functor.obj.{v, v, u, u} (ihom y) z ≫ NatTrans.app (ihom.ev 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
            (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))
      (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) z)) ≫
        NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) z ≫ NatTrans.app (ihom.ev 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) (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))

Tactic:
simp only [compTranspose_eq]

Premises used: 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
w x y z : C
inst_2 : Closed.{v, u} w
inst_3 : Closed.{v, u} x
inst_4 : Closed.{v, u} y
⊢ 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)) ≫
      Iso.inv
          (α_ w
            (tensorObj.{v, u} (𝒞 := inst) (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)) ≫
        (Iso.inv (α_ w (Functor.obj.{v, v, u, u} (ihom w) x) (Functor.obj.{v, v, u, u} (ihom x) y)) ≫
              NatTrans.app (ihom.ev w) x ▷ Functor.obj.{v, v, u, u} (ihom x) y ≫ NatTrans.app (ihom.ev x) y) ▷
            Functor.obj.{v, v, u, u} (ihom y) z ≫
          NatTrans.app (ihom.ev y) z)
    (Iso.inv
        (α_ w (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))) ≫
      NatTrans.app (ihom.ev w) x ▷
          tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom x) y) (Functor.obj.{v, v, u, u} (ihom 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:
simp
-- 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
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y
⊢ curry' (uncurry' g) = g

Tactic:
simp [curry', uncurry']

Premises used: CategoryTheory.MonoidalClosed.uncurry', CategoryTheory.MonoidalClosed.curry'
-- 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
f : X ⟶ Y
⊢ uncurry' (curry' f) = f

Tactic:
simp [curry', uncurry']

Premises used: CategoryTheory.MonoidalClosed.uncurry', CategoryTheory.MonoidalClosed.curry'
-- 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_1 Y' Z : C
inst_2 : Closed.{v, u} A
X Y : C
inst_3 : Closed.{v, u} X
x : X ⟶ Y
⊢ uncurry' (curry' x) = x

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_1 Y' Z : C
inst_2 : Closed.{v, u} A
X Y : C
inst_3 : Closed.{v, u} X
x : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y
⊢ curry' (uncurry' x) = x

Tactic:
simp
-- 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
f f' : X ⟶ Y
h : Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y) (curry' f) (curry' f')
⊢ f = f'

Tactic:
curryHomEquiv'.injective h

Premises used: CategoryTheory.MonoidalClosed.curryHomEquiv', Equiv.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
f f' : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y
h : uncurry' f = uncurry' f'
⊢ f = f'

Tactic:
curryHomEquiv'.symm.injective h

Premises used: CategoryTheory.MonoidalClosed.curryHomEquiv', Equiv.injective, Equiv.symm
-- 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
rw :
  Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) X) (curry (Iso.hom (ρ_ X)))
    (id X)
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) X) (curry (Iso.hom (ρ_ X) ≫ 𝟙 X))
    (id X)

Tactic:
rw [Category.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
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) (curry (Iso.hom (ρ_ X)))
    (id X)

Tactic:
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
f : X ⟶ Y
dsimp :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))
      (X ◁ curry (Iso.hom (ρ_ X) ≫ f)) (NatTrans.app (ihom.ev X) Y))
    (Iso.hom (ρ_ X) ≫ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y)) (X ◁ curry' f)
      (NatTrans.app (ihom.ev X) Y))
    (Iso.hom (ρ_ X) ≫ f)

Tactic:
dsimp [curry']

Premises used: CategoryTheory.MonoidalClosed.curry'
-- 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
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (Functor.obj.{v, v, u, u} (ihom X) Y))
      (X ◁ curry (Iso.hom (ρ_ X) ≫ f)) (NatTrans.app (ihom.ev X) Y))
    (Iso.hom (ρ_ X) ≫ f)

Tactic:
simp only [whiskerLeft_curry_ihom_ev_app]

Premises used: 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
X Y Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : X ⟶ Y
rw :
  Eq (α := Functor.obj.{v, v, u, u} (ihom Y) Z ⟶ Functor.obj.{v, v, u, u} (ihom X) Z)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
    (NatTrans.app (pre f) Z)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (Functor.obj.{v, v, u, u} (ihom Y) Z) ⟶
      Functor.obj.{v, v, u, u} (ihom X) Z)
    (curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
    (Iso.hom (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ NatTrans.app (pre f) Z)

Tactic:
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
f : X ⟶ Y
a :
  uncurry
      (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫
        curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z) =
    uncurry (NatTrans.app (pre f) Z)
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom Y) Z ⟶ Functor.obj.{v, v, u, u} (ihom X) Z)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom Y) Z)) ≫ curry' f ▷ Functor.obj.{v, v, u, u} (ihom Y) Z ≫ comp X Y Z)
    (NatTrans.app (pre f) 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
X Y Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
rw :
  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) Z))
        (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z) =
    Functor.map (ihom X) f
⊢ CategoryStruct.comp (Y :=
      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) Y ◁ curry' f) (comp X Y Z) =
    Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫ Functor.map (ihom X) f

Tactic:
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
f : Y ⟶ Z
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) Z))
          (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z)) =
    uncurry (Functor.map (ihom X) f)
⊢ 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) Z))
        (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z) =
    Functor.map (ihom X) f

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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
            (Functor.obj.{v, v, u, u} (𝟭 C) Y ◁ curry' f) (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ 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) Z))
          (Functor.obj.{v, v, u, u} (ihom X) Y ◁ curry' f) (comp X Y Z)) =
    uncurry (Functor.map (ihom X) f)

Tactic:
rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
    compTranspose_eq, associator_inv_naturality_right_assoc, whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalClosed.curry_natural_left, CategoryTheory.MonoidalClosed.comp_eq, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalClosed.uncurry_ihom_map, 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 Z : C
inst_2 : Closed.{v, u} X
inst_3 : Closed.{v, u} Y
f : Y ⟶ Z
a :
  X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y (Functor.obj.{v, v, u, u} (ihom Y) Z)) (Y ◁ curry' f)
            (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f
⊢ X ◁ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y)) ≫
      Iso.inv (α_ X (Functor.obj.{v, v, u, u} (ihom X) Y) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
        NatTrans.app (ihom.ev X) Y ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) Y) (Functor.obj.{v, v, u, u} (ihom Y) Z))
            (Functor.obj.{v, v, u, u} (𝟭 C) Y ◁ curry' f) (NatTrans.app (ihom.ev Y) Z) =
    NatTrans.app (ihom.ev X) Y ≫ f

Tactic:
dsimp
-- 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
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Z) (curry' f ≫ Functor.map (ihom X) g)
    (curry' (f ≫ g))

Tactic:
simp only [curry', ← curry_natural_right, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.curry', CategoryTheory.MonoidalClosed.curry_natural_right
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Braided
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
A : C
inst_3 : Closed.{v_1, u_1} A
⊢ Functor.IsLeftAdjoint.{v_1, v_1, u_1, u_1} (tensorRight A)

Tactic:
Functor.isLeftAdjoint_of_iso (BraidedCategory.tensorLeftIsoTensorRight A)

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Functor.isLeftAdjoint_of_iso
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Braided
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : BraidedCategory.{v_1, u_1} C
A : C
inst_3 : MonoidalClosed.{v_1, u_1} C
J : Type u_2
inst_4 : Category.{v_2, u_2} J
⊢ PreservesLimitsOfShape.{v_2, u_2, v_1, v_1, u_1, u_1} J (Functor.obj (Functor.flip MonoidalClosed.internalHom) A)

Tactic:
MonoidalClosed.internalHomAdjunction₂.preservesLimitsOfShape_flip_obj _ _

Premises used: CategoryTheory.ParametrizedAdjunction.preservesLimitsOfShape_flip_obj, CategoryTheory.MonoidalClosed.internalHomAdjunction₂
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A : C
inst_2 : Closed.{v, u} A
⊢ Functor.IsLeftAdjoint.{v, v, u, u} (Functor.obj prod.functor A)

Tactic:
Functor.isLeftAdjoint_of_iso (CartesianMonoidalCategory.tensorLeftIsoProd A)

Premises used: CategoryTheory.CartesianMonoidalCategory.tensorLeftIsoProd, CategoryTheory.Functor.isLeftAdjoint_of_iso
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
rw : Eq (α := I ⟶ A ⟹ I) (curry (snd A I)) (t.to (A ⟹ I))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))

Tactic:
rw [← curry_eq_iff]

Premises used: CategoryTheory.MonoidalClosed.curry_eq_iff
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
⊢ Eq (α := I ⟶ A ⟹ I) (curry (snd A I)) (t.to (A ⟹ I))

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))

Tactic:
have : snd A I = uncurry (t.to _) := by
      rw [← curry_eq_iff]
      apply t.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
this : Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))
rw :
  Eq (α := I ⟶ A ⟹ tensorObj.{v, u} (𝒞 := inst) A I)
    (t.to (A ⟹ I) ≫ Functor.map (ihom A) (t.to (tensorObj.{v, u} (𝒞 := inst) A I)))
    (curry (𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)))
⊢ snd A I ≫ t.to (tensorObj.{v, u} (𝒞 := inst) A I) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)

Tactic:
rw [this, ← uncurry_natural_right, ← eq_curry_iff]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_right, CategoryTheory.MonoidalClosed.eq_curry_iff
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
this : Eq (α := tensorObj.{v, u} (𝒞 := inst) A I ⟶ I) (snd A I) (uncurry (t.to (A ⟹ I)))
⊢ Eq (α := I ⟶ A ⟹ tensorObj.{v, u} (𝒞 := inst) A I)
    (t.to (A ⟹ I) ≫ Functor.map (ihom A) (t.to (tensorObj.{v, u} (𝒞 := inst) A I)))
    (curry (𝟙 (tensorObj.{v, u} (𝒞 := inst) A I)))

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
inst_3 : BraidedCategory.{v, u} C
I : C
t : IsInitial.{v, u} I
inst_4 : MonoidalClosed.{v, u} C
rw :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (I ⟹ B)) (Iso.inv (mulZero t))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (tensorUnit.{v, u} C (𝒞 := inst))) (I ◁ default)
        (Iso.hom (mulZero t) ≫ t.to B)) =
    Iso.inv (mulZero t) ≫ uncurry (𝟙 (I ⟹ B))
⊢ CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (curry (Iso.hom (mulZero t) ≫ t.to B)) = 𝟙 (I ⟹ B)

Tactic:
rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left, CategoryTheory.MonoidalClosed.curry_eq_iff, CategoryTheory.mulZero, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
inst_3 : BraidedCategory.{v, u} C
I : C
t : IsInitial.{v, u} I
inst_4 : MonoidalClosed.{v, u} C
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (I ⟹ B)) (Iso.inv (mulZero t))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) I (tensorUnit.{v, u} C (𝒞 := inst))) (I ◁ default)
        (Iso.hom (mulZero t) ≫ t.to B)) =
    Iso.inv (mulZero t) ≫ uncurry (𝟙 (I ⟹ B))

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
rw : Mono (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A I) (lift (𝟙 A) f) (Iso.hom (zeroMul t)))
⊢ Mono f

Tactic:
rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]

Premises used: CategoryTheory.zeroMul_hom, CategoryTheory.CategoryStruct.id, CategoryTheory.CartesianMonoidalCategory.lift_snd
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
⊢ Mono (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A I) (lift (𝟙 A) f) (Iso.hom (zeroMul t)))

Tactic:
mono_comp _ _

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
⊢ Mono (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) A I) (lift (𝟙 A) f) (Iso.hom (zeroMul t)))

Tactic:
exact mono_comp _ _

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
⊢ Mono f

Tactic:
haveI : Mono f := by
    rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
    exact mono_comp _ _
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
this : Mono f
⊢ IsSplitEpi f

Tactic:
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
inst_2 : Closed.{v, u} A
I : C
t : IsInitial.{v, u} I
f : A ⟶ I
this_1 : Mono f
this : IsSplitEpi f
⊢ IsIso f

Tactic:
apply isIso_of_mono_of_isSplitEpi

Premises used: CategoryTheory.isIso_of_mono_of_isSplitEpi
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B : C
inst_2 : Closed.{v, u} A
inst_3 : HasInitial.{v, u} C
f : A ⟶ initial.{v, u} C
⊢ IsIso f

Tactic:
strict_initial initialIsInitial _

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.strict_initial