awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
slice_rhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) (((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W ≫ (μ ⊗ₘ μ))

Tactic:
slice_rhs 1 2 => rw [tensorμ_natural]

Premises used: CategoryTheory.MonoidalCategory.tensorμ_natural
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
a : ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)
| (μ ⊗ₘ μ) ≫ (f ⊗ₘ g)

Tactic:
rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    (tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))

Tactic:
slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    (tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)) ((tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)) ≫ (μ ⊗ₘ μ))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : Y ⟶ Z
inst_10 : IsMonHom f
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (η ≫ X ◁ f) η

Tactic:
simpa using ((inferInstance : IsMonHom (𝟙 X ⊗ₘ f))).one_hom

Premises used: CategoryTheory.IsMonHom.one_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : Y ⟶ Z
inst_10 : IsMonHom f
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X Z)
    (μ ≫ X ◁ f) ((X ◁ f ⊗ₘ X ◁ f) ≫ μ)

Tactic:
simpa using ((inferInstance : IsMonHom (𝟙 X ⊗ₘ f))).mul_hom

Premises used: CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
inst_10 : IsMonHom f
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) (η ≫ f ▷ Z) η

Tactic:
simpa using ((inferInstance : IsMonHom (f ⊗ₘ (𝟙 Z)))).one_hom

Premises used: CategoryTheory.IsMonHom.one_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
f : X ⟶ Y
inst_10 : IsMonHom f
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
    (μ ≫ f ▷ Z) ((f ▷ Z ⊗ₘ f ▷ Z) ≫ μ)

Tactic:
simpa using ((inferInstance : IsMonHom (f ⊗ₘ (𝟙 Z)))).mul_hom

Premises used: CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
⊢ IsMonHom.{v₁, u₁} (M := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) (Iso.hom (α_ X Y Z))

Tactic:
⟨one_associator, mul_associator⟩

Premises used: CategoryTheory.IsMonHom.mk, CategoryTheory.MonObj.mul_associator, CategoryTheory.MonObj.one_associator
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
⊢ IsMonHom.{v₁, u₁} (M := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.hom (λ_ X))

Tactic:
⟨one_leftUnitor, mul_leftUnitor⟩

Premises used: CategoryTheory.MonObj.mul_leftUnitor, CategoryTheory.IsMonHom.mk, CategoryTheory.MonObj.one_leftUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X_1 : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X Y Z W : C
inst_6 : MonObj X
inst_7 : MonObj Y
inst_8 : MonObj Z
inst_9 : MonObj W
⊢ IsMonHom.{v₁, u₁} (M := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom (ρ_ X))

Tactic:
⟨one_rightUnitor, mul_rightUnitor⟩

Premises used: CategoryTheory.IsMonHom.mk, CategoryTheory.MonObj.one_rightUnitor, CategoryTheory.MonObj.mul_rightUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
simp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
    (η ⊗ₘ η)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y X) (η ≫ Iso.hom (β_ X Y)) η

Tactic:
simp only [tensorObj.one_def, Category.assoc, BraidedCategory.braiding_naturality,
    braiding_tensorUnit_right, Iso.cancel_iso_inv_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.BraidedCategory.braiding_naturality, CategoryTheory.MonObj.tensorObj.one_def, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.braiding_tensorUnit_right
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
    (η ⊗ₘ η)

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
M N : Mon.{v₁, u₁} C
f : M ⟶ N
⊢ IsMonHom f.hom

Tactic:
f.isMonHom_hom

Premises used: CategoryTheory.Mon.Hom.isMonHom_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
f g : M ⟶ N
w : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext w

Premises used: CategoryTheory.Mon.Hom.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
⊢ Injective.{v₁ + 1, v₁ + 1} (α := M.Hom N) Hom.hom

Tactic:
fun _ _ ↦ Hom.ext

Premises used: CategoryTheory.Mon.Hom.ext, Function.Injective
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : Mon.{v₁, u₁} C
⊢ Hom.hom (𝟙 M) = 𝟙 M.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N K : Mon.{v₁, u₁} C
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A B : Mon.{v₁, u₁} C
f : A ⟶ B
e : IsIso (X := Functor.obj (forget C) A) (Functor.map (forget C) f)
⊢ IsIso f.hom

Tactic:
e
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
M N : Mon.{v₁, u₁} C
f : M ⟶ N
inst_5 : IsIso f
⊢ IsIso f.hom

Tactic:
inferInstanceAs <| IsIso <| (forget C).map f

Premises used: _private.0.CategoryTheory.Mon.instIsIsoHom._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (Mon.X.{v₁, u₁} (trivial C)) (Mon.X.{v₁, u₁} (trivial C)) ⟶ A.X)
    (μ ≫ η) ((η ⊗ₘ η) ≫ μ)

Tactic:
simp [unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
w : f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }
⊢ f = { hom := η, isMonHom_hom := ⋯ }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
w : 𝟙 (Mon.X.{v₁, u₁} (trivial C)) ≫ f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }
⊢ f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }

Tactic:
rw [← Category.id_comp f.hom]

Premises used: CategoryTheory.Mon.Hom.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
w : 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ f.hom = η
⊢ 𝟙 (Mon.X.{v₁, u₁} (trivial C)) ≫ f.hom = Hom.hom { hom := η, isMonHom_hom := ⋯ }

Tactic:
dsimp only [trivial_X]

Premises used: CategoryTheory.Mon.trivial_X
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
A : Mon.{v₁, u₁} C
f : trivial C ⟶ A
w : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A.X) (η ≫ f.hom) η
w₁ w₂ : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ A.X) η η
⊢ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ f.hom = η

Tactic:
rw [← trivial_mon_one, IsMonHom.one_hom]

Premises used: CategoryTheory.IsMonHom.one_hom, CategoryTheory.Mon.trivial_mon_one
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
⊢ HasInitial (Mon.{v₁, u₁} C)

Tactic:
hasInitial_of_unique (Mon.trivial C)

Premises used: CategoryTheory.Limits.hasInitial_of_unique, CategoryTheory.Mon.trivial
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ X.{v₁, u₁} ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory)) = tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ η = 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ μ = Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Mon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (tensorObj (𝒞 := instCategory) X Y).X) η
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Mon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj (𝒞 := instCategory) X Y).X (tensorObj (𝒞 := instCategory) X Y).X ⟶
      (tensorObj (𝒞 := instCategory) X Y).X)
    μ (tensorμ X.X Y.X X.X Y.X ≫ (μ ⊗ₘ μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Mon.{v₁, u₁} C
f : X ⟶ Y
Z : Mon.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X Z).X ⟶ (tensorObj (𝒞 := instCategory) Y Z).X) (Hom.hom (f ▷ Z))
    (f.hom ▷ Z.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y Z : Mon.{v₁, u₁} C
f : Y ⟶ Z
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X Y).X ⟶ (tensorObj (𝒞 := instCategory) X Z).X) (Hom.hom (X ◁ f))
    (X.X ◁ f.hom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory)) X).X ⟶ X.X)
    (Hom.hom (Iso.hom (λ_ X))) (Iso.hom (λ_ X.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ Eq (α := X.X ⟶ (tensorObj (𝒞 := instCategory) ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory)) X).X)
    (Hom.hom (Iso.inv (λ_ X))) (Iso.inv (λ_ X.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory))).X ⟶ X.X)
    (Hom.hom (Iso.hom (ρ_ X))) (Iso.hom (ρ_ X.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X : Mon.{v₁, u₁} C
⊢ Eq (α := X.X ⟶ (tensorObj (𝒞 := instCategory) X ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory))).X)
    (Hom.hom (Iso.inv (ρ_ X))) (Iso.inv (ρ_ X.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y Z : Mon.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z).X ⟶
      (tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)).X)
    (Hom.hom (Iso.hom (α_ X Y Z))) (Iso.hom (α_ X.X Y.X Z.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y Z : Mon.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) X (tensorObj (𝒞 := instCategory) Y Z)).X ⟶
      (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) X Y) Z).X)
    (Hom.hom (Iso.inv (α_ X Y Z))) (Iso.inv (α_ X.X Y.X Z.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (tensorObj (𝒞 := instCategory) M N).X) η
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N : Mon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj (𝒞 := instCategory) M N).X (tensorObj (𝒞 := instCategory) M N).X ⟶
      (tensorObj (𝒞 := instCategory) M N).X)
    μ (tensorμ M.X N.X M.X N.X ≫ (μ ⊗ₘ μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Mon.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
w :
  Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).X) (Hom.hom (f ⊗ₘ g))
    (Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g))
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Y₁ Y₂) (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
inst_5 : BraidedCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Mon.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).X) (Hom.hom (f ⊗ₘ g))
    (Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g))

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      Functor.obj (C := Mon.{v₁, u₁} C) (forget C) ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory)))
    (ε (forget C)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj (C := Mon.{v₁, u₁} C) (forget C) ((𝟙_ (Mon.{v₁, u₁} C)) (𝒞 := instCategory)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    («η» (forget C)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Mon.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget C) X) (Functor.obj (forget C) Y) ⟶
      Functor.obj (forget C) (tensorObj (𝒞 := instCategory) X Y))
    («μ» (forget C) X Y) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Y.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Mon.{v₁, u₁} C
⊢ Eq (α :=
    Functor.obj (forget C) (tensorObj (𝒞 := instCategory) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget C) X) (Functor.obj (forget C) Y))
    (δ (forget C) X Y) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Y.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : SymmetricCategory.{v₁, u₁} C
X Y : C
inst_3 : MonObj X
inst_4 : MonObj Y
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    ((tensorμ X Y X Y ≫ (μ ⊗ₘ μ)) ≫ Iso.hom (β_ X Y))
    ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ tensorμ Y X Y X ≫ (μ ⊗ₘ μ))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y X)
    (μ ≫ Iso.hom (β_ X Y)) ((Iso.hom (β_ X Y) ⊗ₘ Iso.hom (β_ X Y)) ≫ μ)

Tactic:
dsimp [tensorObj.mul_def]

Premises used: CategoryTheory.MonObj.tensorObj.mul_def