[GOAL]
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ g) ≫ (braiding Y₁ Y₂).hom = (braiding X₁ X₂).hom ≫ (g ⊗ f)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂), ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
[PROOFSTEP]
intro x y
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ X₂ Y₁ Y₂ : ModuleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ ↑((f ⊗ g) ≫ (braiding Y₁ Y₂).hom) (x ⊗ₜ[R] y) = ↑((braiding X₁ X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
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)
[PROOFSTEP]
intro x y z
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
apply (cancel_epi (α_ X Y Z).hom).1
[GOAL]
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)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
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)
[PROOFSTEP]
intro x y z
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : ModuleCat R
⊢ (β_ x✝¹ x✝).hom ≫ (β_ x✝ x✝¹).hom = 𝟙 (x✝¹ ⊗ x✝)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : ModuleCat R
⊢ ∀ (x : ↑x✝¹) (y : ↑x✝), ↑((β_ x✝¹ x✝).hom ≫ (β_ x✝ x✝¹).hom) (x ⊗ₜ[R] y) = ↑(𝟙 (x✝¹ ⊗ x✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
aesop_cat
