-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_associator {M N P : Mon_ C} :
    (tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
          (tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) ⊗ P.mul)) ≫
        (α_ M.X N.X P.X).hom =
      ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
        tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫
          (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ (tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫ (tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) ⊗ P.mul)) ≫
      (α_ M.X N.X P.X).hom =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Tactic:
simp only [tensor_obj, prodMonoidal_tensorObj, Category.assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫ (tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) ⊗ P.mul) ≫ (α_ M.X N.X P.X).hom =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      (tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫
        (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Tactic:
slice_rhs 3 4 => rw [← Category.id_comp M.mul, tensor_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      (tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫
        (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (𝟙 (M.X ⊗ M.X) ⊗ tensorμ N.X P.X N.X P.X) ≫ (M.mul ⊗ N.mul ⊗ P.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ (((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
        tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X) ≫
      (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X ≫ (M.mul ⊗ N.mul ⊗ P.mul)

Tactic:
simp only [Category.assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫ (tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) ⊗ P.mul) ≫ (α_ M.X N.X P.X).hom =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Tactic:
slice_lhs 2 3 => rw [← Category.id_comp P.mul, tensor_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      ((tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫ ((M.mul ⊗ N.mul) ⊗ P.mul)) ≫ (α_ M.X N.X P.X).hom =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      ((tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫ ((M.mul ⊗ N.mul) ⊗ P.mul)) ≫ (α_ M.X N.X P.X).hom =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Tactic:
slice_lhs 3 4 => rw [associator_naturality]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      (tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫
        (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.mul ⊗ tensorμ N.X P.X N.X P.X ≫ (N.mul ⊗ P.mul))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      tensorμ M.X N.X M.X N.X ▷ (P.X ⊗ P.X) ≫ (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X ≫ (M.mul ⊗ N.mul ⊗ P.mul)

Tactic:
slice_lhs 1 3 => rw [associator_monoidal]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ (((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
        tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X) ≫
      (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X ≫ (M.mul ⊗ N.mul ⊗ P.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      (tensorμ M.X N.X M.X N.X ⊗ 𝟙 (P.X ⊗ P.X)) ≫
        (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (𝟙 (M.X ⊗ M.X) ⊗ tensorμ N.X P.X N.X P.X) ≫ (M.mul ⊗ N.mul ⊗ P.mul)

Tactic:
simp only [tensorHom_id, id_tensorHom]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N P : Mon_ C
⊢ tensorμ (M.X ⊗ N.X) P.X (M.X ⊗ N.X) P.X ≫
      tensorμ M.X N.X M.X N.X ▷ (P.X ⊗ P.X) ≫ (α_ (M.X ⊗ M.X) (N.X ⊗ N.X) (P.X ⊗ P.X)).hom ≫ (M.mul ⊗ N.mul ⊗ P.mul) =
    ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫
      tensorμ M.X (N.X ⊗ P.X) M.X (N.X ⊗ P.X) ≫ (M.X ⊗ M.X) ◁ tensorμ N.X P.X N.X P.X ≫ (M.mul ⊗ N.mul ⊗ P.mul)