diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index eae7a9d6a..460107a35 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -57,6 +57,9 @@
 
 ### Renamed
 
+- in `lebesgue_measure.v`:
+  + `EFin_measurable_fun` -> `measurable_EFinP`
+
 ### Generalized
 
 - in `num_topology.v` (new file):
diff --git a/theories/charge.v b/theories/charge.v
index 7e2d07f48..3ce46c005 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1219,7 +1219,7 @@ rewrite /Rintegral fineK; last first.
   apply: le_lt_trans intfoo.
   apply: ge0_subset_integral => //=.
   apply: measurableT_comp => //.
-  by case/integrableP : intnf => /= /EFin_measurable_fun.
+  by case/integrableP : intnf => /= /measurable_EFinP.
 rewrite -[leLHS](gee0_abs)//; last exact: integral_ge0.
 exact: (le_trans _ (abse_charge_variation _ _)).
 Qed.
@@ -1926,7 +1926,7 @@ have -> : \int[nu]_(x in E) f x =
     by move=> Ex; apply/esym/cvg_lim => //; exact: hf.
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
-  - move=> n; apply/EFin_measurable_fun.
+  - move=> n; apply/measurable_EFinP.
     by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
   - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP.
@@ -1938,7 +1938,7 @@ have -> : \int[mu]_(x in E) (f \* g) x =
   under eq_integral => x /[!inE] /fg -> //.
   apply: monotone_convergence => [//| | |].
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
-      exact/EFin_measurable_fun.
+      exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
   - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
   - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
@@ -1970,7 +1970,7 @@ rewrite ge0_integralZl//.
   rewrite (eq_integral (g \_ (h n @^-1` [set r]))); last first.
     by move=> x xE; rewrite epatch_indic.
   by rewrite -integral_mkcondr -f_integral// integral_indic// setIC.
-- apply: emeasurable_funM; first exact/EFin_measurable_fun.
+- apply: emeasurable_funM; first exact/measurable_EFinP.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
 - by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0.
 - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin.
diff --git a/theories/ftc.v b/theories/ftc.v
index 0a65b63ec..4f553f2c1 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -286,7 +286,7 @@ move=> xu fi F ax fx; suff lfx : lebesgue_pt f x.
   have /(_ ax lfx)[dfx f'xE] := @FTC1_lebesgue_pt _ a _ _ xu fi.
   by split; [exact: dfx|rewrite f'xE].
 apply: itv_continuous_lebesgue_pt xu _ ax fx.
-by move/integrableP : fi => -[/EFin_measurable_fun].
+by move/integrableP : fi => -[/measurable_EFinP].
 Qed.
 
 Corollary continuous_FTC1_closed f (a x : R) (u : R) : (x < u)%R ->
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 80685842a..346c0cb48 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -387,24 +387,24 @@ pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E.
 apply: (@le_lt_trans _ _ x).
   rewrite ge0_le_integral//=.
   - by move=> t _; rewrite lee_fin// powR_ge0.
-  - apply/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp => //.
+  - apply/measurable_EFinP/measurableT_comp_powR/measurableT_comp => //.
     exact: measurable_funD.
   - by move=> t _; rewrite lee_fin mulr_ge0 ?addr_ge0 ?powR_ge0.
-  - by apply/EFin_measurable_fun/measurable_funM/measurable_funD => //;
+  - by apply/measurable_EFinP/measurable_funM/measurable_funD => //;
       exact/measurableT_comp_powR/measurableT_comp.
   - by move=> ? _; rewrite lee_fin.
 rewrite {}/x; under eq_integral do rewrite EFinM.
 rewrite ge0_integralZl_EFin ?powR_ge0//; last 2 first.
   - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0.
-  - by apply/EFin_measurable_fun/measurable_funD => //;
+  - by apply/measurable_EFinP/measurable_funD => //;
       exact/measurableT_comp_powR/measurableT_comp.
 rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
 under eq_integral do rewrite EFinD.
 rewrite ge0_integralD//; last 4 first.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
+  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/EFin_measurable_fun/measurableT_comp_powR/measurableT_comp.
+  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
 by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty.
 Qed.
 
diff --git a/theories/kernel.v b/theories/kernel.v
index 396347359..1594b27f6 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -456,7 +456,7 @@ have CXY : C `<=` XY.
   move=> _ [A mA [B mB <-]]; split; first exact: measurableX.
   rewrite phiM.
   apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI.
-  by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA).
+  by apply/measurable_EFinP; rewrite (_ : \1_ _ = mindic R mA).
 suff lsystemB : lambda_system setT XY by exact: lambda_system_subset.
 split => //; [exact: CXY| |exact: xsection_ndseq_closed].
 move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD.
@@ -522,13 +522,13 @@ rewrite (_ : (fun x => _) =
     apply: ereal_nondecreasing_is_cvgn => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurableT_comp.
+    - exact/measurable_EFinP/measurableT_comp.
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurableT_comp.
+    - exact/measurable_EFinP/measurableT_comp.
     - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
   rewrite -monotone_convergence//.
   - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k.
-  - by move=> n; exact/EFin_measurable_fun/measurableT_comp.
+  - by move=> n; exact/measurable_EFinP/measurableT_comp.
   - by move=> n y _; rewrite lee_fin.
   - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
 apply: measurable_fun_limn_esup => n.
@@ -541,7 +541,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
   apply/funext => x; rewrite -ge0_integral_fsum//.
   - by apply: eq_integral => y _; rewrite -fsumEFin.
   - move=> r.
-    apply/EFin_measurable_fun/measurableT_comp => [//|].
+    apply/measurable_EFinP/measurableT_comp => [//|].
     exact/measurableT_comp.
   - by move=> m y _; rewrite nnfun_muleindic_ge0.
 apply: emeasurable_fun_fsum => // r.
@@ -550,7 +550,7 @@ rewrite [X in measurable_fun _ X](_ : _ = fun x => r%:E *
   apply/funext => x; under eq_integral do rewrite EFinM.
   have [r0|r0] := leP 0%R r.
     rewrite ge0_integralZl//; last by move=> *; rewrite lee_fin.
-    exact/EFin_measurable_fun/measurableT_comp.
+    exact/measurable_EFinP/measurableT_comp.
   rewrite integral0_eq; last first.
     by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
   by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0.
@@ -607,7 +607,7 @@ Hypothesis mf : measurable_fun [set: X] f.
 Let measurable_fun_kdirac U : measurable U ->
   measurable_fun [set: X] (kdirac mf ^~ U).
 Proof.
-move=> mU; apply/EFin_measurable_fun.
+move=> mU; apply/measurable_EFinP.
 by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurableT_comp.
 Qed.
 
@@ -742,7 +742,7 @@ apply: measurable_fun_if => //.
   exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
     exact: measurable_funS (measurable_kernel f U mU).
-  apply/EFin_measurable_fun.
+  apply/measurable_EFinP.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
   + exact: open_measurable.
   + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0.
@@ -787,7 +787,7 @@ apply: measurable_fun_if => //.
     by apply/seteqP; split=> x /= /orP.
   by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst.
 - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
-  apply/EFin_measurable_fun; rewrite setTI.
+  apply/measurable_EFinP; rewrite setTI.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
   + exact: open_measurable.
   + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
@@ -1022,7 +1022,7 @@ Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) :
 Proof.
 under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum//; last 2 first.
-  - move=> r; apply/EFin_measurable_fun/measurableT_comp => [//|].
+  - move=> r; apply/measurable_EFinP/measurableT_comp => [//|].
     have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
     by rewrite (_ : \1__ = mindic R fr).
   - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
@@ -1031,7 +1031,7 @@ under [in RHS]eq_integral.
   under eq_integral.
     by move=> z _; rewrite fimfunE -fsumEFin//; over.
   rewrite /= ge0_integral_fsum//; last 2 first.
-    - move=> r; apply/EFin_measurable_fun/measurableT_comp => [//|].
+    - move=> r; apply/measurable_EFinP/measurableT_comp => [//|].
       have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
       by rewrite (_ : \1__ = mindic R fr).
     - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
@@ -1070,7 +1070,7 @@ have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
 transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))).
   by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f.
 rewrite monotone_convergence//; last 3 first.
-  by move=> n; exact/EFin_measurable_fun.
+  by move=> n; exact/measurable_EFinP.
   by move=> n z _; rewrite lee_fin.
   by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
 rewrite (_ : (fun _ => _) =
@@ -1081,16 +1081,16 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])).
   - move=> n; apply: measurable_fun_integral_kernel => //.
     + by move=> U mU; exact: measurableT_comp (measurable_kernel k _ mU) _.
     + by move=> z; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
   - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin.
   - move=> y _ a b ab; apply: ge0_le_integral => //.
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
+    + exact/measurable_EFinP.
     + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin.
 apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.
-  - by move=> n; exact/EFin_measurable_fun.
+  - by move=> n; exact/measurable_EFinP.
   - by move=> n z _; rewrite lee_fin.
   - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
 by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 28f918c46..176ac5c0a 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1731,7 +1731,7 @@ Let measurable_almost_continuous' (f : rT -> rT) (eps : rT) :
   {within K, continuous f}].
 Proof.
 move: eps=> _/posnumP[eps] mf; pose f' := EFin \o f.
-have mf' : measurable_fun A f' by exact/EFin_measurable_fun.
+have mf' : measurable_fun A f' by exact/measurable_EFinP.
 have [/= g_ gf'] := @approximation_sfun _ R rT _ _ mA mf'.
 pose e2n n := (eps%:num / 2) / (2 ^ n.+1)%:R.
 have e2npos n : (0 < e2n n)%R by rewrite divr_gt0.
@@ -1814,7 +1814,7 @@ wlog fg : D mD mf mg mfg / forall x, D x -> f x +? g x => [hwlogD|]; last first.
    have [f_ f_cvg] := approximation_sfun mD mf.
    have [g_ g_cvg] := approximation_sfun mD mg.
    apply: (emeasurable_fun_cvg (fun n x => (f_ n x + g_ n x)%:E)) => //.
-     by move=> n; apply/EFin_measurable_fun/measurable_funTS/measurable_funD.
+     by move=> n; exact/measurable_EFinP/measurable_funTS/measurable_funD.
   move=> x Dx; under eq_fun do rewrite EFinD.
   exact: cvgeD (fg _ _) (f_cvg _ _) (g_cvg _ _).
 move=> A mA; wlog NAnoo: A mD mf mg mA / ~ (A -oo) => [hwlogA|].
@@ -1912,7 +1912,7 @@ wlog fg : D mD mf mg mfg / forall x, D x -> f x *? g x => [hwlogM|]; last first.
   have [f_ f_cvg] := approximation_sfun mD mf.
   have [g_ g_cvg] := approximation_sfun mD mg.
   apply: (emeasurable_fun_cvg (fun n x => (f_ n x * g_ n x)%:E)) => //.
-    move=> n; apply/EFin_measurable_fun.
+    move=> n; apply/measurable_EFinP.
     by apply: measurable_funM => //; exact: measurable_funTS.
   move=> x Dx; under eq_fun do rewrite EFinM.
   exact: cvgeM (fg _ _) (f_cvg _ _) (g_cvg _ _).
@@ -2310,7 +2310,7 @@ move=> fk0 mfk; have [k0|k0] := ltP k 0%R.
   rewrite integral0_eq//; last by move=> x _; rewrite fk0// indic0 mulr0.
   by rewrite integral0_eq ?mule0// => x _; rewrite fk0// indic0.
 under eq_integral do rewrite EFinM.
-rewrite ge0_integralZl//; first exact/EFin_measurable_fun.
+rewrite ge0_integralZl//; first exact/measurable_EFinP.
 by move=> y _; rewrite lee_fin.
 Qed.
 
@@ -2345,7 +2345,7 @@ Let integral_mscale_nnsfun (h : {nnsfun T >-> R}) :
 Proof.
 under [LHS]eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite [LHS]ge0_integral_fsum//; last 2 first.
-  - by move=> r; exact/EFin_measurable_fun/measurableT_comp.
+  - by move=> r; exact/measurable_EFinP/measurableT_comp.
   - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
 rewrite -[RHS]ge0_integralZl//; last 2 first.
   - by apply: measurableT_comp => //; exact: measurable_funTS.
@@ -2355,11 +2355,11 @@ under [RHS]eq_integral.
     by move=> r; rewrite EFinM nnfun_muleindic_ge0.
   over.
 rewrite [RHS]ge0_integral_fsum//; last 2 first.
-  - by move=> r; apply/EFin_measurable_fun; do 2 apply/measurableT_comp => //.
+  - by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
   - by move=> n x _; rewrite EFinM mule_ge0// nnfun_muleindic_ge0.
 apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
 - by rewrite !integralZl_indic_nnsfun//= integral_mscale_indic// muleCA.
-- exact/EFin_measurable_fun/measurableT_comp.
+- exact/measurable_EFinP/measurableT_comp.
 - by move=> t _; rewrite nnfun_muleindic_ge0.
 Qed.
 
@@ -2378,16 +2378,16 @@ rewrite (_ : \int[m]_(x in D) _ =
     limn (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first.
   rewrite -monotone_convergence//=.
   - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f.
-  - by move=> n; exact/EFin_measurable_fun/measurable_funTS.
+  - by move=> n; exact/measurable_EFinP/measurable_funTS.
   - by move=> n x _; rewrite lee_fin.
   - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin.
 rewrite -limeMl//.
   by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun.
 apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
-- exact/EFin_measurable_fun/measurable_funTS.
+- exact/measurable_EFinP/measurable_funTS.
 - by move=> x _; rewrite lee_fin.
-- exact/EFin_measurable_fun/measurable_funTS.
+- exact/measurable_EFinP/measurable_funTS.
 - by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP.
 Qed.
 
@@ -2537,7 +2537,7 @@ have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t).
 transitivity (limn (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)).
   rewrite -monotone_convergence//.
   - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f.
-  - by move=> n; exact/EFin_measurable_fun.
+  - by move=> n; exact/measurable_EFinP.
   - by move=> n y _; rewrite lee_fin.
   - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_.
 rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)).
@@ -2554,14 +2554,14 @@ transitivity (\sum_(k \in range (f_ n))
     \int[mu]_x (k * \1_((f_ n @^-1` [set k]) \o phi) x)%:E).
   under eq_integral do rewrite fimfunE -fsumEFin//.
   rewrite ge0_integral_fsum//; last 2 first.
-    - by move=> y; apply/EFin_measurable_fun; exact: measurable_funM.
+    - by move=> y; apply/measurable_EFinP; exact: measurable_funM.
     - by move=> y x _; rewrite nnfun_muleindic_ge0.
   apply: eq_fsbigr => r _; rewrite integralZl_indic_nnsfun// integral_indic//=.
   rewrite (integralZl_indic _ (fun r => f_ n @^-1` [set r] \o phi))//.
     by congr (_ * _); rewrite [RHS](@integral_indic).
   by move=> r0; rewrite preimage_nnfun0.
 rewrite -ge0_integral_fsum//; last 2 first.
-  - by move=> r; apply/EFin_measurable_fun; exact: measurable_funM.
+  - by move=> r; apply/measurable_EFinP; exact: measurable_funM.
   - by move=> r x _; rewrite nnfun_muleindic_ge0.
 by apply: eq_integral => x _; rewrite fsumEFin// -fimfunE.
 Qed.
@@ -2582,7 +2582,7 @@ transitivity (limn (fun n => \int[\d_ a]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//.
   - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f.
     by rewrite inE in Dx.
-  - by move=> n; apply/EFin_measurable_fun; exact/measurable_funTS.
+  - by move=> n; apply/measurable_EFinP; exact/measurable_funTS.
   - by move=> *; rewrite lee_fin.
   - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_.
 rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)).
@@ -2596,7 +2596,7 @@ rewrite ge0_integral_fsum//.
   rewrite fsbig1 ?adde0// => r /= [_ rfna].
   rewrite integral_indic//= diracE memNset ?mule0//=.
   by apply/not_andP; left; exact/nesym.
-- by move=> r; exact/EFin_measurable_fun/measurableT_comp.
+- by move=> r; exact/measurable_EFinP/measurableT_comp.
 - by move=> r x _; rewrite nnfun_muleindic_ge0.
 Qed.
 
@@ -2688,7 +2688,7 @@ rewrite big_ord_recr/= -ih.
 rewrite (_ : _ m_ N.+1 = measure_add (msum m_ N) (m_ N)); last first.
   by apply/funext => A; rewrite measure_addE /msum/= big_ord_recr.
 have mf_ n : measurable_fun D (fun x => (f_ n x)%:E).
-  exact/measurable_funTS/EFin_measurable_fun.
+  exact/measurable_funTS/measurable_EFinP.
 have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin.
 have cvg_f_ (m : {measure set T -> \bar R}) :
     cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E).
@@ -2795,7 +2795,7 @@ apply: lee_nneseries => n _.
   by apply: integral_ge0 => // x _; rewrite lee_fin.
 rewrite [leRHS]integral_mkcond; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
-- exact/EFin_measurable_fun.
+- exact/measurable_EFinP.
 - by move=> x _; rewrite erestrict_ge0.
 - exact/(measurable_restrictT _ mD).
 Qed.
@@ -2897,8 +2897,8 @@ Lemma integral_setU_EFin d (T : measurableType d) (R : realType)
 Proof.
 move=> mA mB ABf AB.
 rewrite integralE/=.
-rewrite ge0_integral_setU//; last exact/measurable_funepos/EFin_measurable_fun.
-rewrite ge0_integral_setU//; last exact/measurable_funeneg/EFin_measurable_fun.
+rewrite ge0_integral_setU//; last exact/measurable_funepos/measurable_EFinP.
+rewrite ge0_integral_setU//; last exact/measurable_funeneg/measurable_EFinP.
 rewrite [X in _ = X + _]integralE/=.
 rewrite [X in _ = _ + X]integralE/=.
 set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _.
@@ -3111,7 +3111,7 @@ have: \int[mu]_(x in D) (`|M + 1|%:E * `|g x|) < +oo.
   by apply: measurableT_comp => //; exact: measurable_int gi.
 apply/le_lt_trans/ge0_le_integral => //.
 - apply/emeasurable_funM; last exact/measurableT_comp/(measurable_int _ gi).
-  exact/EFin_measurable_fun/measurableT_comp.
+  exact/measurable_EFinP/measurableT_comp.
 - apply/emeasurable_funM => //; apply/measurableT_comp => //.
   exact: measurable_int gi.
 - move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=.
@@ -3291,7 +3291,7 @@ Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType)
     (mu : {finite_measure set T -> \bar R}) k :
   mu.-integrable [set: T] (EFin \o cst k).
 Proof.
-apply/integrableP; split; first exact/EFin_measurable_fun.
+apply/integrableP; split; first exact/measurable_EFinP.
 have [k0|k0] := leP 0 k.
 - under eq_integral do rewrite /= ger0_norm//.
   rewrite integral_cstr//= lte_mul_pinfty// fin_num_fun_lty//.
@@ -3339,7 +3339,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
     by rewrite ge0_fin_numE// integral_ge0.
   apply: ge0_le_integral => //.
   - by move=> *; rewrite lee_fin /indic.
-  - exact/EFin_measurable_fun/measurableT_comp.
+  - exact/measurable_EFinP/measurableT_comp.
   - by apply: measurableT_comp => //; exact: measurable_int fint.
   - move=> x Dx; rewrite /= indicE.
     have [|xE] := boolP (x \in E); last by rewrite mule0.
@@ -4403,7 +4403,7 @@ move: ifoo.
 rewrite -ge0_fin_numE; last exact: integral_ge0.
 move/fineK ->.
 by apply: ge0_le_integral => //=; do 2 apply: measurableT_comp => //;
-  exact/EFin_measurable_fun.
+  exact/measurable_EFinP.
 Qed.
 
 Lemma Rintegral_setU_EFin (A B : set T) (f : T -> R) :
@@ -4412,7 +4412,7 @@ Lemma Rintegral_setU_EFin (A B : set T) (f : T -> R) :
   \int[mu]_(x in (A `|` B)) f x = \int[mu]_(x in A) f x + \int[mu]_(x in B) f x.
 Proof.
 move=> mA mB mf AB; rewrite /Rintegral integral_setU_EFin//; last first.
-  exact/EFin_measurable_fun/(measurable_int mu).
+  exact/measurable_EFinP/(measurable_int mu).
 have mAf :  mu.-integrable A (EFin \o f).
   by  apply: integrableS mf => //; exact: measurableU.
 have mBf :  mu.-integrable B (EFin \o f).
@@ -4644,7 +4644,7 @@ have CB : C `<=` B.
     rewrite funeqE => x; rewrite indicE /phi /m2/= /mrestr.
     have [xX1|xX1] := boolP (x \in X1); first by rewrite mule1 in_xsectionX.
     by rewrite mule0 notin_xsectionX// set0I measure0.
-  exact/measurable_funeM/EFin_measurable_fun.
+  exact/measurable_funeM/measurable_EFinP.
 suff lsystemB : lambda_system setT B by exact: lambda_system_subset.
 split => //; [exact: CB| |exact: xsection_ndseq_closed].
 move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD.
@@ -4685,7 +4685,7 @@ have CB : C `<=` B.
     rewrite funeqE => y; rewrite indicE /psi /m1/= /mrestr.
     have [yX2|yX2] := boolP (y \in X2); first by rewrite mule1 in_ysectionX.
     by rewrite mule0 notin_ysectionX// set0I measure0.
-  exact/measurable_funeM/EFin_measurable_fun.
+  exact/measurable_funeM/measurable_EFinP.
 suff lsystemB : lambda_system setT B by exact: lambda_system_subset.
 split => //; [exact: CB| |exact: ysection_ndseq_closed].
 move=> X Y XY [mX mphiX] [mY mphiY]; split; first exact: measurableD.
@@ -4966,7 +4966,7 @@ Lemma measurable_bounded_integrable (f : T -> R^o)  :
   mu E < +oo -> measurable_fun E f ->
   [bounded f x | x in E] -> mu.-integrable E (EFin \o f).
 Proof.
-move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
+move=> Afin mfA bdA; apply/integrableP; split; first exact/measurable_EFinP.
 have [M [_ mrt]] := bdA; apply: le_lt_trans.
   apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
   by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm.
@@ -4983,14 +4983,14 @@ Proof.
 move=> intf fpos; case/integrableP: (intf) => mfE _.
 pose g_ n := nnsfun_approx mE mfE n.
 have [] // := @dominated_convergence _ _ _ mu _ mE (fun n => EFin \o g_ n) f f.
-- by move=> ?; apply/EFin_measurable_fun/measurable_funTS.
+- by move=> ?; exact/measurable_EFinP/measurable_funTS.
 - apply: aeW => ? ?; under eq_fun => ? do rewrite /g_ nnsfun_approxE.
   exact: ecvg_approx.
 - apply: aeW => /= ? ? ?; rewrite ger0_norm // /g_ nnsfun_approxE.
   exact: le_approx.
 move=> _ /= fg0 gfcvg; exists g_; split.
 - move=> n; apply: (le_integrable mE _ _ intf).
-    exact/EFin_measurable_fun/measurable_funTS.
+    exact/measurable_EFinP/measurable_funTS.
   move=> ? ?; rewrite /g_ !gee0_abs ?lee_fin//; last exact: fpos.
   by rewrite /= nnsfun_approxE le_approx.
 - exact: cvg_nnsfun_approx.
@@ -5087,7 +5087,7 @@ Lemma approximation_continuous_integrable (E : set _) (f : rT -> rT):
         \int[mu]_(z in E) `|(f z - g_ n z)%:E| @[n --> \oo] --> 0].
 Proof.
 move=> mE Efin intf.
-have mf : measurable_fun E f by case/integrableP : intf => /EFin_measurable_fun.
+have mf : measurable_fun E f by case/integrableP : intf => /measurable_EFinP.
 suff apxf eps : exists h : rT -> rT, (eps > 0)%R ->
     [/\ continuous h,
         mu.-integrable E (EFin \o h) &
@@ -5256,14 +5256,14 @@ Proof.
 rewrite funeqE => x; rewrite /F /fubini_F [in LHS]/=.
 under eq_fun do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum //; last 2 first.
-  - move=> i; apply/EFin_measurable_fun/measurableT_comp => //=.
+  - move=> i; apply/measurable_EFinP/measurableT_comp => //=.
     exact: measurableT_comp.
   - by move=> r y _; rewrite EFinM nnfun_muleindic_ge0.
 apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
 under eq_fun do rewrite EFinM.
 rewrite ge0_integralZl//; last by rewrite lee_fin.
 - by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
-- exact/EFin_measurable_fun/measurableT_comp.
+- exact/measurable_EFinP/measurableT_comp.
 - by move=> y _; rewrite lee_fin.
 Qed.
 
@@ -5279,14 +5279,14 @@ Proof.
 rewrite funeqE => y; rewrite /G /fubini_G [in LHS]/=.
 under eq_fun do rewrite fimfunE -fsumEFin//.
 rewrite ge0_integral_fsum //; last 2 first.
-  - move=> i; apply/EFin_measurable_fun/measurableT_comp => //=.
+  - move=> i; apply/measurable_EFinP/measurableT_comp => //=.
     exact: measurableT_comp.
   - by move=> r x _; rewrite EFinM nnfun_muleindic_ge0.
 apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
 under eq_fun do rewrite EFinM.
 rewrite ge0_integralZl//; last by rewrite lee_fin.
 - by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
-- exact/EFin_measurable_fun/measurableT_comp.
+- exact/measurable_EFinP/measurableT_comp.
 - by move=> x _; rewrite lee_fin.
 Qed.
 
@@ -5304,14 +5304,13 @@ Lemma sfun_fubini_tonelli1 : \int[m1 \x m2]_z (f z)%:E = \int[m1]_x F x.
 Proof.
 under [LHS]eq_integral
   do rewrite EFinf; rewrite ge0_integral_fsum //; last 2 first.
-  - move=> r.
-    apply/EFin_measurable_fun/measurableT_comp => //=.
+  - by move=> r; exact/measurable_EFinP/measurableT_comp.
   - by move=> r /= z _; exact: nnfun_muleindic_ge0.
 transitivity (\sum_(k \in range f)
   \int[m1]_x (k%:E * fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x)).
   apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
   rewrite ge0_integralZl//; last 3 first.
-    - exact/EFin_measurable_fun.
+    - exact/measurable_EFinP.
     - by move=> /= x _; rewrite lee_fin.
     - by rewrite lee_fin.
   rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin.
@@ -5332,14 +5331,13 @@ Lemma sfun_fubini_tonelli2 : \int[m1 \x^ m2]_z (f z)%:E = \int[m2]_y G y.
 Proof.
 under [LHS]eq_integral
   do rewrite EFinf; rewrite ge0_integral_fsum //; last 2 first.
-  - move=> i.
-  apply/EFin_measurable_fun/measurableT_comp => //=.
+  - by move=> i; exact/measurable_EFinP/measurableT_comp.
   - by move=> r /= z _; exact: nnfun_muleindic_ge0.
 transitivity (\sum_(k \in range f)
   \int[m2]_x (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))).
   apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
   rewrite ge0_integralZl//; last 3 first.
-    - exact/EFin_measurable_fun.
+    - exact/measurable_EFinP.
     - by move=> /= x _; rewrite lee_fin.
     - by rewrite lee_fin.
   rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin.
@@ -5387,7 +5385,7 @@ apply: (emeasurable_fun_cvg (F_ g)) => //.
       fun y => limn (EFin \o g ^~ (x, y))); last first.
     by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: g_f.
   apply: cvg_monotone_convergence => //.
-  - by move=> n; apply/EFin_measurable_fun => //; exact/measurableT_comp.
+  - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp.
   - by move=> n y _; rewrite lee_fin//; exact: fun_ge0.
   - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/g_nd.
 Qed.
@@ -5401,7 +5399,7 @@ apply: (emeasurable_fun_cvg (G_ g)) => //.
       fun x => limn (EFin \o g ^~ (x, y))); last first.
     by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: g_f.
   apply: cvg_monotone_convergence => //.
-  - by move=> n; apply/EFin_measurable_fun => //; exact/measurableT_comp.
+  - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp.
   - by move=> n x _; rewrite lee_fin; exact: fun_ge0.
   - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/g_nd.
 Qed.
@@ -5412,13 +5410,13 @@ have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x).
 have F_F x : F x = limn (F_ g ^~ x).
   rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y (EFin \o g n) (x, y)))//.
   rewrite -monotone_convergence//; last 3 first.
-    - by move=> n; exact/EFin_measurable_fun/measurableT_comp.
+    - by move=> n; exact/measurable_EFinP/measurableT_comp.
     - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0.
     - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact.
   by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: g_f.
 rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)).
   rewrite -monotone_convergence //; last 3 first.
-    - by move=> n; exact/EFin_measurable_fun.
+    - by move=> n; exact/measurable_EFinP.
     - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
     - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact.
   by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f.
@@ -5433,9 +5431,9 @@ rewrite -monotone_convergence //; first exact: eq_integral.
   exact: fun_ge0.
 - move=> x /= _ a b ab; apply: ge0_le_integral => //.
   + by move=> y _; rewrite lee_fin; exact: fun_ge0.
-  + exact/EFin_measurable_fun/measurableT_comp.
+  + exact/measurable_EFinP/measurableT_comp.
   + by move=> *; rewrite lee_fin; exact: fun_ge0.
-  + exact/EFin_measurable_fun/measurableT_comp.
+  + exact/measurable_EFinP/measurableT_comp.
   + by move=> y _; rewrite lee_fin; move/g_nd : ab => /lefP; exact.
 Qed.
 
@@ -5446,13 +5444,13 @@ have G_G y : G y = limn (G_ g ^~ y).
   rewrite /G /fubini_G.
   rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x (EFin \o g n) (x, y)))//.
   rewrite -monotone_convergence//; last 3 first.
-    - by move=> n; exact/EFin_measurable_fun/measurableT_comp.
+    - by move=> n; exact/measurable_EFinP/measurableT_comp.
     - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
     - by move=> x /= _ a b; rewrite lee_fin => /g_nd/lefP; exact.
   by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: g_f.
 rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)).
   rewrite -monotone_convergence //; last 3 first.
-    - by move=> n; exact/EFin_measurable_fun.
+    - by move=> n; exact/measurable_EFinP.
     - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0.
     - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact.
   by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f.
@@ -5466,9 +5464,9 @@ rewrite -monotone_convergence //; first exact: eq_integral.
 - by move=> n y _; apply: integral_ge0 => // x _ /=; rewrite lee_fin fun_ge0.
 - move=> y /= _ a b ab; apply: ge0_le_integral => //.
   + by move=> x _; rewrite lee_fin fun_ge0.
-  + exact/EFin_measurable_fun/measurableT_comp.
+  + exact/measurable_EFinP/measurableT_comp.
   + by move=> *; rewrite lee_fin fun_ge0.
-  + exact/EFin_measurable_fun/measurableT_comp.
+  + exact/measurable_EFinP/measurableT_comp.
   + by move=> x _; rewrite lee_fin; move/g_nd : ab => /lefP; exact.
 Qed.
 
@@ -5836,12 +5834,12 @@ Definition locally_integrable D f := [/\ measurable_fun D f, open D &
 Lemma open_integrable_locally D f : open D ->
   mu.-integrable D (EFin \o f) -> locally_integrable D f.
 Proof.
-move=> oD /integrableP[mf foo]; split => //; first exact/EFin_measurable_fun.
+move=> oD /integrableP[mf foo]; split => //; first exact/measurable_EFinP.
 move=> K KD cK; rewrite (le_lt_trans _ foo)// ge0_subset_integral//=.
 - exact: compact_measurable.
 - exact: open_measurable.
-- apply/EFin_measurable_fun; apply: measurableT_comp => //.
-  exact/EFin_measurable_fun.
+- apply/measurable_EFinP; apply: measurableT_comp => //.
+  exact/measurable_EFinP.
 Qed.
 
 Lemma locally_integrableN D f :
@@ -5861,10 +5859,10 @@ suff : lebesgue_measure.-integrable K ((EFin \o f) \+ (EFin \o g)).
   by case/integrableP.
 apply: integrableD => //=; first exact: compact_measurable.
 - apply/integrableP; split; last exact: foo.
-  apply/EFin_measurable_fun; apply: measurable_funS mf => //.
+  apply/measurable_EFinP; apply: measurable_funS mf => //.
   exact: open_measurable.
 - apply/integrableP; split; last exact: goo.
-  apply/EFin_measurable_fun; apply: measurable_funS mg => //.
+  apply/measurable_EFinP; apply: measurable_funS mg => //.
   exact: open_measurable.
 Qed.
 
@@ -5898,9 +5896,9 @@ have ? : measurable_fun [set: R] (f \_ A).
   exact/(measurable_restrictT _ _).2.
 split => // K KT cK; apply: le_lt_trans (ifB _ KT cK).
 apply: ge0_le_integral => //=; first exact: compact_measurable.
-- apply/EFin_measurable_fun; apply/measurableT_comp => //.
+- apply/measurable_EFinP; apply/measurableT_comp => //.
   exact/measurable_funTS.
-- apply/EFin_measurable_fun; apply/measurableT_comp => //.
+- apply/measurable_EFinP; apply/measurableT_comp => //.
   exact/measurable_funTS.
 - move=> x Kx; rewrite lee_fin !patchE.
   case: ifPn => xA; case: ifPn => xB //; last by rewrite normr0.
@@ -5913,7 +5911,7 @@ Lemma integrable_locally_restrict f (A : set R) : measurable A ->
 Proof.
 move=> mA intf; split.
 - move/integrableP : intf => [mf _].
-  by apply/(measurable_restrictT _ _).1 => //; exact/EFin_measurable_fun.
+  by apply/(measurable_restrictT _ _).1 => //; exact/measurable_EFinP.
 - exact: openT.
 - move=> K _ cK.
   move/integrableP : intf => [mf].
@@ -5921,7 +5919,7 @@ move=> mA intf; split.
   under eq_integral do rewrite restrict_EFin restrict_normr.
   apply: le_lt_trans.
   apply: ge0_subset_integral => //=; first exact: compact_measurable.
-  apply/EFin_measurable_fun/measurableT_comp/EFin_measurable_fun => //=.
+  apply/measurable_EFinP/measurableT_comp/measurable_EFinP => //=.
   move/(measurable_restrictT _ _).1 : mf => /=.
   by rewrite restrict_EFin; exact.
 Qed.
@@ -6540,7 +6538,7 @@ Lemma Rintegral_itv_bndo_bndc (a : itv_bound R) (r : R) f :
    \int[mu]_(x in [set` Interval a (BRight r)]) (f x).
 Proof.
 move=> mf; rewrite /Rintegral integral_itv_bndo_bndc//.
-by apply/EFin_measurable_fun; exact: (measurable_int mu).
+by apply/measurable_EFinP; exact: (measurable_int mu).
 Qed.
 
 Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f :
@@ -6549,7 +6547,7 @@ Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f :
   \int[mu]_(x in [set` Interval (BLeft r) b]) (f x).
 Proof.
 move=> mf; rewrite /Rintegral integral_itv_obnd_cbnd//.
-by apply/EFin_measurable_fun; exact: (measurable_int mu).
+by apply/measurable_EFinP; exact: (measurable_int mu).
 Qed.
 
 Lemma Rintegral_set1 f (r : R) : \int[mu]_(x in [set r]) f x = 0.
@@ -6660,7 +6658,7 @@ pose HLf_g_Be n : set _ :=
 pose Ee := \bigcap_n (B k `&` (HLf_g_Be n `|` f_g_Be n)).
 case/integrableP: (intf_ k) => mf intf.
 have mfg n : measurable_fun setT (f_ k \- g_ n)%R.
-  apply: measurable_funB; first by move/EFin_measurable_fun : mf.
+  apply: measurable_funB; first by move/measurable_EFinP : mf.
   by apply: continuous_measurable_fun; exact: cg_.
 have locg_B n : locally_integrable [set: R] (g_B n).
   split; [|exact: openT|].
@@ -6681,12 +6679,12 @@ have locg_B n : locally_integrable [set: R] (g_B n).
       by rewrite normr0 lee_fin.
 have locf_g_B n : locally_integrable setT (f_ k \- g_B n)%R.
   apply: locally_integrableB => //; split.
-  - by move/EFin_measurable_fun : mf.
+  - by move/measurable_EFinP : mf.
   - exact: openT.
   - move=> K _ cK; rewrite (le_lt_trans _ intf)//=.
     apply: ge0_subset_integral => //.
     + exact: compact_measurable.
-    + by do 2 apply: measurableT_comp => //; move/EFin_measurable_fun : mf.
+    + by do 2 apply: measurableT_comp => //; move/measurable_EFinP : mf.
 have mEHL i : measurable (HLf_g_Be i).
   rewrite /HLf_g_Be -[X in measurable X]setTI.
   apply: emeasurable_fun_o_infty => //.
@@ -6707,11 +6705,11 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee.
     apply/seteqP; split => [x [Ex] /=|x [Ex] /=].
       rewrite (@lim_sup_davgB _ _ _ _ (B k))//.
       by split; [exact: ball_open|exact: Ex].
-      by move/EFin_measurable_fun : mf; apply: measurable_funS.
+      by move/measurable_EFinP : mf; apply: measurable_funS.
       by apply: cg_B; rewrite inE.
     rewrite (@lim_sup_davgB _ _ _ _ (B k))//.
     by split; [exact: ball_open|exact: Ex].
-    by move/EFin_measurable_fun : mf; apply: measurable_funS.
+    by move/measurable_EFinP : mf; apply: measurable_funS.
     by apply: cg_B; rewrite inE.
   move=> r /= [Er] efgnr; split => //.
   have {}efgnr := lt_le_trans efgnr (lim_sup_davgT_HL_maximal r (locf_g_B n)).
@@ -6773,7 +6771,7 @@ pose fk k := f \_ (B k).
 have mfk k : mu.-integrable setT (EFin \o fk k).
   case: locf => mf _ intf.
   apply/integrableP; split => /=.
-    by apply/EFin_measurable_fun/(measurable_restrictT _ _).1 => //=;
+    by apply/measurable_EFinP/(measurable_restrictT _ _).1 => //=;
       [exact: measurable_ball|exact: measurable_funS mf].
   rewrite (_ : (fun x => _) = (EFin \o normr \o f) \_ (B k)); last first.
     by apply/funext => x; rewrite restrict_EFin/= restrict_normr.
@@ -6855,14 +6853,14 @@ have : (fine (mu (ball x r)))^-1%:E *
     rewrite lte_fin invr_gt0// fine_gt0//.
     by rewrite lebesgue_measure_ball// ltry andbT lte_fin mulrn_wgt0.
   apply: le_abse_integral => //; first exact: measurable_ball.
-  by apply/EFin_measurable_fun; exact: measurable_funB.
+  by apply/measurable_EFinP; exact: measurable_funB.
 set f := (f in f r @[r --> 0^'+] --> _ -> _).
 rewrite (_ : f = fun r => (fine (mu (ball x r)))^-1%:E *
    `|mu (A `&` ball x r) - (\1_A x)%:E * mu (ball x r)|); last first.
   apply/funext => r; rewrite /f integralB_EFin//=; last 3 first.
     - exact: measurable_ball.
     - apply/integrableP; split.
-        exact/EFin_measurable_fun/measurable_indic.
+        exact/measurable_EFinP/measurable_indic.
       under eq_integral do rewrite /= ger0_norm//=.
       rewrite integral_indic//=; last exact: measurable_ball.
       rewrite -/mu (@le_lt_trans _ _ (mu (ball x r)))// ?le_measure// ?inE.
@@ -6871,7 +6869,7 @@ rewrite (_ : f = fun r => (fine (mu (ball x r)))^-1%:E *
       + have [r0|r0] := ltP r 0%R.
           by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0.
         by rewrite lebesgue_measure_ball//= ?ltry.
-    - apply/integrableP; split; first exact/EFin_measurable_fun/measurable_cst.
+    - apply/integrableP; split; first exact/measurable_EFinP/measurable_cst.
       rewrite /= integral_cst//=; last exact: measurable_ball.
       have [r0|r0] := ltP r 0%R.
         by rewrite ((ball0 _ _).2 (ltW r0))// /mu measure0 mule0.
@@ -6983,13 +6981,13 @@ apply: (@le_trans _ _ ((fine (mu (E x n)))^-1%:E *
   rewrite integralD//=.
   - exact: (hE x).1.
   - apply/integrableP; split.
-      by apply/EFin_measurable_fun; case: locf => + _ _; exact: measurable_funS.
+      by apply/measurable_EFinP; case: locf => + _ _; exact: measurable_funS.
     rewrite (@le_lt_trans _ _
       (\int[mu]_(y in closed_ball x (r_ x n)%:num) `|(f y)%:E|))//.
       apply: ge0_subset_integral => //.
       + exact: (hE _).1.
       + exact: measurable_closed_ball.
-      + apply: measurableT_comp => //; apply/EFin_measurable_fun => //.
+      + apply: measurableT_comp => //; apply/measurable_EFinP => //.
         by case: locf => + _ _; exact: measurable_funS.
       + by apply: (subset_trans (E_r_ n)) => //; exact: subset_closed_ball.
     by case: locf => _ _; apply => //; exact: closed_ballR_compact.
@@ -7009,11 +7007,11 @@ rewrite muleA lee_pmul//.
   exact: muEr_.
 - apply: le_trans.
   + apply: le_abse_integral => //; first exact: (hE x).1.
-    apply/EFin_measurable_fun; apply/measurable_funB => //.
+    apply/measurable_EFinP; apply/measurable_funB => //.
     by case: locf => + _ _; exact: measurable_funS.
   + apply: ge0_subset_integral => //; first exact: (hE x).1.
     exact: measurable_ball.
-  + apply/EFin_measurable_fun; apply: measurableT_comp => //.
+  + apply/measurable_EFinP; apply: measurableT_comp => //.
     apply/measurable_funB => //.
     by case: locf => + _ _; exact: measurable_funS.
 Unshelve. all: by end_near. Qed.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index f5bfa3780..e658b9a26 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1431,8 +1431,7 @@ Notation measurable_EFin := EFin_measurable (only parsing).
 Notation measurable_natmul := natmul_measurable (only parsing).
 
 (* NB: real-valued function *)
-(* TODO: rename to measurable_EFin after notation measurable_EFin is removed? *)
-Lemma EFin_measurable_fun d (T : measurableType d) (R : realType) (D : set T)
+Lemma measurable_EFinP d (T : measurableType d) (R : realType) (D : set T)
     (g : T -> R) :
   measurable_fun D (EFin \o g) <-> measurable_fun D g.
 Proof.
@@ -1442,11 +1441,13 @@ rewrite [X in measurable X](_ : _ = D `&` (EFin \o g) @^-1` (EFin @` A)).
 congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]].
 by move=> ? ?; exact: preimage_image.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.6.0", note="use `measurable_EFinP` instead")]
+Notation EFin_measurable_fun := measurable_EFinP (only parsing).
 
 Lemma measurable_fun_dirac
     d {T : measurableType d} {R : realType} D (U : set T) :
   measurable U -> measurable_fun D (fun x => \d_x U : \bar R).
-Proof. by move=> /measurable_fun_indic/EFin_measurable_fun. Qed.
+Proof. by move=> /measurable_fun_indic/measurable_EFinP. Qed.
 
 Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) :
   measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f).
@@ -1456,7 +1457,7 @@ move=> mf;rewrite (_ : er_map _ =
   by apply: funext=> -[].
 apply: measurable_fun_ifT => //=.
 + by apply: (measurable_fun_bool true); exact/emeasurable_fin_num.
-+ exact/EFin_measurable_fun/measurableT_comp.
++ exact/measurable_EFinP/measurableT_comp.
 Qed.
 #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")]
 Notation measurable_fun_er_map := measurable_er_map (only parsing).
diff --git a/theories/probability.v b/theories/probability.v
index 2fbeeb171..e9d54e429 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -175,9 +175,9 @@ Lemma expectation_le (X Y : T -> R) :
 Proof.
 move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //.
 - by move=> t _; apply: X0.
-- exact/EFin_measurable_fun.
+- exact/measurable_EFinP.
 - by move=> t _; apply: Y0.
-- exact/EFin_measurable_fun.
+- exact/measurable_EFinP.
 - move: XY => [N [mN PN XYN]]; exists N; split => // t /= h.
   by apply: XYN => /=; apply: contra_not h; rewrite lee_fin.
 Qed.
@@ -543,7 +543,7 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X)
 - by case => //= r _; exact: f0.
 - move=> [x| |] [y| |]; rewrite !inE/= !in_itv/= ?andbT ?lee_fin ?leey//.
   by move=> ? ? ?; rewrite f_nd.
-- exact/EFin_measurable_fun.
+- exact/measurable_EFinP.
 - by rewrite unlock.
 Qed.
 
@@ -651,7 +651,7 @@ have le (u : R) : (0 <= u)%R ->
   - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
     by apply: emeasurable_funB => //; exact: measurable_int X1.
   - rewrite -[[set _ | _]]setTI inE; apply: emeasurable_fun_c_infty => [//|].
-    rewrite EFin_measurable_fun [X in measurable_fun _ X](_ : _ =
+    rewrite measurable_EFinP [X in measurable_fun _ X](_ : _ =
       (fun x => x ^+ 2) \o (fun x => Y x + u))%R//.
     by apply/measurableT_comp => //; apply/measurable_funD.
   set eps := ((lambda + u) ^ 2)%R.
@@ -1266,7 +1266,7 @@ apply: (@le_trans _ _
 apply: ge0_le_integral => //=.
 - exact: measurableI.
 - by move=> x [Ax]; rewrite /= in_itv/= => axb; rewrite lee_fin uniform_pdf_ge0.
-- by apply/EFin_measurable_fun/measurable_funTS; exact: measurable_uniform_pdf.
+- by apply/measurable_EFinP/measurable_funTS; exact: measurable_uniform_pdf.
 - by move=> x [Ax _]; rewrite lee_fin invr_ge0// ltW// subr_gt0.
 - by move=> x [Ax]; rewrite in_itv/= /uniform_pdf => ->.
 Qed.
@@ -1284,7 +1284,7 @@ move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=.
     by rewrite notin_setE/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->.
   case: ifPn => //.
   by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0.
-- exact/EFin_measurable_fun/measurable_indic.
+- exact/measurable_EFinP/measurable_indic.
 - by move=> x _; rewrite lee_fin.
 - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 Qed.
@@ -1295,10 +1295,10 @@ Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) :
 Proof.
 under [LHS]eq_integral do rewrite fimfunE -fsumEFin//.
 rewrite [LHS]ge0_integral_fsum//; last 2 first.
-  - by move=> r; exact/EFin_measurable_fun/measurableT_comp.
+  - by move=> r; exact/measurable_EFinP/measurableT_comp.
   - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
 rewrite -[RHS]ge0_integralZl//; last 3 first.
-  - exact/EFin_measurable_fun/measurable_funTS.
+  - exact/measurable_EFinP/measurable_funTS.
   - by move=> x _; rewrite lee_fin.
   - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 under [RHS]eq_integral.
@@ -1306,12 +1306,12 @@ under [RHS]eq_integral.
     by move=> r; rewrite EFinM nnfun_muleindic_ge0.
   over.
 rewrite [RHS]ge0_integral_fsum//; last 2 first.
-  - by move=> r; apply/EFin_measurable_fun; do 2 apply/measurableT_comp => //.
+  - by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
   - move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0.
     by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
 - by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA.
-- exact/EFin_measurable_fun/measurableT_comp.
+- exact/measurable_EFinP/measurableT_comp.
 - by move=> t _; rewrite nnfun_muleindic_ge0.
 - by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 Qed.
@@ -1326,23 +1326,23 @@ transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E).
   rewrite -monotone_convergence//=.
   - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=.
     exact: f_f.
-  - by move=> n; exact/EFin_measurable_fun/measurable_funTS.
+  - by move=> n; exact/measurable_EFinP/measurable_funTS.
   - by move=> n ? _; rewrite lee_fin.
   - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/ndf_.
 rewrite [X in _ = (_ * X)%E](_ : _ = lim
     (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first.
   rewrite -monotone_convergence//=.
   - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f.
-  - by move=> n; exact/EFin_measurable_fun/measurable_funTS.
+  - by move=> n; exact/measurable_EFinP/measurable_funTS.
   - by move=> n ? _; rewrite lee_fin.
   - by move=> ? _ ? ? /ndf_ /lefP; rewrite lee_fin.
 rewrite -limeMl//.
   by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun.
 apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=.
 - by move=> ? _; rewrite lee_fin.
-- exact/EFin_measurable_fun/measurable_funTS.
+- exact/measurable_EFinP/measurable_funTS.
 - by move=> ? _; rewrite lee_fin.
-- exact/EFin_measurable_fun/measurable_funTS.
+- exact/measurable_EFinP/measurable_funTS.
 - by move=> ? _; rewrite lee_fin; move/ndf_ : xy => /lefP.
 Qed.