case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    ↑((ihom.ev M).app N) (x ⊗ₜ[R] y) =
      ↑(↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)) (x ⊗ₜ[R] y)
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (ihom.ev M).app N = ↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)
apply TensorProduct.ext'
no goals
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    ↑((ihom.ev M).app N) (x ⊗ₜ[R] y) =
      ↑(↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)) (x ⊗ₜ[R] y)
apply ModuleCat.monoidalClosed_uncurry