case H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (tensorHom (𝟙 M) (𝟙 N)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (𝟙 (of R (↑M ⊗[R] ↑N)))
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))
apply TensorProduct.ext
no goals
case H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (tensorHom (𝟙 M) (𝟙 N)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (𝟙 (of R (↑M ⊗[R] ↑N)))
rfl