-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_braiding {X Y : Mon_ C} :
    (X ⊗ Y).mul ≫ (β_ X.X Y.X).hom = ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ (Y ⊗ X).mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (β_ X.X Y.X).hom ▷ (X.X ⊗ Y.X) ≫
      ((((((𝟙 ((Y.X ⊗ X.X) ⊗ X.X ⊗ Y.X) ≫ (α_ Y.X X.X (X.X ⊗ Y.X)).hom) ≫ Y.X ◁ X.X ◁ (β_ X.X Y.X).hom) ≫
                Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
              Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
            Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
          (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
        (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Tactic:
rw [Category.id_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (β_ X.X Y.X).hom ▷ (X.X ⊗ Y.X) ≫
      ((((((α_ Y.X X.X (X.X ⊗ Y.X)).hom ≫ Y.X ◁ X.X ◁ (β_ X.X Y.X).hom) ≫ Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
              Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
            Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
          (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
        (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (((((((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ (α_ Y.X X.X (Y.X ⊗ X.X)).hom) ≫ Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
            Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
          Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
        (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
      (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Tactic:
simp only [Category.assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (β_ X.X Y.X).hom ▷ (X.X ⊗ Y.X) ≫
      ((((((α_ Y.X X.X (X.X ⊗ Y.X)).hom ≫ Y.X ◁ X.X ◁ (β_ X.X Y.X).hom) ≫ Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
              Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
            Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
          (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
        (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Tactic:
slice_lhs 2 3 =>
  rw [← associator_naturality_right]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (β_ X.X Y.X).hom ▷ (X.X ⊗ Y.X) ≫
      ((((((Y.X ⊗ X.X) ◁ (β_ X.X Y.X).hom ≫ (α_ Y.X X.X (Y.X ⊗ X.X)).hom) ≫ Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
              Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
            Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
          (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
        (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (α_ (X.X ⊗ Y.X) X.X Y.X).inv ≫
      (β_ X.X Y.X).hom ▷ X.X ▷ Y.X ≫
        (α_ (Y.X ⊗ X.X) X.X Y.X).hom ≫
          (α_ Y.X X.X (X.X ⊗ Y.X)).hom ≫
            Y.X ◁ X.X ◁ (β_ X.X Y.X).hom ≫
              Y.X ◁ (α_ X.X Y.X X.X).inv ≫
                Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫
                  Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Tactic:
slice_lhs 1 2 =>
  rw [← associator_inv_naturality_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (((((((((β_ X.X Y.X).hom ▷ (X.X ⊗ Y.X) ≫ (α_ (Y.X ⊗ X.X) X.X Y.X).inv) ≫ (α_ (Y.X ⊗ X.X) X.X Y.X).hom) ≫
                  (α_ Y.X X.X (X.X ⊗ Y.X)).hom) ≫
                Y.X ◁ X.X ◁ (β_ X.X Y.X).hom) ≫
              Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
            Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
          Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
        (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
      (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (α_ X.X Y.X (X.X ⊗ Y.X)).hom ≫
      X.X ◁ (α_ Y.X X.X Y.X).inv ≫
        ((((((((((X.X ◁ 𝟙 (Y.X ⊗ X.X) ▷ Y.X ≫ (α_ X.X (Y.X ⊗ X.X) Y.X).inv) ≫ (α_ X.X Y.X X.X).inv ▷ Y.X) ≫
                          (β_ X.X Y.X).hom ▷ X.X ▷ Y.X) ≫
                        (α_ (Y.X ⊗ X.X) X.X Y.X).hom) ≫
                      (α_ Y.X X.X (X.X ⊗ Y.X)).hom) ≫
                    Y.X ◁ X.X ◁ (β_ X.X Y.X).hom) ≫
                  Y.X ◁ (α_ X.X Y.X X.X).inv) ≫
                Y.X ◁ (β_ X.X Y.X).hom ▷ X.X) ≫
              Y.X ◁ (α_ Y.X X.X X.X).hom) ≫
            (α_ Y.X Y.X (X.X ⊗ X.X)).inv) ≫
          (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Tactic:
simp only [id_whiskerRight, MonoidalCategory.whiskerLeft_id, Category.id_comp, Category.assoc,
  pentagon_inv_assoc, Iso.hom_inv_id_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (α_ (X.X ⊗ Y.X) X.X Y.X).inv ≫
      (β_ X.X Y.X).hom ▷ X.X ▷ Y.X ≫
        (α_ (Y.X ⊗ X.X) X.X Y.X).hom ≫
          (α_ Y.X X.X (X.X ⊗ Y.X)).hom ≫
            Y.X ◁ X.X ◁ (β_ X.X Y.X).hom ≫
              Y.X ◁ (α_ X.X Y.X X.X).inv ≫
                Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫
                  Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul) =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫
      (α_ Y.X X.X (Y.X ⊗ X.X)).hom ≫
        Y.X ◁ (α_ X.X Y.X X.X).inv ≫
          Y.X ◁ (β_ X.X Y.X).hom ▷ X.X ≫ Y.X ◁ (α_ Y.X X.X X.X).hom ≫ (α_ Y.X Y.X (X.X ⊗ X.X)).inv ≫ (Y.mul ⊗ X.mul)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (X ⊗ Y).mul ≫ (β_ X.X Y.X).hom = ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ (Y ⊗ X).mul

Tactic:
dsimp

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : SymmetricCategory C
X Y : Mon_ C
⊢ (tensorμ X.X Y.X X.X Y.X ≫ (X.mul ⊗ Y.mul)) ≫ (β_ X.X Y.X).hom =
    ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ tensorμ Y.X X.X Y.X X.X ≫ (Y.mul ⊗ X.mul)