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
inst_2 : BraidedCategory.{v₁, u₁} C
M N P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
slice_lhs :
  tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      (tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      ((tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫ ((μ ⊗ₘ μ) ⊗ₘ μ)) ≫ Iso.hom (α_ M N P) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))

Tactic:
slice_lhs 3 4 => rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
a : (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
| μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ)

Tactic:
rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
slice_rhs :
  tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      (tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      (tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))

Tactic:
slice_rhs 3 4 => rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
simp :
  tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      tensorμ M N M N ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P P ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P ≫ (μ ⊗ₘ μ ⊗ₘ μ)
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      (tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)

Tactic:
simp only [tensorHom_id, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
a :
  (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
    tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P
| tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
    tensorμ M N M N ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P P ≫
      Iso.hom
        (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
          (tensorObj.{v₁, u₁} (𝒞 := inst) P P))

Tactic:
rw [associator_monoidal]

Premises used: CategoryTheory.MonoidalCategory.associator_monoidal
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
slice_lhs :
  ((Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
        tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P) ≫
      (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P ≫ (μ ⊗ₘ μ ⊗ₘ μ)
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      tensorμ M N M N ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P P ≫
        Iso.hom
            (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
              (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
          (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P ≫ (μ ⊗ₘ μ ⊗ₘ μ)

Tactic:
slice_lhs 1 3 => rw [associator_monoidal]

Premises used: CategoryTheory.MonoidalCategory.associator_monoidal
-- 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 P : C
inst_3 : MonObj M
inst_4 : MonObj N
inst_5 : MonObj P
⊢ ((Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
        tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P) ≫
      (μ ⊗ₘ μ ⊗ₘ μ) =
    (Iso.hom (α_ M N P) ⊗ₘ Iso.hom (α_ M N P)) ≫
      tensorμ M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) M (tensorObj.{v₁, u₁} (𝒞 := inst) N P) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ tensorμ N P N P ≫ (μ ⊗ₘ μ ⊗ₘ μ)

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
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : MonObj M
rw :
  (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
        (Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫
          (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ μ)) ≫
      Iso.hom (λ_ M) =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
        (Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ μ)) ≫
      Iso.hom (λ_ M) =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ μ

Tactic:
rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp μ, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Iso.hom, CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp
-- 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 : C
inst_3 : MonObj M
simp :
  (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
        Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ μ) ≫
      Iso.hom (λ_ M) =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
        (Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫
          (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗ₘ μ)) ≫
      Iso.hom (λ_ M) =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
simp only [tensorHom_id, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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 : C
inst_3 : MonObj M
a : Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ μ ≫ Iso.hom (λ_ M)

Tactic:
rw [leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_naturality
-- 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 : C
inst_3 : MonObj M
slice_lhs :
  tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
        Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ μ) ≫
      Iso.hom (λ_ M) =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
slice_lhs 3 4 => rw [leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_naturality
-- 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 : C
inst_3 : MonObj M
a : Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)
| tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
      Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M))

Tactic:
rw [← leftUnitor_monoidal]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_monoidal
-- 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 : C
inst_3 : MonObj M
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M) ⟶
      M)
    ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ μ)
    ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)
⊢ tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M M ≫
        Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
slice_lhs 1 3 => rw [← leftUnitor_monoidal]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_monoidal
-- 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 : C
inst_3 : MonObj M
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M) ⟶
      M)
    ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ μ)
    ((Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)

Tactic:
simp only [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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 : C
inst_3 : MonObj M
rw :
  (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          (μ ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (μ ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ μ

Tactic:
rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Iso.hom, CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp
-- 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 : C
inst_3 : MonObj M
simp :
  (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
          (μ ⊗ₘ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
simp only [tensorHom_id, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- 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 : C
inst_3 : MonObj M
a : Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ
| μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ Iso.hom (ρ_ M)

Tactic:
rw [rightUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- 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 : C
inst_3 : MonObj M
slice_lhs :
  tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ
⊢ (tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          μ ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      Iso.hom (ρ_ M) =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
slice_lhs 3 4 => rw [rightUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- 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 : C
inst_3 : MonObj M
a : Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)
| tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M))

Tactic:
rw [← rightUnitor_monoidal]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_monoidal
-- 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 : C
inst_3 : MonObj M
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      M)
    ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ μ)
    ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)
⊢ tensorμ M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) M M ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ =
    (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ

Tactic:
slice_lhs 1 3 => rw [← rightUnitor_monoidal]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_monoidal
-- 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 : C
inst_3 : MonObj M
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      M)
    ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ μ)
    ((Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ M)) ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ≫ μ)

Tactic:
simp only [Category.id_comp]

Premises used: 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_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
dsimp :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W) (η ≫ (f ⊗ₘ g)) η

Tactic:
dsimp [tensorObj.one_def]

Premises used: CategoryTheory.MonObj.tensorObj.one_def
-- 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 ⊗ₘ g)

Tactic:
rw [tensorHom_comp_tensorHom, one_hom, one_hom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, 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
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
slice_lhs :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
slice_lhs₁ :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    ((Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g))
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

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

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, 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
g : Z ⟶ W
inst_10 : IsMonHom f
inst_11 : IsMonHom g
dsimp :
  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 ≫ (μ ⊗ₘ μ))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y W)
    (μ ≫ (f ⊗ₘ g)) (((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ μ)

Tactic:
dsimp [tensorObj.mul_def]

Premises used: CategoryTheory.MonObj.tensorObj.mul_def
-- 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 : tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g)
| ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W

Tactic:
rw [tensorμ_natural]

Premises used: CategoryTheory.MonoidalCategory.tensorμ_natural