awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ Eq (α := T ⟶ tensorObj.{v, u} (𝒞 := inst) Y X) (lift f g ≫ Iso.inv (β_ Y X)) (lift g f)

Tactic:
aesop
-- 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
inst_3 : BraidedCategory.{v, u} C
⊢ Nonempty (BraidedCategory.{v, u} C)

Tactic:
⟨.ofCartesianMonoidalCategory⟩

Premises used: Nonempty.intro, CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
e_braiding : e₁ = e₂
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := @b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ : BraidedCategory.{v, u} C } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := @b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }

Tactic:
congr
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
e_braiding : ∀ (x x_1 : C), (e₁ x x_1).hom ≫ fst x_1 x = (e₂ x x_1).hom ≫ fst x_1 x
e_braiding₁ : ∀ (x x_1 : C), (e₁ x x_1).hom ≫ snd x_1 x = (e₂ x x_1).hom ≫ snd x_1 x
⊢ e₁ = e₂

Tactic:
ext
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
x x_1 : C
⊢ (e₁ x x_1).hom ≫ fst x_1 x = (e₂ x x_1).hom ≫ fst x_1 x

Tactic:
(@braiding_hom_fst C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_fst C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

Premises used: CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst, Eq.trans
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
x x_1 : C
⊢ (e₁ x x_1).hom ≫ fst x_1 x = (e₂ x x_1).hom ≫ fst x_1 x

Tactic:
exact (@braiding_hom_fst C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_fst C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

Premises used: CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst, Eq.trans
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
x x_1 : C
⊢ (e₁ x x_1).hom ≫ snd x_1 x = (e₂ x x_1).hom ≫ snd x_1 x

Tactic:
(@braiding_hom_snd C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_snd C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

Premises used: CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd, Eq.trans
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
x x_1 : C
⊢ (e₁ x x_1).hom ≫ snd x_1 x = (e₂ x x_1).hom ≫ snd x_1 x

Tactic:
exact (@braiding_hom_snd C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_snd C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

Premises used: CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd, Eq.trans
-- 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
inst_3 toBraidedCategory : BraidedCategory.{v, u} C
symmetry : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
toBraidedCategory_1 : BraidedCategory.{v, u} C
symmetry_1 : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
e_toBraidedCategory : toBraidedCategory = toBraidedCategory_1
⊢ { toBraidedCategory := toBraidedCategory, symmetry := symmetry : SymmetricCategory.{v, u} C } =
    { toBraidedCategory := toBraidedCategory_1, symmetry := symmetry_1 }

Tactic:
congr
-- 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
inst_3 toBraidedCategory : BraidedCategory.{v, u} C
symmetry : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
toBraidedCategory_1 : BraidedCategory.{v, u} C
symmetry_1 : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
⊢ toBraidedCategory = toBraidedCategory_1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
inst_3 toBraidedCategory : BraidedCategory.{v, u} C
symmetry : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
toBraidedCategory_1 : BraidedCategory.{v, u} C
symmetry_1 : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
⊢ toBraidedCategory = toBraidedCategory_1

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
⊢ HasFiniteProducts.{v, u} C

Tactic:
letI : ∀ (X Y : C), Limits.HasLimit (Limits.pair X Y) := fun _ _ =>
    .mk ⟨_, tensorProductIsBinaryProduct _ _⟩
  letI : Limits.HasBinaryProducts C := Limits.hasBinaryProducts_of_hasLimit_pair _
  letI : Limits.HasTerminal C := Limits.hasTerminal_of_unique (𝟙_ C)
  hasFiniteProducts_of_has_binary_and_terminal

Premises used: CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A : C
⊢ Eq (α := F.obj A ⟶ tensorUnit.{v₁, u₁} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (F.map (toUnit A)) (terminalComparison F))
    (toUnit (F.obj A))

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 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
inst_4 :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_2)) (terminalComparison F)
apply : IsLimit (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst))))
⊢ PreservesLimit (Functor.empty C) F

Tactic:
apply preservesLimit_of_preserves_limit_cone isTerminalTensorUnit

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
inst_4 :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_2)) (terminalComparison F)
hi :
  Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} D (𝒞 := inst_2))) ≅
    (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst)))).pt
⊢ IsLimit (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst))))

Tactic:
apply isLimitChangeEmptyCone D isTerminalTensorUnit

Premises used: CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
inst_4 :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_2)) (terminalComparison F)
⊢ Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} D (𝒞 := inst_2))) ≅
    (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst)))).pt

Tactic:
exact asIso (terminalComparison F) |>.symm

Premises used: CategoryTheory.CartesianMonoidalCategory.terminalComparison, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
inst_4 : PreservesLimit (Functor.empty C) F
⊢ Eq (α := F.obj (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ tensorUnit.{v₁, u₁} D (𝒞 := inst_2))
    (Iso.hom (preservesTerminalIso F)) (terminalComparison F)

Tactic:
toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_7 : PreservesLimit (Functor.empty C) F
rw :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst_1))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_3))
    (Iso.hom (preservesTerminalIso F))
⊢ IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst_1))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_3))
    (terminalComparison F)

Tactic:
rw [← preservesTerminalIso_hom]

Premises used: CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_hom
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_7 : PreservesLimit (Functor.empty C) F
⊢ IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst_1))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_3))
    (Iso.hom (preservesTerminalIso F))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (prodComparison F A B)
      (fst (F.obj A) (F.obj B)))
    (F.map (fst A B))

Tactic:
lift_fst _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (prodComparison F A B)
      (snd (F.obj A) (F.obj B)))
    (F.map (snd A B))

Tactic:
lift_snd _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (prodComparison F A B)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (inv (prodComparison F A B)) (F.map (fst A B)))
    (fst (F.obj A) (F.obj B))

Tactic:
simp [IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (prodComparison F A B)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (inv (prodComparison F A B)) (F.map (snd A B)))
    (snd (F.obj A) (F.obj B))

Tactic:
simp [IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
h_fst :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (fst (F.obj A') (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) (fst (F.obj A') (F.obj B')))
h_snd :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (snd (F.obj A') (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) (snd (F.obj A') (F.obj B')))
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))

Tactic:
apply hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (fst (F.obj A') (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) (fst (F.obj A') (F.obj B')))

Tactic:
simp only [Category.assoc, prodComparison_fst, tensorHom_fst, prodComparison_fst_assoc,
    prodComparison_snd, tensorHom_snd, prodComparison_snd_assoc, ← F.map_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc, CategoryTheory.Functor.map_comp