case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)
apply TensorProduct.ext_threefold
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
intro x y z
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
change R at y
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] ↑(leftUnitor N).hom (y ⊗ₜ[R] z) = ↑(rightUnitor M).hom (x ⊗ₜ[R] y) ⊗ₜ[R] z
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
change x ⊗ₜ[R] ((leftUnitor N).hom) (y ⊗ₜ[R] z) = ((rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] ↑(leftUnitor N).hom (y ⊗ₜ[R] z) = ↑(rightUnitor M).hom (x ⊗ₜ[R] y) ⊗ₜ[R] z
erw [TensorProduct.lid_tmul, TensorProduct.rid_tmul]
no goals
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z
exact (TensorProduct.smul_tmul _ _ _).symm