awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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))
have 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))
Tactic: slice_lhs 2 3 => rw [tensorμ_natural_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (M ◁ η ⊗ₘ N ◁ η) ≫ (μ ⊗ₘ μ)
have a : Iso.hom (ρ_ M) ⊗ₘ Iso.hom (ρ_ N)
Tactic: rw [tensorHom_comp_tensorHom, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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))
have 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))
Tactic: slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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))
have 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))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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 ≫ (μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ)
Tactic: simp only [comp_whiskerRight_assoc, whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (μ ⊗ₘ μ) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) M N ≫ tensorμ M N M N
have a : tensorμ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N) M N ≫ (μ ▷ M ⊗ₘ μ ▷ N)
Tactic: rw [tensorμ_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ)
Tactic: slice_lhs 2 3 => rw [tensorμ_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (μ ▷ M ⊗ₘ μ ▷ N) ≫ (μ ⊗ₘ μ)
have a : (Iso.hom (α_ M M M) ⊗ₘ Iso.hom (α_ N N N)) ≫ (M ◁ μ ⊗ₘ N ◁ μ) ≫ (μ ⊗ₘ μ)
Tactic: rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom,
    ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ)
Tactic: slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom,
    ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| 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))
have 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)
Tactic: rw [tensor_associativity]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ)
Tactic: slice_lhs 1 3 => rw [tensor_associativity]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| tensorμ M N (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N) ≫ (M ◁ μ ⊗ₘ N ◁ μ)
have a : tensorObj.{v₁, u₁} (𝒞 := inst) M N ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N
Tactic: rw [← tensorμ_natural_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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 ≫
            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 ≫ (μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ)
Tactic: slice_lhs 3 4 => rw [← tensorμ_natural_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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 ≫ (μ ⊗ₘ μ))
have 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 ≫ (μ ⊗ₘ μ))
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| (tensorμ M N M N ≫ (μ ⊗ₘ μ) ⊗ₘ μ) ≫ Iso.hom (α_ M N P)
have a : ((tensorμ M N M N ⊗ₘ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫ ((μ ⊗ₘ μ) ⊗ₘ μ)) ≫ Iso.hom (α_ M N P)
Tactic: rw [← Category.id_comp μ[P], ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ))
have 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 ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 2 3 => rw [← Category.id_comp μ[P], ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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)
have a : Iso.hom
    (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) N N)
      (tensorObj.{v₁, u₁} (𝒞 := inst) P P)) ≫
  (μ ⊗ₘ μ ⊗ₘ μ)
Tactic: rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ))
have 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 ≫ (μ ⊗ₘ μ))
Tactic: slice_lhs 3 4 => rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ)
have a : (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
Tactic: rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ))
have 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) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
Tactic: slice_rhs 3 4 => rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ ⊗ₘ μ)
Tactic: simp only [tensorHom_id, id_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| 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))
have 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
Tactic: rw [associator_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ 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 ≫ (μ ⊗ₘ μ ⊗ₘ μ)
have 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 ≫ (μ ⊗ₘ μ ⊗ₘ μ)
Tactic: slice_lhs 1 3 => rw [associator_monoidal]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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)) ≫ μ
have 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) ≫ μ
Tactic: rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp μ, ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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) ≫ μ
have 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) ≫ μ
Tactic: simp only [tensorHom_id, id_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ μ ≫ Iso.hom (λ_ M)
have a : Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ μ
Tactic: rw [leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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
⊢ (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) ≫ μ
have 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) ≫ μ
Tactic: slice_lhs 3 4 => rw [leftUnitor_naturality]