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
X Y : C
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (fst X Y) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ fst X Y
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (snd X Y) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ snd X Y
⊢ lift (fst X Y) (snd X Y) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (fst X Y) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ 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
X Y : C
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Y) (lift (fst X Y) (snd X Y)) (snd X Y) =
    𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ≫ snd 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
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ X) (X ◁ f ≫ fst X Z) (fst X Y)

Tactic:
simp [fst_def, ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Z) (X ◁ f ≫ snd X Z) (snd X Y ≫ f)

Tactic:
simp [snd_def, whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ Y) (f ▷ Z ≫ fst Y Z) (fst X Z ≫ f)

Tactic:
simp [fst_def, ← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ Z) (f ▷ Z ≫ snd Y Z) (snd X Z)

Tactic:
simp [snd_def, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y₁ ⟶ X₂) ((f ⊗ₘ g) ≫ fst X₂ Y₂) (fst X₁ Y₁ ≫ f)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y₁ ⟶ Y₂) ((f ⊗ₘ g) ≫ snd X₂ Y₂) (snd X₁ Y₁ ≫ g)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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 Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (fst Y Z) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (fst Y Z)
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (snd Y Z) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (snd Y Z)
⊢ Eq (α := V ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (lift (f ≫ h) (g ≫ k))

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 Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (fst Y Z) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (fst Y Z)

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 Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift f g ≫ (h ⊗ₘ k)) (snd Y Z) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y Z) (lift (f ≫ h) (g ≫ k)) (snd Y Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
h_fst :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (fst X Z))
    ((g ⊗ₘ g') ≫ fst X Z)
h_snd :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ Z)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (snd X Z))
    ((g ⊗ₘ g') ≫ snd X Z)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g'))
    (g ⊗ₘ g')

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (fst X Z))
    ((g ⊗ₘ g') ≫ fst X Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ Z)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X Z) (lift (fst W Y ≫ g) (snd W Y ≫ g')) (snd X Z))
    ((g ⊗ₘ g') ≫ snd X Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.hom (α_ X Y Z) ≫ fst X (tensorObj.{v, u} (𝒞 := inst) Y Z) = fst (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫ fst X Y

Tactic:
simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor,
    ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor, CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.hom (α_ X Y Z) ≫ snd X (tensorObj.{v, u} (𝒞 := inst) Y Z) ≫ fst Y Z =
    fst (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫ snd X Y

Tactic:
simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor, CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.hom (α_ X Y Z) ≫ snd X (tensorObj.{v, u} (𝒞 := inst) Y Z) ≫ snd Y Z = snd (tensorObj.{v, u} (𝒞 := inst) X Y) Z

Tactic:
simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.inv (α_ X Y Z) ≫ fst (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫ fst X Y = fst X (tensorObj.{v, u} (𝒞 := inst) Y Z)

Tactic:
simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor,
    ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor, CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.inv (α_ X Y Z) ≫ fst (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≫ snd X Y =
    snd X (tensorObj.{v, u} (𝒞 := inst) Y Z) ≫ fst Y Z

Tactic:
simp [fst_def, ← whiskerLeft_rightUnitor_assoc, -whiskerLeft_rightUnitor]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor, CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y Z : C
⊢ Iso.inv (α_ X Y Z) ≫ snd (tensorObj.{v, u} (𝒞 := inst) X Y) Z = snd X (tensorObj.{v, u} (𝒞 := inst) Y Z) ≫ snd Y Z

Tactic:
simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Iso.hom (λ_ X) = snd (tensorUnit.{v, u} C (𝒞 := inst)) X

Tactic:
simp [snd_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶ X) (Iso.hom (ρ_ X))
    (fst X (tensorUnit.{v, u} C (𝒞 := inst)))

Tactic:
simp [fst_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Iso.inv (λ_ X) ≫ fst (tensorUnit.{v, u} C (𝒞 := inst)) X = 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
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Iso.inv (λ_ X) ≫ snd (tensorUnit.{v, u} C (𝒞 := inst)) X = 𝟙 X

Tactic:
simp [snd_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (fst X (tensorUnit.{v, u} C (𝒞 := inst))))
    (𝟙 X)

Tactic:
simp [fst_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) (Iso.inv (ρ_ X) ≫ snd X (tensorUnit.{v, u} C (𝒞 := inst)))
    (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
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)))
    ((X ◁ toUnit Y ≫ Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ X)) (fst X Y ≫ Iso.inv (ρ_ X))
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ X) (X ◁ toUnit Y ≫ Iso.hom (ρ_ X)) (fst X Y)

Tactic:
rw [← cancel_mono (ρ_ X).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)))
    ((X ◁ toUnit Y ≫ Iso.hom (ρ_ X)) ≫ Iso.inv (ρ_ X)) (fst X Y ≫ Iso.inv (ρ_ X))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y)
    ((toUnit X ▷ Y ≫ Iso.hom (λ_ Y)) ≫ Iso.inv (λ_ Y)) (snd X Y ≫ Iso.inv (λ_ Y))
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Y) (toUnit X ▷ Y ≫ Iso.hom (λ_ Y)) (snd X Y)

Tactic:
rw [← cancel_mono (λ_ Y).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y)
    ((toUnit X ▷ Y ≫ Iso.hom (λ_ Y)) ≫ Iso.inv (λ_ Y)) (snd X Y ≫ Iso.inv (λ_ Y))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
g : X ⟶ Y
rw : lift f g = g ≫ Iso.inv (λ_ Y)
⊢ lift f g ≫ Iso.hom (λ_ Y) = g

Tactic:
rw [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
g : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
rw : lift f g = f ≫ Iso.inv (ρ_ Y)
⊢ lift f g ≫ Iso.hom (ρ_ Y) = f

Tactic:
rw [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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
X Y Z : C
x : Z ⟶ tensorObj.{v, u} (𝒞 := inst_1) X Y
⊢ (fun (f : (Z ⟶ X) × (Z ⟶ Y)) ↦ (lift f.1 f.2 : Z ⟶ tensorObj.{v, u} (𝒞 := inst_1) X Y))
      ((fun (f : Z ⟶ tensorObj.{v, u} (𝒞 := inst_1) X Y) ↦ (f ≫ fst X Y, f ≫ snd X Y)) x) =
    x

Tactic:
simp
-- 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
X Y Z : C
x : (Z ⟶ X) × (Z ⟶ Y)
⊢ (fun (f : Z ⟶ tensorObj.{v, u} (𝒞 := inst_1) X Y) ↦ (f ≫ fst X Y, f ≫ snd X Y))
      ((fun (f : (Z ⟶ X) × (Z ⟶ Y)) ↦ (lift f.1 f.2 : Z ⟶ tensorObj.{v, u} (𝒞 := inst_1) X Y)) x) =
    x

Tactic:
simp
-- 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
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ Y) (Iso.hom (β_ X Y) ≫ fst Y X) (snd X Y)

Tactic:
simp [fst_def, snd_def, ← BraidedCategory.braiding_naturality_left_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_left_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ X) (Iso.hom (β_ X Y) ≫ snd Y X) (fst X Y)

Tactic:
simp [fst_def, snd_def, ← BraidedCategory.braiding_naturality_right_assoc]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) Y X ⟶ X) (Iso.inv (β_ X Y) ≫ fst X Y) (snd Y X)

Tactic:
simp [fst_def, snd_def, ← BraidedCategory.braiding_inv_naturality_left_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_inv_naturality_left_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) Y X ⟶ Y) (Iso.inv (β_ X Y) ≫ snd X Y) (fst Y X)

Tactic:
simp [fst_def, snd_def, ← BraidedCategory.braiding_inv_naturality_right_assoc]

Premises used: CategoryTheory.BraidedCategory.braiding_inv_naturality_right_assoc, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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
W X Y Z : C
h_fst :
  (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst W Y =
    (fst W X ⊗ₘ fst Y Z) ≫ fst W Y
h_snd :
  (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd W Y =
    (fst W X ⊗ₘ fst Y Z) ≫ snd W Y
⊢ tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = fst W X ⊗ₘ fst Y Z

Tactic:
ext
-- 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
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst W Y =
    (fst W X ⊗ₘ fst Y Z) ≫ fst W Y

Tactic:
simp [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- 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
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd W Y =
    (fst W X ⊗ₘ fst Y Z) ≫ snd W Y

Tactic:
simp [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- 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
W X Y Z : C
h_fst :
  (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst X Z =
    (snd W X ⊗ₘ snd Y Z) ≫ fst X Z
h_snd :
  (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd X Z =
    (snd W X ⊗ₘ snd Y Z) ≫ snd X Z
⊢ tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z) = snd W X ⊗ₘ snd Y Z

Tactic:
ext
-- 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
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ fst X Z =
    (snd W X ⊗ₘ snd Y Z) ≫ fst X Z

Tactic:
simp [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- 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
W X Y Z : C
⊢ (tensorμ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W Y) (tensorObj.{v, u} (𝒞 := inst) X Z)) ≫ snd X Z =
    (snd W X ⊗ₘ snd Y Z) ≫ snd X Z

Tactic:
simp [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- 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
W X Y Z : C
h_fst :
  (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst W X =
    (fst W Y ⊗ₘ fst X Z) ≫ fst W X
h_snd :
  (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd W X =
    (fst W Y ⊗ₘ fst X Z) ≫ snd W X
⊢ tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = fst W Y ⊗ₘ fst X Z

Tactic:
ext
-- 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
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst W X =
    (fst W Y ⊗ₘ fst X Z) ≫ fst W X

Tactic:
simp [tensorδ]

Premises used: CategoryTheory.MonoidalCategory.tensorδ
-- 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
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ fst (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd W X =
    (fst W Y ⊗ₘ fst X Z) ≫ snd W X

Tactic:
simp [tensorδ]

Premises used: CategoryTheory.MonoidalCategory.tensorδ
-- 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
W X Y Z : C
h_fst :
  (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst Y Z =
    (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z
h_snd :
  (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd Y Z =
    (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z
⊢ tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z) = snd W Y ⊗ₘ snd X Z

Tactic:
ext
-- 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
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ fst Y Z =
    (snd W Y ⊗ₘ snd X Z) ≫ fst Y Z

Tactic:
simp [tensorδ]

Premises used: CategoryTheory.MonoidalCategory.tensorδ
-- 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
W X Y Z : C
⊢ (tensorδ W X Y Z ≫ snd (tensorObj.{v, u} (𝒞 := inst) W X) (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ snd Y Z =
    (snd W Y ⊗ₘ snd X Z) ≫ snd Y Z

Tactic:
simp [tensorδ]

Premises used: CategoryTheory.MonoidalCategory.tensorδ
-- 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.hom (β_ X Y)) (lift g f)

Tactic:
aesop