diff --git a/src/algebra/category/Module/monoidal.lean b/src/algebra/category/Module/monoidal.lean
index 0cba2bfab3deb..cfdf034c416d1 100644
--- a/src/algebra/category/Module/monoidal.lean
+++ b/src/algebra/category/Module/monoidal.lean
@@ -299,4 +299,17 @@ instance : monoidal_closed (Module.{u} R) :=
       adj := adjunction.mk_of_hom_equiv
       { hom_equiv := λ N P, monoidal_closed_hom_equiv M N P, } } } }
 
+-- I can't seem to express the function coercion here without writing `@coe_fn`.
+@[simp]
+lemma monoidal_closed_curry {M N P : Module.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
+  @coe_fn _ _ linear_map.has_coe_to_fun ((monoidal_closed.curry f : N →ₗ[R] (M →ₗ[R] P)) y) x =
+    f (x ⊗ₜ[R] y) :=
+rfl
+
+@[simp]
+lemma monoidal_closed_uncurry {M N P : Module.{u} R}
+  (f : N ⟶ (M ⟶[Module.{u} R] P)) (x : M) (y : N) :
+  monoidal_closed.uncurry f (x ⊗ₜ[R] y) = (@coe_fn _ _ linear_map.has_coe_to_fun (f y)) x :=
+by { simp only [monoidal_closed.uncurry, ihom.adjunction, is_left_adjoint.adj], simp, }
+
 end Module