-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
    (tensorμ X₁ X₂ Y₁ Y₂ ▷ (Z₁ ⊗ Z₂)) ≫
        tensorμ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) Z₁ Z₂ ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) =
      (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
        ((X₁ ⊗ X₂) ◁ tensorμ Y₁ Y₂ Z₁ Z₂) ≫ tensorμ X₁ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)

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

Tactic:
simp only [braiding_tensor_left, braiding_tensor_right]

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

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

Tactic:
dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]

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

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

Tactic:
calc
  _ = 𝟙 _ ⊗≫
    X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
      X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := by monoidal
  _ = _ := by rw [← whisker_exchange]; monoidal

Result:
no goals

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

Tactic:
rw [← whisker_exchange]

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