-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem Mon_tensor_mul_assoc (M N : Mon_ C) :
    ((tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul)) ▷ (M.X ⊗ N.X)) ≫
        tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
      (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫
        ((M.X ⊗ N.X) ◁ (tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul))) ≫
          tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul)

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

Tactic:
slice_lhs 1 3 => rw [tensor_associativity]

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

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

Tactic:
slice_lhs 3 4 => rw [← tensor_comp, mul_assoc M, mul_assoc N, tensor_comp, tensor_comp]

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

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

Tactic:
simp only [comp_whiskerRight_assoc, MonoidalCategory.whiskerLeft_comp_assoc]

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

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

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

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

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

Tactic:
simp

Result:
no goals

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

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

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