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 : C
inst_3 : MonObj M
inst_4 : MonObj N
simp :
  Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      (η ⊗ₘ η) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
⊢ (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η)) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      tensorμ M N M N ≫ (μ ⊗ₘ μ) =
    Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N))

Tactic:
simp only [comp_whiskerRight_assoc]

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

Tactic:
rw [tensorμ_natural_left]

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

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_left]

Premises used: CategoryTheory.MonoidalCategory.tensorμ_natural_left
-- 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 : C
inst_3 : MonObj M
inst_4 : MonObj N
a : Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N)
| (η ▷ M ⊗ₘ η ▷ N) ≫ (μ ⊗ₘ μ)

Tactic:
rw [tensorHom_comp_tensorHom, one_mul, one_mul]

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

Tactic:
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]

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

Tactic:
symm
-- 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 : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N)) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫
      tensorμ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M N ≫
        (Iso.hom (λ_ M) ⊗ₘ Iso.hom (λ_ N))

Tactic:
tensor_left_unitality M N

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

Tactic:
exact tensor_left_unitality M N

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

Tactic:
simp only [whiskerLeft_comp_assoc]

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

Tactic:
rw [tensorμ_natural_right]

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

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_right]

Premises used: CategoryTheory.MonoidalCategory.tensorμ_natural_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
M N : C
inst_3 : MonObj M
inst_4 : MonObj N
a : Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ N)
| (M ◁ η ⊗ₘ N ◁ η) ≫ (μ ⊗ₘ μ)

Tactic:
rw [tensorHom_comp_tensorHom, mul_one, mul_one]

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

Tactic:
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_one, mul_one]

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

Tactic:
symm
-- 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 : C
inst_3 : MonObj M
inst_4 : MonObj N
⊢ Iso.hom (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N)) =
    tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      tensorμ M N (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        (Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ N))

Tactic:
tensor_right_unitality M N

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

Tactic:
exact tensor_right_unitality M N

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

Tactic:
simp only [comp_whiskerRight_assoc, whiskerLeft_comp_assoc]

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

Tactic:
rw [tensorμ_natural_left]

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

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_left]

Premises used: CategoryTheory.MonoidalCategory.tensorμ_natural_left
-- 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 : C
inst_3 : MonObj M
inst_4 : MonObj N
a : (Iso.hom (α_ M M M) ⊗ₘ Iso.hom (α_ N N N)) ≫ (M ◁ μ ⊗ₘ N ◁ μ) ≫ (μ ⊗ₘ μ)
| (μ ▷ M ⊗ₘ μ ▷ N) ≫ (μ ⊗ₘ μ)

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

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

Tactic:
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom,
    ← tensorHom_comp_tensorHom]

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

Tactic:
rw [tensor_associativity]

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

Tactic:
slice_lhs 1 3 => rw [tensor_associativity]

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

Tactic:
rw [← tensorμ_natural_right]

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

Tactic:
slice_lhs 3 4 => rw [← tensorμ_natural_right]

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

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

Tactic:
rw [← Category.id_comp μ[P], ← 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_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 (α_ 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 ≫ (μ ⊗ₘ μ))
⊢ tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P (tensorObj.{v₁, u₁} (𝒞 := inst) M N) P ≫
      (tensorμ M N M N ≫ (μ ⊗ₘ μ) ⊗ₘ μ) ≫ 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 2 3 => rw [← Category.id_comp μ[P], ← 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
a :
  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)

Tactic:
rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality