awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c X Y : C
x : X ⟶ Y
refine_1 :
  Eq (α := L.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (R.obj c) (R.obj X)) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) c Y)
    (L.map (R.obj c ◁ R.map x) ≫ δ L (R.obj c) (R.obj Y) ≫ (adj.counit.app c ⊗ₘ adj.counit.app Y))
    ((δ L (R.obj c) (R.obj X) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X)) ≫ c ◁ x)
⊢ Eq (α := (R ⋙ tensorLeft (R.obj c) ⋙ L).obj X ⟶ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) Y)
    ((R ⋙ tensorLeft (R.obj c) ⋙ L).map x ≫
      Iso.hom
        ((fun (x : C) ↦
            (Iso.symm (μIso L (R.obj c) (R.obj x)) ≪≫ asIso (adj.counit.app c ⊗ₘ adj.counit.app x) :
              (R ⋙ tensorLeft (R.obj c) ⋙ L).obj x ≅ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) x))
          Y))
    (Iso.hom
        ((fun (x : C) ↦
            (Iso.symm (μIso L (R.obj c) (R.obj x)) ≪≫ asIso (adj.counit.app c ⊗ₘ adj.counit.app x) :
              (R ⋙ tensorLeft (R.obj c) ⋙ L).obj x ≅ obj.{v_1, v_1, u_1, u_1} (tensorLeft c ⋙ 𝟭 C) x))
          X) ≫
      map (tensorLeft c ⋙ 𝟭 C) x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_2, u_2} D
inst_3 : SymmetricCategory.{v_2, u_2} D
inst_4 : MonoidalClosed.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_1, u_1} C
L : Functor.{v_2, v_1, u_2, u_1} D C
inst_6 : L.Monoidal
R : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : R.Faithful
inst_8 : R.Full
adj : L ⊣ R
c : C
⊢ 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R

Tactic:
exact NatIso.ofComponents (fun _ ↦ asIso (adj.unit.app ((ihom _).obj _)))

Premises used: CategoryTheory.asIso, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
x x_1 : Transported e
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj x) (e.inverse.obj x_1) ⟶
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) x_1 x))
    (CategoryStruct.comp (Y := e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) x x_1))
      (μ e.inverse x x_1)
      (e.inverse.map
        (Iso.hom
          ((fun (x x_2 : Transported e) ↦
              (e.functor.mapIso (β_ (e.inverse.obj x) (e.inverse.obj x_2)) :
                e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj x) (e.inverse.obj x_2)) ≅
                  e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj x_2) (e.inverse.obj x))))
            x x_1))))
    (Iso.hom (β_ (e.inverse.obj x) (e.inverse.obj x_1)) ≫ μ e.inverse x_1 x)

Tactic:
simp +instances [fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]

Premises used: CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal, CategoryTheory.Monoidal.fromInducedCoreMonoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : Transported e
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) ((e' e).inverse.obj X) ((e' e).inverse.obj Y) ⟶
      (e' e).inverse.obj (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) Y X))
    (μ (e' e).inverse X Y ≫ (e' e).inverse.map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((e' e).inverse.obj X) ((e' e).inverse.obj Y)) ≫ μ (e' e).inverse Y X)

Tactic:
simp +instances [Transported.instBraidedCategory, BraidedCategory.ofFaithful,
      fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]

Premises used: CategoryTheory.Monoidal.Transported.instBraidedCategory, CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal, CategoryTheory.Monoidal.fromInducedCoreMonoidal, CategoryTheory.BraidedCategory.ofFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
a :
  Eq (α :=
    (e' e).inverse.obj
        (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y)) ⟶
      (e' e).inverse.obj ((e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    ((e' e).inverse.map (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y))))
    ((e' e).inverse.map (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y) ⟶
      (e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y)))
    (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X)

Tactic:
apply (e' e).inverse.map_injective

Premises used: CategoryTheory.Functor.map_injective, CategoryTheory.Monoidal.equivalenceTransported, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj Y)
        (((e' e).functor ⋙ (e' e).inverse).obj X))
    (Iso.hom (β_ (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y)))
    (CategoryStruct.comp (Y := ((e' e).functor ⋙ (e' e).inverse).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ ((e' e).functor ⋙ (e' e).inverse) X Y)
      (((e' e).functor ⋙ (e' e).inverse).map (Iso.hom (β_ X Y)) ≫ δ ((e' e).functor ⋙ (e' e).inverse) Y X))

Tactic:
simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_braiding, CategoryTheory.Monoidal.equivalenceTransported, CategoryTheory.Functor.Monoidal.μ_δ, CategoryTheory.Functor.Monoidal.μ_δ_assoc, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj Y)
        (((e' e).functor ⋙ (e' e).inverse).obj X))
    (Iso.hom (β_ (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y)))
    (CategoryStruct.comp (Y := ((e' e).functor ⋙ (e' e).inverse).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ ((e' e).functor ⋙ (e' e).inverse) X Y)
      (((e' e).functor ⋙ (e' e).inverse).map (Iso.hom (β_ X Y)) ≫ δ ((e' e).functor ⋙ (e' e).inverse) Y X))

Tactic:
have : (β_ (((e' e).functor ⋙ (e' e).inverse).obj X)
        (((e' e).functor ⋙ (e' e).inverse).obj Y)).hom =
          Functor.LaxMonoidal.μ (((e' e).functor ⋙ (e' e).inverse)) X Y ≫
            ((e' e).functor ⋙ (e' e).inverse).map (β_ X Y).hom ≫
              Functor.OplaxMonoidal.δ ((e' e).functor ⋙ (e' e).inverse) Y X := by
      simp only [((e' e).functor ⋙ (e' e).inverse).map_braiding X Y,
        assoc, Functor.Monoidal.μ_δ, comp_id, Functor.Monoidal.μ_δ_assoc]
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : BraidedCategory.{v₁, u₁} C
X Y : C
this :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (((e' e).functor ⋙ (e' e).inverse).obj Y)
        (((e' e).functor ⋙ (e' e).inverse).obj X))
    (Iso.hom (β_ (((e' e).functor ⋙ (e' e).inverse).obj X) (((e' e).functor ⋙ (e' e).inverse).obj Y)))
    (CategoryStruct.comp (Y := ((e' e).functor ⋙ (e' e).inverse).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ ((e' e).functor ⋙ (e' e).inverse) X Y)
      (((e' e).functor ⋙ (e' e).inverse).map (Iso.hom (β_ X Y)) ≫ δ ((e' e).functor ⋙ (e' e).inverse) Y X))
⊢ Eq (α :=
    (e' e).inverse.obj
        (tensorObj.{v₂, u₂} (𝒞 := instCategoryTransported e) ((e' e).functor.obj X) ((e' e).functor.obj Y)) ⟶
      (e' e).inverse.obj ((e' e).functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    ((e' e).inverse.map (μ (e' e).functor X Y ≫ (e' e).functor.map (Iso.hom (β_ X Y))))
    ((e' e).inverse.map (Iso.hom (β_ ((e' e).functor.obj X) ((e' e).functor.obj Y)) ≫ μ (e' e).functor Y X))

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SemiCartesianMonoidalCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) default (toUnit X)

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.asEmptyCone, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SemiCartesianMonoidalCategory.{v, u} C
X : C
f g : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
⊢ f = g

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SemiCartesianMonoidalCategory.{v, u} C
⊢ toUnit (tensorUnit.{v, u} C (𝒞 := inst)) = 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))

Tactic:
toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SemiCartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) (f ≫ toUnit Y) (toUnit X)

Tactic:
toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X Y : C
⊢ Eq (α := tensorObj ℬ X Y ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left })
    (𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.left })

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X Y : C
⊢ Eq (α := tensorObj ℬ X Y ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (tensorHom ℬ (𝟙 X) (𝟙 Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right })
    (𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app { as := WalkingPair.right })

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := tensorObj ℬ X₁ X₂ ⟶ Functor.obj.{0, v, 0, u} (pair Z₁ Z₂) { as := WalkingPair.left : Discrete WalkingPair })
    ((tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left })
    (tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.left })

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := tensorObj ℬ X₁ X₂ ⟶ Functor.obj.{0, v, 0, u} (pair Z₁ Z₂) { as := WalkingPair.right : Discrete WalkingPair })
    ((tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right })
    (tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right })

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X Y : C
⊢ Eq (α :=
    Cone.pt (F := pair (Cone.pt (F := pair X 𝒯.cone.pt) (LimitCone.cone (ℬ X 𝒯.cone.pt))) Y)
        (LimitCone.cone (ℬ (Cone.pt (F := pair X 𝒯.cone.pt) (LimitCone.cone (ℬ X 𝒯.cone.pt))) Y)) ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((Iso.hom (BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y) ≫
        tensorHom ℬ (𝟙 X) (Iso.hom (BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt Y))))) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left })
    (tensorHom ℬ (Iso.hom (BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X 𝒯.cone.pt)))) (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X Y : C
⊢ Eq (α :=
    Cone.pt (F := pair (Cone.pt (F := pair X 𝒯.cone.pt) (LimitCone.cone (ℬ X 𝒯.cone.pt))) Y)
        (LimitCone.cone (ℬ (Cone.pt (F := pair X 𝒯.cone.pt) (LimitCone.cone (ℬ X 𝒯.cone.pt))) Y)) ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    ((Iso.hom (BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y) ≫
        tensorHom ℬ (𝟙 X) (Iso.hom (BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt Y))))) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right })
    (tensorHom ℬ (Iso.hom (BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X 𝒯.cone.pt)))) (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ Iso.hom (BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt X₂))) =
    Iso.hom (BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt X₁))) ≫ f

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ Iso.hom (BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X₂ 𝒯.cone.pt))) =
    Iso.hom (BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X₁ 𝒯.cone.pt))) ≫ f

Tactic:
simp [tensorHom]

Premises used: CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct.{v, u} C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun (X : C) {x x_2 : C} (g : x ⟶ x_2) ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_2 : C} (f : x ⟶ x_2) (Y : C) ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂ : C} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun (X : C) ↦ BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt X)),
    rightUnitor := fun (X : C) ↦ BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X 𝒯.cone.pt)) }
x : C
x_1 : x ⟶ tensorUnit.{v, u} C (𝒞 := inst)
⊢ ∀ (j : Discrete PEmpty.{1}),
    x_1 ≫ 𝒯.cone.π.app j =
      (fun (x : C) ↦ (𝒯.isLimit.lift (asEmptyCone x) : Cone.pt.{0, v, 0, u} (asEmptyCone x) ⟶ 𝒯.cone.pt)) x ≫
        𝒯.cone.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct.{v, u} C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun (X : C) {x x_1 : C} (g : x ⟶ x_1) ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_1 : C} (f : x ⟶ x_1) (Y : C) ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂ : C} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun (X : C) ↦ BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt X)),
    rightUnitor := fun (X : C) ↦ BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X 𝒯.cone.pt)) }
X Y T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).pt
hf : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).fst = f
hg : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).snd = g
⊢ m ≫ BinaryFan.fst (ℬ X Y).cone =
    (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ (↑(BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g) : T ⟶ (ℬ X Y).cone.pt)) f g ≫
      BinaryFan.fst (ℬ X Y).cone

Tactic:
simpa using hf
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
𝒯 : LimitCone.{0, 0, v, u} (Functor.empty C)
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct.{v, u} C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun (X : C) {x x_1 : C} (g : x ⟶ x_1) ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_1 : C} (f : x ⟶ x_1) (Y : C) ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂ : C} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun (X : C) ↦ BinaryFan.leftUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ 𝒯.cone.pt X)),
    rightUnitor := fun (X : C) ↦ BinaryFan.rightUnitor 𝒯.isLimit (LimitCone.isLimit (ℬ X 𝒯.cone.pt)) }
X Y T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).pt
hf : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).fst = f
hg : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).snd = g
⊢ m ≫ BinaryFan.snd (ℬ X Y).cone =
    (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ (↑(BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g) : T ⟶ (ℬ X Y).cone.pt)) f g ≫
      BinaryFan.snd (ℬ X Y).cone

Tactic:
simpa using hg
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift f g) (fst X Y) = f

Tactic:
(BinaryFan.IsLimit.lift' (tensorProductIsBinaryProduct X Y) f g).2.1

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.left, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, Subtype.property
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift f g) (snd X Y) = g

Tactic:
(BinaryFan.IsLimit.lift' (tensorProductIsBinaryProduct X Y) f g).2.2

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.Limits.BinaryFan.IsLimit.lift', And.right, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, Subtype.property
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_3 : Mono f
⊢ Mono (Y := tensorObj.{v, u} (𝒞 := inst_1) X Y) (lift f g)

Tactic:
mono_of_mono_fac <| lift_fst _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_3 : Mono g
⊢ Mono (Y := tensorObj.{v, u} (𝒞 := inst_1) X Y) (lift f g)

Tactic:
mono_of_mono_fac <| lift_snd _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
T X Y : C
f g : T ⟶ tensorObj.{v, u} (𝒞 := inst) X Y
h_fst : f ≫ fst X Y = g ≫ fst X Y
h_snd : f ≫ snd X Y = g ≫ snd X Y
⊢ f = g

Tactic:
BinaryFan.IsLimit.hom_ext (tensorProductIsBinaryProduct X Y) h_fst h_snd

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (fst X Y) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (fst X Y)
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (snd X Y) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (snd X Y)
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (lift (f ≫ g) (f ≫ h))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (fst X Y) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (fst X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (f ≫ lift g h) (snd X Y) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (f ≫ g) (f ≫ h)) (snd X Y)

Tactic:
simp