awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ i.obj ((reflector i).obj B))
    (snd A B ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction i)) B)
    (NatTrans.app (Adjunction.unit (reflectorAdjunction i)) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ≫
      i.map ((reflector i).map (snd A B)))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.reflectorAdjunction, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
⊢ PreservesFiniteProducts (reflector i)

Tactic:
have := preservesBinaryProducts_of_exponentialIdeal i
  have : PreservesLimitsOfShape _ (reflector i) := leftAdjoint_preservesTerminal_of_reflective.{0} i
  .of_preserves_binary_and_terminal _

Premises used: CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal, CategoryTheory.leftAdjoint_preservesTerminal_of_reflective, CategoryTheory.preservesBinaryProducts_of_exponentialIdeal, CategoryTheory.reflector
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      Functor.obj.{v, v, u, u} (ihom x) z)
    (uncurry (ihomCurry x y z))
    (curry
      (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
        NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z))

Tactic:
uncurry_curry _

Premises used: CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalClosed.ihomCurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ⟶
      z)
    (uncurry (uncurry (ihomCurry x y z)))
    (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
      NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)

Tactic:
simp [uncurry_ihomCurry]

Premises used: CategoryTheory.MonoidalClosed.uncurry_ihomCurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)) ⟶
      z)
    (uncurry (ihomUncurry x y z))
    (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)

Tactic:
uncurry_curry _

Premises used: CategoryTheory.MonoidalClosed.uncurry_curry, CategoryTheory.MonoidalClosed.ihomUncurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
        (ihomUncurry x y z) (ihomCurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) (ihomUncurry x y z)
      (ihomCurry x y z) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  uncurry
      (uncurry
        (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
          (ihomUncurry x y z) (ihomCurry x y z))) =
    uncurry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))))
⊢ uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
        (ihomUncurry x y z) (ihomCurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)))
      (x ◁ y ◁ ihomUncurry x y z)
      (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
        NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z))
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
⊢ uncurry
      (uncurry
        (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)
          (ihomUncurry x y z) (ihomCurry x y z))) =
    uncurry (uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))))

Tactic:
simp only [uncurry_natural_left, uncurry_uncurry_ihomCurry, Functor.id_obj, uncurry_id_eq_ev]

Premises used: CategoryTheory.MonoidalClosed.uncurry_uncurry_ihomCurry, CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)))
      (x ◁ y ◁ ihomUncurry x y z)
      (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
        NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z))
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))

Tactic:
rw [associator_inv_naturality_right_assoc, ← dsimp% uncurry_eq, uncurry_ihomUncurry]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc, CategoryTheory.MonoidalClosed.uncurry_eq, CategoryTheory.MonoidalClosed.uncurry_ihomUncurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (Iso.inv (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
      Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) x
        (tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ⟶
      z)
    (x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z)
    (uncurry (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))
        (ihomCurry x y z) (ihomUncurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z))
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)) (ihomCurry x y z)
      (ihomUncurry x y z) =
    𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)

Tactic:
apply uncurry_injective

Premises used: CategoryTheory.MonoidalClosed.uncurry_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
⊢ uncurry
      (CategoryStruct.comp (Y := Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))
        (ihomCurry x y z) (ihomUncurry x y z)) =
    uncurry (𝟙 (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z))

Tactic:
rw [uncurry_natural_left, uncurry_id_eq_ev, uncurry_ihomUncurry]

Premises used: CategoryTheory.MonoidalClosed.uncurry_id_eq_ev, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.MonoidalClosed.uncurry_ihomUncurry
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
a :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) x (Functor.obj.{v, v, u, u} (ihom x) z))
        (x ◁
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
            (y ◁ ihomCurry x y z) (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
        (NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
      (tensorObj.{v, u} (𝒞 := inst) x y ◁ ihomCurry x y z)
      (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z))) ≫
        x ◁ NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z) ≫ NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)

Tactic:
rw [associator_naturality_right_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.associator_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
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
inst_4 : Closed.{v, u} (tensorObj.{v, u} (𝒞 := inst) x y)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) x y)
        (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z) ⟶
      z)
    (Iso.hom (α_ x y (Functor.obj.{v, v, u, u} (ihom (tensorObj.{v, u} (𝒞 := inst) x y)) z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) x (Functor.obj.{v, v, u, u} (ihom x) z))
        (x ◁
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst) y (Functor.obj.{v, v, u, u} (ihom y) (Functor.obj.{v, v, u, u} (ihom x) z)))
            (y ◁ ihomCurry x y z) (NatTrans.app (ihom.ev y) (Functor.obj.{v, v, u, u} (ihom x) z)))
        (NatTrans.app (ihom.ev x) z))
    (NatTrans.app (ihom.ev (tensorObj.{v, u} (𝒞 := inst) x y)) z)

Tactic:
simp [← dsimp% uncurry_eq, uncurry_uncurry_ihomCurry]

Premises used: CategoryTheory.MonoidalClosed.uncurry_uncurry_ihomCurry, CategoryTheory.MonoidalClosed.uncurry_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C : Type v₂
inst : Category.{v₁, v₂} C
X : Type v₁
⊢ Functor.IsLeftAdjoint (tensorLeft X)

Tactic:
⟨_, ⟨Types.tensorProductAdjunction X⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Types.tensorProductAdjunction, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
⊢ ∀ (X : Type v₁), PreservesColimits (tensorLeft X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
⊢ ∀ (X : Type v₁), PreservesColimits (tensorLeft X)

Tactic:
haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
this : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
⊢ ∀ {J : Type v₁} [inst : Category.{v₁, v₁} J], PreservesColimitsOfShape J (tensorLeft F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
this_1 : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this : PreservesColimits (tensorLeft F) := ⋯
⊢ Functor.IsLeftAdjoint (tensorLeft F)

Tactic:
have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Types
Goal:
C_1 : Type v₂
inst : Category.{v₁, v₂} C_1
C : Type v₁
inst_1 : SmallCategory C
F : C ⥤ Type v₁
this_1 : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this_2 : PreservesColimits (tensorLeft F) := ⋯
this : Functor.IsLeftAdjoint (tensorLeft F)
⊢ Closed F

Tactic:
exact Closed.mk _ (Adjunction.ofIsLeftAdjoint (tensorLeft F))

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.Closed.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ HasInitial.{v, u} C

Tactic:
haveI : HasInitial C := HasZeroObject.hasInitial
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
apply : initial.{v, u} C ≅ tensorUnit.{v, u} C (𝒞 := inst)
⊢ Unique (X ⟶ Y)

Tactic:
apply uniqueHomsetOfInitialIsoUnit _ X Y

Premises used: CategoryTheory.uniqueHomsetOfInitialIsoUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
refine_1 :
  Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C)
    (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (CategoryStruct.comp (Y := 0) default default))
    (𝟙 (initial.{v, u} C))
refine_2 :
  Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ tensorUnit.{v, u} C (𝒞 := inst))
    (CategoryStruct.comp (Y := initial.{v, u} C) (CategoryStruct.comp (Y := 0) default default) default)
    (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)))
⊢ initial.{v, u} C ≅ tensorUnit.{v, u} C (𝒞 := inst)

Tactic:
refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
⊢ Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C)
    (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) default (CategoryStruct.comp (Y := 0) default default))
    (𝟙 (initial.{v, u} C))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
this : HasInitial.{v, u} C
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ tensorUnit.{v, u} C (𝒞 := inst))
    (CategoryStruct.comp (Y := initial.{v, u} C) (CategoryStruct.comp (Y := 0) default default) default)
    (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
X Y : C
⊢ hom (α_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) =
    hom (λ_ X) ⊗ₘ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
X Y : C
⊢ hom (λ_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) =
    Iso.inv (α_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) X Y) ≫ (hom (λ_ X) ⊗ₘ 𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
X Y : C
⊢ Iso.inv (λ_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) =
    (Iso.inv (λ_ X) ⊗ₘ 𝟙 Y) ≫ hom (α_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
X Y : C
⊢ 𝟙 X ⊗ₘ Iso.inv (ρ_ Y) =
    Iso.inv (ρ_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ hom (α_ X Y (tensorUnit.{v_1, u_1} C (𝒞 := inst)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
X Y : C
⊢ Iso.inv (λ_ X) ⊗ₘ 𝟙 Y =
    Iso.inv (λ_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) X Y)

Tactic:
simp