case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)
apply TensorProduct.ext_threefold
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
intro x y z
no goals
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
x : ↑X
y : ↑Y
z : ↑Z
⊢ ↑((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
rfl