R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)
apply (cancel_epi (α_ X Y Z).hom).1
case H
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    ↑((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
R : Type u
inst✝ : CommRing R
X Y Z : ModuleCat R
⊢ (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    (α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)
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 ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((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 ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((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 ≫ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑((α_ X Y Z).hom ≫ (𝟙 X ⊗ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ⊗ 𝟙 Y)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
rfl