diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 8eaa1ba7c..e6adb8d98 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -155,6 +155,15 @@ Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed.
 HB.instance Definition _ := @isMeasurableFun.Build _ _ rT
   (@normr rT rT) (@measurable_normr rT setT).
 
+HB.instance Definition _ := isMeasurableFun.Build _ _ rT
+  (@expR rT) (@measurable_expR rT).
+
+Let measurableT_comp_subproof {rT' : realType} (f : {mfun rT >-> rT'}) (g : {mfun aT >-> rT}) :
+  measurable_fun setT (f \o g).
+Proof. by apply: measurableT_comp; last apply: @measurable_funP _ _ _ g. Qed.
+
+HB.instance Definition _ {rT' : realType} (f : {mfun rT >-> rT'}) (g : {mfun aT >-> rT}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _ _).
+
 End mfun.
 
 Section ring.