From 4510bf6624cdff6781dd2b1f9de0aa4d101467d9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 9 Oct 2024 20:13:14 +0900
Subject: [PATCH] adding Import numFieldNormedType.Exports. solve the ^o
 problem

---
 theories/charge.v            |   9 +-
 theories/ftc.v               |  74 ++++++-------
 theories/lebesgue_integral.v |  60 +++++------
 theories/lebesgue_measure.v  | 202 +++++++++++++++++------------------
 theories/normedtype.v        |   6 +-
 theories/numfun.v            |   2 +-
 theories/separation_axioms.v |   2 -
 theories/tvs.v               |   1 -
 8 files changed, 175 insertions(+), 181 deletions(-)

diff --git a/theories/charge.v b/theories/charge.v
index 60b403d795..e1f9965f94 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -92,6 +92,7 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
@@ -700,7 +701,7 @@ have nuAoo : 0 <= nu Aoo.
 have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
   rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first.
     by apply/funext => n/=; rewrite fineK// fin_num_measure.
-  apply: continuous_cvg => //; apply: (@cvg_series_cvg_0 _ R^o).
+  apply: continuous_cvg => //; apply: cvg_series_cvg_0.
   rewrite (_ : series _ = fine \o (fun n => \sum_(0 <= i < n) nu (A_ (v i)))); last first.
     apply/funext => n /=.
     by rewrite /series/= sum_fine//= => i _; rewrite fin_num_measure.
@@ -831,7 +832,7 @@ have znuD n : z_ (v n) <= nu D.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
   by rewrite ge_max leeN10 andbT pmule_lle0.
 have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo]  --> 0.
-  move/fine_cvgP => -[zfin] /(@cvgrPdist_lt _ R^o).
+  move/fine_cvgP => -[zfin] /cvgrPdist_lt.
   have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R.
     by rewrite normr_gt0// fine_eq0// ?lt_eqF// fin_num_measure.
   near \oo => n.
@@ -862,7 +863,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
   apply/funext => n/=; rewrite sum_fine// => m _.
   rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT.
   by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0.
-move/(@cvg_series_cvg_0 _ R^o) => maxe_cvg_0.
+move/cvg_series_cvg_0 => maxe_cvg_0.
 apply: not_s_cvg_0.
 rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first.
   by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE.
@@ -874,7 +875,7 @@ apply/fine_cvgP; split.
   rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split.
     by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx.
   by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0.
-apply/(@cvgrPdist_lt _ R^o) => _ /posnumP[e].
+apply/cvgrPdist_lt => _ /posnumP[e].
 have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT.
 move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.
diff --git a/theories/ftc.v b/theories/ftc.v
index 0ff23d7b27..2d944d434e 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -25,6 +25,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -36,7 +37,7 @@ Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
-  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
+  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
     h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x.
 Proof.
@@ -79,7 +80,7 @@ apply: cvg_at_right_left_dnbhs.
         by apply/negP; rewrite negb_and -!leNgt xz orbT.
       - by apply/negP; rewrite -leNgt.
   rewrite [f in f n @[n --> _] --> _](_ : _ =
-      fun n => (d n)^-1 *: (fine (\int[mu]_(t in E x n) (f t)%:E) : R^o)); last first.
+      fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
     apply/funext => n; congr (_ *: _); rewrite -fineB/=.
     by rewrite /= (addrC (d n) x) ixdf.
     by apply: integral_fune_fin_num => //; exact: integrableS intf.
@@ -106,7 +107,7 @@ apply: cvg_at_right_left_dnbhs.
   have nice_E y : nicely_shrinking y (E y).
     split=> [n|]; first exact: measurable_itv.
     exists (2, (fun n => PosNum (Nd_gt0 n))); split => //=.
-      by rewrite -oppr0; exact: (@cvgN _ R^o).
+      by rewrite -oppr0; exact: cvgN.
     move=> n z.
       rewrite /E/= in_itv/= /ball/= => /andP[yz zy].
       by rewrite ltr_distlC opprK yz /= (le_lt_trans zy)// ltrDl.
@@ -141,7 +142,7 @@ apply: cvg_at_right_left_dnbhs.
         rewrite /E /= !in_itv/= leNgt => xdnz.
         by apply/negP; rewrite negb_and xdnz.
     move=> b a ax.
-    move/(@cvgrPdist_le _ R^o) : d0.
+    move/cvgrPdist_le : d0.
     move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
     near=> n.
     have mn : (m <= n)%N by near: n; exists m.
@@ -170,7 +171,7 @@ apply: cvg_at_right_left_dnbhs.
       by apply/negP; rewrite negb_and -leNgt zxdn.
   suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R
           @[n --> \oo] --> f x.
-    apply: cvg_trans; apply: near_eq_cvg; near=> n;  congr (_ *: (_ : R^o)).
+    apply: cvg_trans; apply: near_eq_cvg; near=> n;  congr (_ *: _).
     rewrite /F -fineN -fineB; last 2 first.
       by apply: integral_fune_fin_num => //; exact: integrableS intf.
       by apply: integral_fune_fin_num => //; exact: integrableS intf.
@@ -188,9 +189,9 @@ Unshelve. all: by end_near. Qed.
 
 Let FTC0_restrict f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
-  let F y : R^o := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
+  let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
   a < BRight x -> lebesgue_pt f x ->
-  h^-1 *: (F (h + x) - F x) @[h --> ((0:R^o)%R^')] --> f x.
+  h^-1 *: (F (h + x) - F x) @[h --> ((0:R)%R^')] --> f x.
 Proof.
 move=> xu + F ax fx.
 rewrite integrable_mkcond//= (restrict_EFin f) => intf.
@@ -204,8 +205,7 @@ apply: cvg_trans; apply: near_eq_cvg; near=> r; congr (_ *: (_ - _)).
   move: yaxr; rewrite /= !in_itv/= inE/= in_itv/= => /andP[->/=].
   move=> /le_trans; apply; rewrite -lerBrDr.
   have [r0|r0] := leP r 0%R; first by rewrite (le_trans r0)// subr_ge0 ltW.
-  rewrite -(gtr0_norm r0); near: r.
-  by apply: (@dnbhs0_le _ R^o); rewrite subr_gt0.
+  by rewrite -(gtr0_norm r0); near: r; apply: dnbhs0_le; rewrite subr_gt0.
 - apply: eq_Rintegral => y yaxr; rewrite patchE mem_set//=.
   move: yaxr => /=; rewrite !in_itv/= inE/= in_itv/= => /andP[->/=].
   by move=> /le_trans; apply; exact/ltW.
@@ -214,9 +214,9 @@ Unshelve. all: by end_near. Qed.
 (* NB: right-closed interval *)
 Lemma FTC1_lebesgue_pt f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
-  let F (y : R^o) := (\int[mu]_(t in [set` Interval a (BRight y)]) (f t))%R in
+  let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) (f t))%R in
   a < BRight x -> lebesgue_pt f x ->
-  derivable  (F : R^o -> R^o) x 1 /\ ((F : R^o -> R^o)^`() x = f x).
+  derivable F x 1 /\ F^`() x = f x.
 Proof.
 move=> xu intf F ax fx; split; last first.
   by apply/cvg_lim; [exact: Rhausdorff|exact: (@FTC0_restrict _ _ _ u)].
@@ -231,8 +231,8 @@ Qed.
 Corollary FTC1 f a :
   (forall y, mu.-integrable [set` Interval a (BRight y)] (EFin \o f)) ->
   locally_integrable [set: R] f ->
-  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
-  {ae mu, forall x, a < BRight x -> derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}.
+  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}.
 Proof.
 move=> intf locf F; move: (locf) => /lebesgue_differentiation.
 apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
@@ -243,15 +243,15 @@ Qed.
 Corollary FTC1Ny f :
   (forall y, mu.-integrable `]-oo, y] (EFin \o f)) ->
   locally_integrable [set: R] f ->
-  let F x : R^o := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
-  {ae mu, forall x, derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x}.
+  let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
+  {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}.
 Proof.
 move=> intf locf F; have := FTC1 intf locf.
 apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
 by move=> r /=; apply; rewrite ltNyr.
 Qed.
 
-Let itv_continuous_lebesgue_pt f a (x : R^o) (u : R) : (x < u)%R ->
+Let itv_continuous_lebesgue_pt f a x (u : R) : (x < u)%R ->
   measurable_fun [set` Interval a (BRight u)] f ->
   a < BRight x ->
   {for x, continuous f} -> lebesgue_pt f x.
@@ -259,7 +259,7 @@ Proof.
 move=> xu fi + fx.
 move: a fi => [b a fi /[1!(@lte_fin R)] ax|[|//] fi _].
 - near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)) => //.
-  + exact: (ball_open_nbhs x).
+  + exact: ball_open_nbhs.
   + exact: measurable_ball.
   + apply: measurable_funS fi => //; rewrite ball_itv.
     apply: (@subset_trans _ `](x - e)%R, u]) => //.
@@ -279,9 +279,9 @@ Unshelve. all: by end_near. Qed.
 
 Corollary continuous_FTC1 f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
-  let F x : R^o := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   a < BRight x -> {for x, continuous f} ->
-  derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x.
+  derivable F x 1 /\ F^`() x = f x.
 Proof.
 move=> xu fi F ax fx; suff lfx : lebesgue_pt f x.
   have /(_ ax lfx)[dfx f'xE] := @FTC1_lebesgue_pt _ a _ _ xu fi.
@@ -292,9 +292,9 @@ Qed.
 
 Corollary continuous_FTC1_closed f (a x : R) (u : R) : (x < u)%R ->
   mu.-integrable `[a, u] (EFin \o f) ->
-  let F x : R^o := (\int[mu]_(t in [set` `[a, x]]) (f t))%R in
+  let F x := (\int[mu]_(t in [set` `[a, x]]) (f t))%R in
   (a < x)%R -> {for x, continuous f} ->
-  derivable (F : R^o -> R^o) x 1 /\ F^`() x = f x.
+  derivable F x 1 /\ F^`() x = f x.
 Proof. by move=> xu locf F ax fx; exact: (@continuous_FTC1 _ _ _ u). Qed.
 
 End FTC.
@@ -359,7 +359,7 @@ Proof.
 move=> ab intf; pose fab := f \_ `[a, b].
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
-apply/(@cvgrPdist_le _ R^o) => /= e e0; near=> x.
+apply/cvgrPdist_le => /= e e0; near=> x.
 rewrite {1}/int /parameterized_integral sub0r normrN.
 have [|xa] := leP a x.
   move=> ax; apply/ltW; move: ax.
@@ -379,7 +379,7 @@ have /= int_normr_cont : forall e : R, 0 < e ->
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setTI.
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
-rewrite /int /parameterized_integral; apply/(@cvgrPdist_le _ R^o) => /= e e0.
+rewrite /int /parameterized_integral; apply/cvgrPdist_le => /= e e0.
 have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//;
@@ -423,7 +423,7 @@ have /= int_normr_cont : forall e : R, 0 < e ->
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr.
 rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb].
-apply/(@cvgrPdist_le _ R^o) => /= e e0.
+apply/cvgrPdist_le => /= e e0.
 have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW.
@@ -493,7 +493,7 @@ rewrite mem_set ?mulr1 /=; last exact: subset_itv_oo_cc.
 exact: cvg_patch.
 Qed.
 
-Corollary continuous_FTC2 (f F : R^o -> R^o) a b : (a < b)%R ->
+Corollary continuous_FTC2 f F a b : (a < b)%R ->
   {within `[a, b], continuous f} ->
   derivable_oo_continuous_bnd F a b ->
   {in `]a, b[, F^`() =1 f} ->
@@ -501,7 +501,7 @@ Corollary continuous_FTC2 (f F : R^o -> R^o) a b : (a < b)%R ->
 Proof.
 move=> ab cf dF F'f.
 pose fab := f \_ `[a, b].
-pose G (x : R^o) : R^o := (\int[mu]_(t in `[a, x]) fab t)%R.
+pose G x := (\int[mu]_(t in `[a, x]) fab t)%R.
 have iabf : mu.-integrable `[a, b] (EFin \o f).
   by apply: continuous_compact_integrable => //; exact: segment_compact.
 have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}.
@@ -528,11 +528,11 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}.
         + by move: yab; rewrite in_itv/= => /andP[_ /ltW].
       have Fz1 : derivable F z 1.
         by case: dF => /= + _ _; apply; rewrite inE in zab.
-      have Gz1 : derivable (G : R^o -> R^o) z 1 by have [|] := G'f z.
+      have Gz1 : derivable G z 1 by have [|] := G'f z.
       apply: DeriveDef.
       + by apply: derivableB; [exact: Fz1|exact: Gz1].
       + by rewrite deriveB -?derive1E; [by []|exact: Fz1|exact: Gz1].
-    - apply: (@derivable_within_continuous _ R^o) => z zxy.
+    - apply: derivable_within_continuous => z zxy.
       apply: derivableB.
       + case: dF => /= + _ _; apply.
         apply: subset_itvSoo zxy => //.
@@ -572,7 +572,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
   by apply/funext => x/=; rewrite subrK.
 have contF : {within `[a, b], continuous F}.
   apply/(continuous_within_itvP _ ab); split => //.
-  move=> z zab; apply/(@differentiable_continuous _ R^o R^o)/derivable1_diffP.
+  move=> z zab; apply/differentiable_continuous/derivable1_diffP.
   by case: dF => /= + _ _; exact.
 have iabfab : mu.-integrable `[a, b] (EFin \o fab).
   by rewrite -restrict_EFin; apply/integrable_restrict => //; rewrite setIidr.
@@ -603,7 +603,7 @@ Notation mu := lebesgue_measure.
 Local Open Scope ereal_scope.
 Implicit Types (F G f g : R -> R) (a b : R).
 
-Lemma integration_by_parts (F : R^o -> R^o) (G : R^o -> R^o) (f g : R^o -> R^o) a b : (a < b)%R ->
+Lemma integration_by_parts F G f g a b : (a < b)%R ->
     {within `[a, b], continuous f} ->
     derivable_oo_continuous_bnd F a b ->
     {in `]a, b[, F^`() =1 f} ->
@@ -615,7 +615,7 @@ Lemma integration_by_parts (F : R^o -> R^o) (G : R^o -> R^o) (f g : R^o -> R^o)
 Proof.
 move=> ab cf Fab Ff cg Gab Gg.
 have cfg : {within `[a, b], continuous (f * G + F * g)%R}.
-apply/subspace_continuousP => x abx; apply:cvgD .
+  apply/subspace_continuousP => x abx; apply: cvgD.
   - apply: cvgM.
     + by move/subspace_continuousP : cf; exact.
     + have := derivable_oo_continuous_bnd_within Gab.
@@ -655,7 +655,7 @@ Context {R : realType}.
 Notation mu := lebesgue_measure.
 Implicit Types (F G f g : R -> R) (a b : R).
 
-Lemma Rintegration_by_parts (F G : R^o -> R^o) f g a b :
+Lemma Rintegration_by_parts F G f g a b :
     (a < b)%R ->
     {within `[a, b], continuous f} ->
     derivable_oo_continuous_bnd F a b ->
@@ -730,7 +730,7 @@ Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab incrF cFb GFb.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
+have /cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb.
 have := cvg_at_left_within cFb.
 move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb].
 near=> t.
@@ -748,7 +748,7 @@ Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab decrF cFa GFa.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
+have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa.
 have := cvg_at_right_within cFa.
 move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa].
 near=> t.
@@ -766,7 +766,7 @@ Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R ->
 Proof.
 move=> ab decrF cFb GFb.
 apply/cvgrPdist_le => /= e e0.
-have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
+have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb.
 have := cvg_at_left_within cFb. (* different point from gt0 version *)
 move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb].
 near=> t.
@@ -863,7 +863,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
       exact: decreasing_image_oo.
     * have : -%R F^`() @ x --> (- f x)%R.
         by rewrite -fE//; apply: cvgN; exact: cF'.
-      apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl.
+      apply: cvg_trans; apply: near_eq_cvg.
       apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE.
         exact: interval_open.
       by move=> z; rewrite inE/= => zab; rewrite fctE fE.
@@ -978,7 +978,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last.
     by case: Fab => + _ _; exact.
   rewrite -derive1E.
   have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg.
-  rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//.
+  near=> y; rewrite fctE !derive1E deriveN//.
   by case: Fab => + _ _; apply; near: y; exact: near_in_itv.
 - by move=> x y xab yab yx; rewrite ltrN2 incrF.
 - by [].
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 5949d7338d..28b581bd6a 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -83,6 +83,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
@@ -441,7 +442,7 @@ Qed.
 Section simple_bounded.
 Context d (T : sigmaRingType d) (R : realType).
 
-Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun (f : _ -> R^o).
+Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.
 Proof.
 have /finite_seqP[r fr] := fimfunP f.
 exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
@@ -1671,6 +1672,7 @@ Qed.
 End approximation_sfun.
 
 Section lusin.
+Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core.
 Local Open Scope ereal_scope.
 Context (rT : realType) (A : set rT).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
@@ -3097,7 +3099,7 @@ case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDl.
 Qed.
 
-Lemma integrableMr (h : T -> R^o) g :
+Lemma integrableMr (h : T -> R) g :
   measurable_fun D h -> [bounded h x | x in D] ->
   mu_int g -> mu_int ((EFin \o h) \* g).
 Proof.
@@ -3117,7 +3119,7 @@ apply/le_lt_trans/ge0_le_integral => //.
   by rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
 Qed.
 
-Lemma integrableMl f (h : T -> R^o) :
+Lemma integrableMl f (h : T -> R) :
   mu_int f -> measurable_fun D h -> [bounded h x | x in D] ->
   mu_int (f \* (EFin \o h)).
 Proof.
@@ -5729,7 +5731,7 @@ Let R  := [the measurableType _ of measurableTypeR rT].
 Let ballE (x : R) (r : {posnum rT}) :
   ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT.
 Proof.
-rewrite -(@ball_normE _ rT^o) /ball_ set_itvoo.
+rewrite -ball_normE /ball_ set_itvoo.
 by under eq_set => ? do rewrite ltr_distlC.
 Qed.
 
@@ -5753,7 +5755,7 @@ have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E.
   rewrite ler_ltD // ?rE // -EFinD; congr (_ _).
   by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
 move=> oA intf ctsfx Ax.
-apply: (@cvg_zero _ R^o).
+apply: cvg_zero.
 apply/cvgrPdist_le => eps epos; apply: filter_app (@nbhs_right_gt rT 0).
 move/cvgrPdist_le/(_ eps epos)/at_right_in_segment : ctsfx; apply: filter_app.
 apply: filter_app (open_itvcc_subset oA Ax).
@@ -6017,7 +6019,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
     rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW.
     by rewrite ltry andbT lte_fin pmulrn_lgt0// addr_gt0.
   exists (ball x d).
-    by split; [exact: (@ball_open _ R^o)|exact: ballxx].
+    by split; [exact: ball_open|exact: ballxx].
   move=> y; rewrite /ball/= => xyd.
   have ? : ball x r `<=` ball y (r + d).
     move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
@@ -6055,7 +6057,7 @@ have axrdk : a%:E < (fine (mu (ball x (r + d))))^-1%:E * k.
   rewrite -mulr_natl -ltr_pdivlMl// -ltrBrDl.
   by near: d; exact: nbhs_right_lt.
 exists (ball x d).
-  by split; [exact: (@ball_open _ R^o)|exact: ballxx].
+  by split; [exact: ball_open|exact: ballxx].
 move=> y; rewrite /ball/= => xyd.
 have ? : ball x r `<=` ball y (r + d).
   move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
@@ -6117,7 +6119,7 @@ have {}Kcmf : K `<=` cover [set i | HL f i > c%:E] (fun i => ball i (r_ i)).
 have {Kcmf}[D Dsub Kcover] : finite_subset_cover [set i | c%:E < HL f i]
     (fun i => ball i (r_ i)) K.
   move: cK; rewrite compact_cover => /(_ _ _ _ _ Kcmf); apply.
-  by move=> /= x cMfx; exact/(@ball_open _ R^o)/r_pos.
+  by move=> /= x cMfx; exact/ball_open/r_pos.
 have KDB : K `<=` cover [set` D] B.
   by apply: (subset_trans Kcover) => /= x [r Dr] rx; exists r.
 have is_ballB i : is_ball (B i) by exact: is_ball_ball.
@@ -6216,16 +6218,14 @@ Let continuous_integralB_fin_num :
   \forall t \near (0:R)%R,
     \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| \is a fin_num.
 Proof.
-move: fx => /(@cvgrPdist_le _ R^o) /= fx'.
+move: fx => /cvgrPdist_le /= fx'.
 near (0%R:R)^'+ => e.
 have e0 : (0 < e)%R by near: e; exact: nbhs_right_gt.
 have [r /= r0 {}fx'] := fx' _ e0.
-have [d/= d0 dxU] := @open_subball _ R^o _ _ xU.1 xU.2.
+have [d/= d0 dxU] := open_subball xU.1 xU.2.
 near=> t; rewrite ge0_fin_numE ?integral_ge0//.
 have [t0|t0] := leP t 0%R; first by rewrite ((ball0 _ _).2 t0) integral_set0.
-have xtU : ball x t `<=` U.
-  apply: dxU => //=.
-  by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o).
+have xtU : ball x t `<=` U by apply: dxU => //=.
 rewrite (@le_lt_trans _ _ (\int[mu]_(y in ball x t) e%:E))//; last first.
   rewrite integral_cst//=; last exact: measurable_ball.
   by rewrite (lebesgue_measure_ball _ (ltW t0)) ltry.
@@ -6241,37 +6241,33 @@ Let continuous_davg_fin_num :
   \forall A \near (0:R)%R, davg f x A \is a fin_num.
 Proof.
 have [e /= e0 exf] := continuous_integralB_fin_num.
-move: fx => /(@cvgrPdist_le _ R^o) fx'.
+move: fx => /cvgrPdist_le fx'.
 near (0%R:R)^'+ => r.
 have r0 : (0 < r)%R by near: r; exact: nbhs_right_gt.
 have [d /= d0 {}fx'] := fx' _ e0.
 near=> t; have [t0|t0] := leP t 0%R; first by rewrite davg0.
-rewrite fin_numM// exf//=.
-by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o).
+by rewrite fin_numM// exf/=.
 Unshelve. all: by end_near. Qed.
 
 Lemma continuous_cvg_davg : davg f x r @[r --> (0:R)%R] --> 0.
 Proof.
 apply/fine_cvgP; split; first exact: continuous_davg_fin_num.
-apply/(@cvgrPdist_le _ R^o) => e e0.
-move: fx => /(@cvgrPdist_le _ R^o) /= fx'.
+apply/cvgrPdist_le => e e0.
+move: fx => /cvgrPdist_le /= fx'.
 have [r /= r0 {}fx'] := fx' _ e0.
 have [d /= d0 dfx] := continuous_davg_fin_num.
-have [l/= l0 lxU] := @open_subball _ R^o _ _ xU.1 xU.2.
+have [l/= l0 lxU] := open_subball xU.1 xU.2.
 near=> t.
 have [t0|t0] := leP t 0%R; first by rewrite /= davg0//= subrr normr0 ltW.
 rewrite sub0r normrN /= ger0_norm; last by rewrite fine_ge0// davg_ge0.
-rewrite -lee_fin fineK//; last first.
-  rewrite dfx//=.
-  by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o).
+rewrite -lee_fin fineK//; last by rewrite dfx//= sub0r normrN gtr0_norm.
 rewrite /davg/= /iavg/= lee_pdivrMl//; last first.
   by rewrite fine_gt0// lebesgue_measure_ball// ?ltry ?lte_fin ?mulrn_wgt0 ?ltW.
 rewrite (@le_trans _ _ (\int[mu]_(y in ball x t) e%:E))//.
   apply: ge0_le_integral => //=.
   - exact: measurable_ball.
   - do 2 apply: measurableT_comp => //=; apply: measurable_funB => //.
-    apply: measurable_funS mUf => //; apply: lxU => //=.
-    by rewrite /ball_ /= sub0r normrN; near: t; exact: (@nbhs0_lt _ R^o).
+    by apply: measurable_funS mUf => //; apply: lxU => //=.
   - by move=> y xty; rewrite lee_fin ltW.
   - move=> y xty; rewrite lee_fin distrC fx'//; apply: (lt_le_trans xty).
     by near: t; exact: nbhs0_ltW.
@@ -6301,7 +6297,7 @@ Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U ->
 Proof.
 move=> xU mY mf /= mg; apply: le_trans (lime_supD _); last first.
   by rewrite ge0_adde_def// inE; exact: lim_sup_davg_ge0.
-have [e/= e0 exU] := @open_subball _ R^o _ _ xU.1 xU.2.
+have [e/= e0 exU] := open_subball xU.1 xU.2.
 apply: lime_sup_le; near=> r => y; rewrite neq_lt => /orP[y0|y0 ry].
   by rewrite !davg0 ?adde0// ltW.
 apply: davgD.
@@ -6331,7 +6327,7 @@ move=> xU mU mUf cg locg; apply/eqP; rewrite eq_le; apply/andP; split.
   rewrite (@continuous_lim_sup_davg (- g)%R _ _ xU mU); first by rewrite adde0.
   - apply/(measurable_comp measurableT) => //.
     by case: locg => + _ _; apply: measurable_funS.
-  + by move=> y; exact/(@continuousN _ R^o)/cg.
+  + by move=> y; exact/continuousN/cg.
 - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//.
     rewrite {1}(_ : f = f \- g + g)%R; last by apply/funext => y; rewrite subrK.
     apply: (lim_sup_davg_le xU mU).
@@ -6345,7 +6341,7 @@ Qed.
 Local Notation mu := (@lebesgue_measure R).
 
 Let is_cvg_ereal_sup_davg f x :
-  cvg (ereal_sup [set davg f x y | y in @ball _ R^o 0%R e `\ 0%R] @[e --> 0^'+]).
+  cvg (ereal_sup [set davg f x y | y in ball 0%R e `\ 0%R] @[e --> 0^'+]).
 Proof.
 apply: nondecreasing_at_right_is_cvge; near=> e => y z.
 rewrite !in_itv/= => /andP[y0 ye] /andP[z0 ze] yz.
@@ -6626,7 +6622,7 @@ have {ex_g_} ex_gn n : exists gn : R -> R,
     [/\ continuous gn,
         mu.-integrable (B k) (EFin \o gn) &
         \int[mu]_(z in B k) `|f_ k z - gn z|%:E <= n.+1%:R^-1%:E].
-  case: ex_g_ => g_ [cg intg] /fine_cvgP[] [m _ fgfin] /(@cvgrPdist_le _ R^o).
+  case: ex_g_ => g_ [cg intg] /fine_cvgP[] [m _ fgfin] /cvgrPdist_le.
   move=> /(_ n.+1%:R^-1 ltac:(by []))[p _] /(_ _ (leq_addr m p)).
   rewrite sub0r normrN -lee_fin => /= fg0.
   exists (g_ (p + m)%N); split => //.
@@ -6694,11 +6690,11 @@ have davgfEe : B k `&` [set x | (f_ k)^* x > e%:E] `<=` Ee.
       B k `&` [set x | e%:E < (f_ k \- g_B n)%R^* x]); last first.
     apply/seteqP; split => [x [Ex] /=|x [Ex] /=].
       rewrite (@lim_sup_davgB _ _ _ _ (B k))//.
-      by split; [exact: (@ball_open _ R^o)|exact: Ex].
+      by split; [exact: ball_open|exact: Ex].
       by move/EFin_measurable_fun : mf; apply: measurable_funS.
       by apply: cg_B; rewrite inE.
     rewrite (@lim_sup_davgB _ _ _ _ (B k))//.
-    by split; [exact: (@ball_open _ R^o)|exact: Ex].
+    by split; [exact: ball_open|exact: Ex].
     by move/EFin_measurable_fun : mf; apply: measurable_funS.
     by apply: cg_B; rewrite inE.
   move=> r /= [Er] efgnr; split => //.
@@ -6780,7 +6776,7 @@ suff: ~` [set x | lebesgue_pt f x] `<=`
   by apply: negligible_bigcup => k /=; exact: suf.
 move=> x /= fx; rewrite -setC_bigcap => h; apply: fx.
 have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
-    forall t : R^o, ball y r t -> f t = fk k t.
+    forall t, ball y r t -> f t = fk k t.
   rewrite /ball/= sub0r normrN => yk1 r1 t.
   rewrite ltr_distlC => /andP[xrt txr].
   rewrite /fk patchE mem_set// /B /ball/= sub0r normrN.
@@ -6812,7 +6808,7 @@ apply/fine_cvgP; split=> [{davg_fk0}|{davg_fk_fin_num}].
 - move: davg_fk_fin_num => -[M /= M0] davg_fk_fin_num.
   apply: filter_app f_fk_ceil; near=> t => Ht.
   by rewrite /davg /iavg Ht davg_fk_fin_num//= sub0r normrN gtr0_norm.
-- move/(@cvgrPdist_le _ R^o) in davg_fk0; apply/(@cvgrPdist_le _ R^o) => e e0.
+- move/cvgrPdist_le in davg_fk0; apply/cvgrPdist_le => e e0.
   have [M /= M0 {}davg_fk0] := davg_fk0 _ e0.
   apply: filter_app f_fk_ceil; near=> t; move=> Ht.
   by rewrite /davg /iavg Ht// davg_fk0//= sub0r normrN gtr0_norm.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 4a3e05af4f..bdd6263f30 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -62,6 +62,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -918,7 +919,7 @@ Implicit Types D : set R.
 Lemma oppr_measurable D : measurable_fun D -%R.
 Proof.
 apply: measurable_funTS => /=; apply: continuous_measurable_fun.
-exact: (@opp_continuous _ R^o).
+exact: opp_continuous.
 Qed.
 
 Lemma normr_measurable D : measurable_fun D (@normr _ R).
@@ -1109,8 +1110,8 @@ move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x).
 apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))).
   by move=> x; rewrite inE => Dx; rewrite -fE.
 apply: (@measurable_fun_limn_sup _ h) => // t Dt.
-- by apply/bounded_fun_has_ubound/(@cvg_seq_bounded _ R^o)/cvg_ex; eexists; exact: f_f.
-- by apply/bounded_fun_has_lbound/(@cvg_seq_bounded _ R^o)/cvg_ex; eexists; exact: f_f.
+- by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f.
+- by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f.
 Qed.
 
 Lemma measurable_fun_indic D (U : set T) : measurable U ->
@@ -1627,6 +1628,100 @@ Qed.
 
 End open_itv_cover.
 
+Section egorov.
+Context d {R : realType} {T : measurableType d}.
+Context (mu : {measure set T -> \bar R}).
+
+Local Open Scope ereal_scope.
+
+(*TODO : this generalizes to any metric space with a borel measure*)
+Lemma pointwise_almost_uniform
+    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
+  (forall n, measurable_fun A (f n)) ->
+  measurable A -> mu A < +oo -> (forall x, A x -> f ^~ x @ \oo --> g x) ->
+  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
+    {uniform A `\` B, f @ \oo --> g}].
+Proof.
+move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R.
+have mfunh q : measurable_fun A (h q).
+  apply: measurableT_comp => //; apply: measurable_funB => //.
+  exact: measurable_fun_cvg.
+pose E k n := \bigcup_(i >= n) (A `&` [set x | h i x >= k.+1%:R^-1]%R).
+have Einc k : nonincreasing_seq (E k).
+  move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?].
+  by exists i => //; exact: mi.
+have mE k n : measurable (E k n).
+  apply: bigcup_measurable => q /= ?.
+  have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[.
+    by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT.
+  exact: mfunh.
+have nEcvg x k : exists n, A x -> (~` E k n) x.
+  have [Ax|?] := pselect (A x); last by exists point.
+  have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)).
+    by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
+  move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
+  apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
+  by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
+have Ek0 k : \bigcap_n (E k n) = set0.
+  rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by [].
+  rewrite setC_bigcap; have [Az | nAz] := pselect (A z).
+    by have [N /(_ Az) ?] := nEcvg z k; exists N.
+  by exists 0%N => //; rewrite setC_bigcup => n _ [].
+have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E.
+  pose ek : R := eps / 2 / (2 ^ k.+1)%:R.
+  have : mu \o E k @ \oo --> mu set0.
+    rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //.
+    - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
+    - exact: bigcap_measurable.
+  rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))).
+    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
+    by rewrite !divr_gt0.
+  move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
+  rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
+  by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
+pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k E k (badn k)); split.
+- exact: bigcup_measurable.
+- apply: (@le_lt_trans _ _ (eps / 2)%:E); first last.
+    by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1.
+  apply: le_trans.
+    apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //.
+    exact: bigcup_measurable.
+  apply: le_trans; first last.
+    by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// ltW.
+  by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))).
+apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT.
+case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU.
+have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
+exists (badn N) => // r badNr x.
+rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel).
+move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I).
+rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//.
+by move/negP; rewrite ltNge // distrC.
+Qed.
+
+Lemma ae_pointwise_almost_uniform
+    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
+  (forall n, measurable_fun A (f n)) -> measurable_fun A g ->
+  measurable A -> mu A < +oo ->
+  {ae mu, (forall x, A x -> f ^~ x @ \oo --> g x)} ->
+  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
+    {uniform A `\` B, f @ \oo --> g}].
+Proof.
+move=> mf mg mA Afin [C [mC C0 nC] epspos].
+have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
+    {uniform (A `\` C) `\` B,  f @\oo --> g}].
+  apply: pointwise_almost_uniform => //.
+  - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
+  - by apply: measurableI => //; exact: measurableC.
+  - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
+  - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact.
+exists (B `|` C); split.
+- exact: measurableU.
+- by apply: (le_lt_trans _ Beps); rewrite measureU0.
+- by rewrite setUC -setDDl.
+Qed.
+
+End egorov.
 
 (* This module contains a direct construction of the Lebesgue measure that is
    kept here for archival purpose. The Lebesgue measure is actually defined as
@@ -2647,101 +2742,6 @@ Qed.
 
 End lebesgue_regularity.
 
-Section egorov.
-Context d {R : realType} {T : measurableType d}.
-Context (mu : {measure set T -> \bar R}).
-
-Local Open Scope ereal_scope.
-
-(*TODO : this generalizes to any metric space with a borel measure*)
-Lemma pointwise_almost_uniform
-    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
-  (forall n, measurable_fun A (f n)) ->
-  measurable A -> mu A < +oo -> (forall x, A x -> f ^~ x @ \oo --> g x) ->
-  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
-    {uniform A `\` B, f @ \oo --> g}].
-Proof.
-move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R.
-have mfunh q : measurable_fun A (h q).
-  apply: measurableT_comp => //; apply: measurable_funB => //.
-  exact: measurable_fun_cvg.
-pose E k n := \bigcup_(i >= n) (A `&` [set x | h i x >= k.+1%:R^-1]%R).
-have Einc k : nonincreasing_seq (E k).
-  move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?].
-  by exists i => //; exact: mi.
-have mE k n : measurable (E k n).
-  apply: bigcup_measurable => q /= ?.
-  have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[.
-    by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT.
-  exact: mfunh.
-have nEcvg x k : exists n, A x -> (~` E k n) x.
-  have [Ax|?] := pselect (A x); last by exists point.
-  have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)).
-    by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
-  move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
-  apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
-  by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
-have Ek0 k : \bigcap_n (E k n) = set0.
-  rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by [].
-  rewrite setC_bigcap; have [Az | nAz] := pselect (A z).
-    by have [N /(_ Az) ?] := nEcvg z k; exists N.
-  by exists 0%N => //; rewrite setC_bigcup => n _ [].
-have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E.
-  pose ek : R := eps / 2 / (2 ^ k.+1)%:R.
-  have : mu \o E k @ \oo --> mu set0.
-    rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //.
-    - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
-    - exact: bigcap_measurable.
-  rewrite measure0; case/fine_cvg/(_ (@interior R^o (ball 0%R ek))).
-    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
-    by rewrite !divr_gt0.
-  move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
-  rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
-  by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
-pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k E k (badn k)); split.
-- exact: bigcup_measurable.
-- apply: (@le_lt_trans _ _ (eps / 2)%:E); first last.
-    by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1.
-  apply: le_trans.
-    apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //.
-    exact: bigcup_measurable.
-  apply: le_trans; first last.
-    by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// ltW.
-  by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))).
-apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT.
-case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU.
-have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
-exists (badn N) => // r badNr x.
-rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel).
-move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I).
-rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//.
-by move/negP; rewrite ltNge // distrC.
-Qed.
-
-Lemma ae_pointwise_almost_uniform
-    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
-  (forall n, measurable_fun A (f n)) -> measurable_fun A g ->
-  measurable A -> mu A < +oo ->
-  {ae mu, (forall x, A x -> f ^~ x @ \oo --> g x)} ->
-  (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E &
-    {uniform A `\` B, f @ \oo --> g}].
-Proof.
-move=> mf mg mA Afin [C [mC C0 nC] epspos].
-have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
-    {uniform (A `\` C) `\` B,  f @\oo --> g}].
-  apply: pointwise_almost_uniform => //.
-  - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
-  - by apply: measurableI => //; exact: measurableC.
-  - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
-  - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact.
-exists (B `|` C); split.
-- exact: measurableU.
-- by apply: (le_lt_trans _ Beps); rewrite measureU0.
-- by rewrite setUC -setDDl.
-Qed.
-
-End egorov.
-
 Definition vitali_cover {R : realType} (E : set R) I
     (B : I -> set R) (D : set I) :=
   (forall i, is_ball (B i)) /\
@@ -2900,7 +2900,7 @@ have [N F5e] : exists N, \sum_(N <= n <oo) \esum_(i in F n) mu (closure (B i)) <
     + by apply: sub_trivIset tDB => // x [].
   have : \sum_(N <= k <oo) (mu \o f) k @[N --> \oo] --> 0.
     exact: nneseries_tail_cvg.
-  rewrite /f /= => /fine_fcvg /= /(@cvgrPdist_lt _ R^o) /=.
+  rewrite /f /= => /fine_fcvg /= /cvgrPdist_lt /=.
   have : (0 < 5%:R^-1 * e%:num)%R by rewrite mulr_gt0// invr_gt0// ltr0n.
   move=> /[swap] /[apply].
   rewrite near_map => -[N _]/(_ _ (leqnn N)) h; exists N; move: h.
@@ -2931,7 +2931,7 @@ have ZNF5 : Z r%:num `<=`
     case: Zz => -[Az notDBz]; rewrite /ball/= sub0r normrN => rz.
     have [d dzr zdK0] : exists2 d : {posnum R},
         (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0.
-      have [d/= d0 dzK] := @closed_disjoint_closed_ball _ R^o _ _ closedK Kz.
+      have [d/= d0 dzK] := closed_disjoint_closed_ball closedK Kz.
       have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R.
         by rewrite lt_min (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
       exists (PosNum rz0) => /=.
@@ -2956,7 +2956,7 @@ have ZNF5 : Z r%:num `<=`
         by rewrite (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW.
       by move: dzr; rewrite -ltrBrDr.
     apply: subsetI_eq0 zdK0 => // y Biy.
-    rewrite (@closed_ballE _ R^o)//= /closed_ball_/=.
+    rewrite closed_ballE//= /closed_ball_/=.
     rewrite -(@subrK _ (cpoint (B i)) z) -(addrA (z - _)%R).
     rewrite (le_trans (ler_normD _ _))// [in leRHS](splitr d%:num) lerD//.
       by rewrite distrC (le_trans (ltW (is_ballP (is_ballB i) Biz)))// ltW.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 94c119a6bd..f71af3fe64 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -837,7 +837,7 @@ rewrite !nbhs_simpl /=; split; by apply: nbhsx_ballx; rewrite ?divr_gt0.
 rewrite -ball_normE /= /ball_ /= => xy /= [nx ny].
 rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (@splitr K (e)) ltrD //=.
 Qed.
- 
+
 Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
 Proof.
 move=> [/= k x].
@@ -914,7 +914,8 @@ HB.end.
 
 Section regular_topology.
 Variable R : numFieldType.
-  
+HB.instance Definition _ := Num.NormedZmodule.on R^o.
+
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl.
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _).
@@ -6098,4 +6099,3 @@ by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j.
 Qed.
 
 End vitali_lemma_infinite.
-
diff --git a/theories/numfun.v b/theories/numfun.v
index f8db1fae4d..357b9f2abf 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -623,7 +623,7 @@ exists (lim (h_ @ \oo)); split.
     by move=> n; rewrite mulr_ge0.
   rewrite (le_trans (lim_series_norm _))//; apply: le_trans.
     exact/(lim_series_le cvg_gt _ (g_bd ^~ t))/is_cvg_geometric_series.
-  rewrite (cvg_lim _ (cvg_geometric_series _))//.
+  rewrite (cvg_lim _ (cvg_geometric_series _))//; last exact: Rhausdorff.
   by rewrite onem_twothirds mulrAC divrr ?mul1r// unitfE.
 Unshelve. all: by end_near. Qed.
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 1b115f99ea..453f254ede 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -258,8 +258,6 @@ Import numFieldTopology.Exports.
 Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
 Proof. exact: order_hausdorff. Qed.
 
-Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core.
-
 Section separated_topologicalType.
 Variable T : topologicalType.
 Implicit Types x y : T.
diff --git a/theories/tvs.v b/theories/tvs.v
index a16219734c..185e0821d2 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -276,7 +276,6 @@ End Tvs_numField.
 
 Section regular_topology.
 Variable R : numFieldType.
-HB.instance Definition _ := Num.NormedZmodule.on R^o.
 
 Lemma regular_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2).
 Proof.