From e1b6f4b0db643f05c5d7970cfdf4eeac2b2ae0cb Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Wed, 4 Dec 2024 01:04:16 +0900
Subject: [PATCH] various fixes (#1409)

* fix technical lemma

* fixes #1417

* fixes #1390

* fixes #1389
---
 CHANGELOG_UNRELEASED.md     |  17 ++++++
 classical/classical_sets.v  |  16 ++++--
 reals/constructive_ereal.v  |  26 +++++----
 theories/ereal.v            | 102 ++++++++++++++++++------------------
 theories/kernel.v           |   2 +-
 theories/lebesgue_measure.v |  48 ++++++++---------
 theories/measure.v          |  12 ++---
 theories/numfun.v           |   4 +-
 theories/realfun.v          |   2 +-
 9 files changed, 126 insertions(+), 103 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d8b7a7db8..9d260b055 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -38,6 +38,18 @@
   + `emeasurable_fun_fsum` -> `emeasurable_fsum`
   + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
 
+- in `classical_sets.v`:
+  + `preimage_itv_o_infty` -> `preimage_itvoy`
+  + `preimage_itv_c_infty` -> `preimage_itvcy`
+  + `preimage_itv_infty_o` -> `preimage_itvNyo`
+  + `preimage_itv_infty_c` -> `preimage_itvNyc`
+
+- in `constructive_ereal.v`:
+  + `maxeMr` -> `maxe_pMr`
+  + `maxeMl` -> `maxe_pMl`
+  + `mineMr` -> `mine_pMr`
+  + `mineMl` -> `mine_pMl`
+
 ### Generalized
 
 ### Deprecated
@@ -50,6 +62,11 @@
 - in `lebesgue_integral.v`:
   + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
   + notation `measurable_fun_indic` (deprecation since 0.6.3)
+- in `constructive_ereal.v`
+  + notation `lee_opp` (deprecated since 0.6.5)
+  + notation `lte_opp` (deprecated since 0.6.5)
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
 
 ### Infrastructure
 
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index b773f279d..e4dc9adeb 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -469,25 +469,33 @@ Lemma preimage_itv T d (rT : porderType d) (f : T -> rT) (i : interval rT) (x :
   ((f @^-1` [set` i]) x) = (f x \in i).
 Proof. by rewrite inE. Qed.
 
-Lemma preimage_itv_o_infty T d (rT : porderType d) (f : T -> rT) y :
+Lemma preimage_itvoy T d (rT : porderType d) (f : T -> rT) y :
   f @^-1` `]y, +oo[%classic = [set x | (y < f x)%O].
 Proof.
 by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvoy")]
+Notation preimage_itv_o_infty := preimage_itvoy (only parsing).
 
-Lemma preimage_itv_c_infty T d (rT : porderType d) (f : T -> rT) y :
+Lemma preimage_itvcy T d (rT : porderType d) (f : T -> rT) y :
   f @^-1` `[y, +oo[%classic = [set x | (y <= f x)%O].
 Proof.
 by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvcy")]
+Notation preimage_itv_c_infty := preimage_itvcy (only parsing).
 
-Lemma preimage_itv_infty_o T d (rT : orderType d) (f : T -> rT) y :
+Lemma preimage_itvNyo T d (rT : orderType d) (f : T -> rT) y :
   f @^-1` `]-oo, y[%classic = [set x | (f x < y)%O].
 Proof. by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvNyo")]
+Notation preimage_itv_infty_o := preimage_itvNyo (only parsing).
 
-Lemma preimage_itv_infty_c T d (rT : orderType d) (f : T -> rT) y :
+Lemma preimage_itvNyc T d (rT : orderType d) (f : T -> rT) y :
   f @^-1` `]-oo, y]%classic = [set x | (f x <= y)%O].
 Proof. by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvNyc")]
+Notation preimage_itv_infty_c := preimage_itvNyc (only parsing).
 
 Lemma eq_set T (P Q : T -> Prop) : (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 3c9cc0940..a119e963f 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -2468,7 +2468,7 @@ Qed.
 Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
 Proof. by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed.
 
-Lemma maxeMr z x y : z \is a fin_num -> 0 <= z ->
+Lemma maxe_pMr z x y : z \is a fin_num -> 0 <= z ->
   z * maxe x y = maxe (z * x) (z * y).
 Proof.
 move=> /[swap]; rewrite le_eqVlt => /predU1P[<- _|z0].
@@ -2478,20 +2478,20 @@ have [xy|yx|->] := ltgtP x y; last by rewrite maxxx.
 - by move=> zfin; rewrite maxC /maxe lte_pmul2l// yx.
 Qed.
 
-Lemma maxeMl z x y : z \is a fin_num -> 0 <= z ->
+Lemma maxe_pMl z x y : z \is a fin_num -> 0 <= z ->
   maxe x y * z = maxe (x * z) (y * z).
-Proof. by move=> zfin z0; rewrite muleC maxeMr// !(muleC z). Qed.
+Proof. by move=> zfin z0; rewrite muleC maxe_pMr// !(muleC z). Qed.
 
-Lemma mineMr z x y : z \is a fin_num -> 0 <= z ->
+Lemma mine_pMr z x y : z \is a fin_num -> 0 <= z ->
   z * mine x y = mine (z * x) (z * y).
 Proof.
 move=> fz zge0.
-by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxeMr// !muleN -oppe_min.
+by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxe_pMr// !muleN -oppe_min.
 Qed.
 
-Lemma mineMl z x y : z \is a fin_num -> 0 <= z ->
+Lemma mine_pMl z x y : z \is a fin_num -> 0 <= z ->
   mine x y * z = mine (x * z) (y * z).
-Proof. by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed.
+Proof. by move=> zfin z0; rewrite muleC mine_pMr// !(muleC z). Qed.
 
 Lemma bigmaxe_fin_num (s : seq R) r : r \in s ->
   \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.
@@ -2660,10 +2660,6 @@ Arguments lee_sum_nneg_natl {R}.
 Arguments lee_sum_npos_natl {R}.
 #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core.
 
-#[deprecated(since="mathcomp-analysis 0.6.5", note="Use leeN2 instead.")]
-Notation lee_opp := leeN2 (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")]
-Notation lte_opp := lteN2 (only parsing).
 #[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDl instead.")]
 Notation lee_addl := leeDl (only parsing).
 #[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDr instead.")]
@@ -2730,6 +2726,14 @@ Notation lte_le_sub := lte_leB (only parsing).
 Notation lee_opp2 := leeN2 (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")]
 Notation lte_opp2 := lteN2 (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMr")]
+Notation maxeMr := maxe_pMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMl")]
+Notation maxeMl := maxe_pMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMr")]
+Notation mineMr := mine_pMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMl")]
+Notation mineMl := mine_pMl (only parsing).
 
 Module DualAddTheoryRealDomain.
 
diff --git a/theories/ereal.v b/theories/ereal.v
index 015c0e020..d8125916c 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -399,7 +399,7 @@ have sSoo : supremums S +oo.
   by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->.
 case: xgetP.
   by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget).
-by move/(_ +oo) => gSoo; exfalso; apply gSoo => {gSoo}.
+by move/(_ +oo) => gSoo; exfalso; exact: gSoo.
 Qed.
 
 Definition ereal_sup S := supremum -oo S.
@@ -430,8 +430,8 @@ Qed.
 
 Lemma lb_ereal_inf S M : lbound S M -> M <= ereal_inf S.
 Proof.
-move=> SM; rewrite /ereal_inf leeNr; apply ub_ereal_sup => x [y Sy <-{x}].
-by rewrite leeNl oppeK; apply SM.
+move=> SM; rewrite /ereal_inf leeNr; apply: ub_ereal_sup => x [y Sy <-{x}].
+by rewrite leeNl oppeK; exact: SM.
 Qed.
 
 Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R ->
@@ -491,7 +491,7 @@ have [|] := eqVneq (ubound U) set0.
   rewrite -subset0 => U0; exists +oo.
   split; [exact/ereal_ub_pinfty | apply/lbP => /= -[r0 /ubP Sr0|//|]].
   - suff : ubound U r0 by move/U0.
-    by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; apply Sr0.
+    by apply/ubP=> _ -[] [r1 Sr1 <-|//| /= _ <-]; rewrite -lee_fin; exact: Sr0.
   - by move/ereal_ub_ninfty => [|]; by [move/eqP : S0|move/eqP : Snoo].
 set u : R := sup U.
 exists u%:E; split; last first.
@@ -514,8 +514,8 @@ Lemma ereal_sup_ubound S : ubound S (ereal_sup S).
 Proof.
 move=> y Sy; rewrite /ereal_sup /supremum ifF; last first.
   by apply/eqP; rewrite predeqE => /(_ y)[+ _]; exact.
-case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS.
-by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0).
+case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply: geS.
+by case: (ereal_supremums_neq0 S) => /= x0 Sx0 /(_ x0).
 Qed.
 
 Lemma ereal_supy S : S +oo -> ereal_sup S = +oo.
@@ -680,13 +680,11 @@ Context {R : numFieldType}.
 Global Instance ereal_dnbhs_filter :
   forall x : \bar R, ProperFilter (ereal_dnbhs x).
 Proof.
-case=> [x||].
+case=> [x| |].
 - case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS].
-  apply Build_ProperFilter => //=; apply Build_Filter => //=.
-  move=> P Q lP lQ; exact: xI.
-  by move=> P Q PQ /xS; apply => y /PQ.
-- apply Build_ProperFilter_ex.
-    move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=.
+    by apply: Build_ProperFilter => //=; exact: Build_Filter.
+- apply: Build_ProperFilter_ex.
+    move=> P [x [xr xP]] //; exists (x + 1)%:E; apply: xP => /=.
     by rewrite lte_fin ltrDl.
   split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
   + by exists 0%R.
@@ -696,11 +694,13 @@ case=> [x||].
           [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
       exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split.
         by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin.
-      by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
+      apply: gtMQ.
+      by rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
     have [MQ0|MQ0] := eqVneq MQ 0%R.
       exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split.
-      by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
-      by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
+        apply: gtMP.
+        by rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
+      by apply: gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
     have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
     have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
     exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
@@ -711,7 +711,7 @@ case=> [x||].
       by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx.
     * by move=> _; split; [apply/gtMP | apply/gtMQ].
   + by exists M; split => // ? /gtM /sPQ.
-- apply Build_ProperFilter_ex.
+- apply: Build_ProperFilter_ex.
   + move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
     by apply: ltMP; rewrite lte_fin gtrDl oppr_lt0.
   + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
@@ -722,15 +722,15 @@ case=> [x||].
           [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
         exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ.
         split.
-          by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 lerNl oppr0.
-       apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin lerNl -normrN.
+          by apply: ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 lerNl oppr0.
+       apply: ltMQ; rewrite (lt_le_trans xMQ) // lee_fin lerNl -normrN.
        by rewrite real_ler_normr ?realN // lexx.
     * have [MQ0|MQ0] := eqVneq MQ 0%R.
         exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx.
         split.
-          apply ltMP; rewrite (lt_le_trans MPx) // lee_fin lerNl -normrN.
+          apply: ltMP; rewrite (lt_le_trans MPx) // lee_fin lerNl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
-        by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 lerNl oppr0.
+        by apply: ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 lerNl oppr0.
       have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
       have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
       exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
@@ -812,7 +812,7 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
   move=> -[x| _ |_] //=; last by exists M.
   rewrite lte_fin => M'x /=.
   apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
+  apply: MA; rewrite lte_fin.
   rewrite addrC -ltrBrDl in M'x.
   rewrite (lt_le_trans M'x) // lerBlDl addrC -lerBlDl.
   rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
@@ -825,7 +825,7 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
   move=> -[x| _ |_] //=; last by exists M.
   rewrite lte_fin => M'x /=.
   apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
+  apply: MA; rewrite lte_fin.
   rewrite ltrBrDl in M'x.
   rewrite (le_lt_trans _ M'x) // addrC -lerBlDl.
   rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
@@ -848,28 +848,28 @@ case: x => [r /=| |].
   rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]].
     exists (-%E @` S).
       exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK.
-      by apply reS; rewrite /ball /= opprK -normrN opprD opprK.
+      by apply: reS; rewrite /ball /= opprK -normrN opprD opprK.
     rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss].
       by rewrite oppeK.
     by exists (- s); [exists s | rewrite oppeK].
   exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK.
-  by apply reS'; rewrite /ball /= opprK -normrN opprD.
+  by apply: reS'; rewrite /ball /= opprK -normrN opprD.
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lteNl | rewrite oppeK].
+      by exists (- x); [apply: MS; rewrite lteNl | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lteNr|rewrite oppeK].
+  exists (- y); by [apply: Mx; rewrite lteNr|rewrite oppeK].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lteNr | rewrite oppeK].
+      by exists (- x); [apply: MS; rewrite lteNr | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lteNl|rewrite oppeK].
+  exists (- y); by [apply: Mx; rewrite lteNl|rewrite oppeK].
 Qed.
 
 Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
@@ -892,7 +892,7 @@ Qed.
 Lemma oppe_continuous (R : realFieldType) :
   continuous (-%E : \bar R -> \bar R).
 Proof.
-move=> x S /= xS; apply nbhsNKe; rewrite image_preimage //.
+move=> x S /= xS; apply: nbhsNKe; rewrite image_preimage //.
 by rewrite predeqE => y; split => // _; exists (- y) => //; rewrite oppeK.
 Qed.
 
@@ -946,7 +946,7 @@ Let contract := @contract R.
 Lemma sup_contract_le1 S : S !=set0 -> (`|sup (contract @` S)| <= 1)%R.
 Proof.
 case=> x Sx; rewrite ler_norml; apply/andP; split; last first.
-  apply sup_le_ub; first by exists (contract x), x.
+  apply: sup_le_ub; first by exists (contract x), x.
   by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y).
 rewrite (@le_trans _ _ (contract x)) //.
   by case/ler_normlP : (contract_le1 x); rewrite lerNl.
@@ -963,13 +963,13 @@ move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
 rewrite leNgt; apply/negP.
 set supc := sup _; set csup := contract _; move=> ltsup.
 suff [y [ysupS ?]] : exists y, y < ereal_sup S /\ ubound S y.
-  have : ereal_sup S <= y by apply ub_ereal_sup.
+  have : ereal_sup S <= y by exact: ub_ereal_sup.
   by move/(lt_le_trans ysupS); rewrite ltxx.
 suff [x [? [ubSx x1]]] : exists x, (x < csup)%R /\ ubound (contract @` S) x /\
     (`|x| <= 1)%R.
   exists (expand x); split => [|y Sy].
     by rewrite -(contractK (ereal_sup S)) lt_expand // inE // contract_le1.
-  by rewrite -(contractK y) le_expand //; apply ubSx; exists y.
+  by rewrite -(contractK y) le_expand //; apply: ubSx; exists y.
 exists ((supc + csup) / 2); split; first by rewrite midf_lt.
 split => [r [y Sy <-{r}]|].
   rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW.
@@ -1085,7 +1085,7 @@ move=> e1 reA; suff h : nbhs +oo (-%E @` A).
   rewrite (_ : -oo = - +oo) // nbhsNe; exists (-%E @` A) => //.
   rewrite predeqE => x; split=> [[y [z Az <- <-]]|Ax]; rewrite ?oppeK //.
   by exists (- x); [exists x | rewrite oppeK].
-apply (@nbhs_oo_up_e1 _ e) => // x x1e; exists (- x); last by rewrite oppeK.
+apply/ (@nbhs_oo_up_e1 _ e) => // x x1e; exists (- x); last by rewrite oppeK.
 by apply/reA/ereal_ballN; rewrite oppeK.
 Qed.
 
@@ -1094,14 +1094,14 @@ Lemma nbhs_oo_up_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R ->
 Proof.
 move=> e1 reA; have [e2{e1}|e2] := ltrP 2 e%:num.
   suff -> : A = setT by exists 0%R.
-  rewrite predeqE => x; split => // _; apply reA.
+  rewrite predeqE => x; split => // _; apply: reA.
   exact/ereal_ballN/ereal_ball_ninfty_oversize.
 have /andP[e10 e11] : (0 < e%:num - 1 <= 1)%R.
   by rewrite subr_gt0 e1 /= lerBlDl.
-apply nbhsNKe.
+apply: nbhsNKe.
 have : ((PosNum e10)%:num <= 1)%R by [].
-move/(@nbhs_oo_down_e1 (-%E @` A) (PosNum e10)); apply.
-move=> y ye; exists (- y); last by rewrite oppeK.
+move/(@nbhs_oo_down_e1 (-%E @` A) (PosNum e10)); apply=> y ye.
+exists (- y); last by rewrite oppeK.
 apply/reA/ereal_ballN; rewrite oppeK /=.
 by apply: le_ereal_ball ye => /=; rewrite lerBlDl lerDr.
 Qed.
@@ -1114,7 +1114,7 @@ move=> e1 reA; have [e2{e1}|e2] := ltrP 2 e%:num.
   by rewrite predeqE => x; split => // _; exact/reA/ereal_ball_ninfty_oversize.
 have /andP[e10 e11] : (0 < e%:num - 1 <= 1)%R.
   by rewrite subr_gt0 e1 /= lerBlDl.
-apply nbhsNKe.
+apply: nbhsNKe.
 have : ((PosNum e10)%:num <= 1)%R by [].
 move/(@nbhs_oo_up_e1 (-%E @` A) (PosNum e10)); apply.
 move=> y ye; exists (- y); last by rewrite oppeK.
@@ -1137,7 +1137,7 @@ have e'0 : (0 < e')%R.
   rewrite subr_gt0 -lte_fin -[ltRHS](contractK r%:E).
   rewrite fine_expand // lt_expand ?inE ?contract_le1// ?ltW//.
   by rewrite ltrBlDl ltrDr.
-apply/nbhs_ballP; exists e' => // r' re'r'; apply reA.
+apply/nbhs_ballP; exists e' => // r' re'r'; apply: reA.
 by have [?|?] := lerP r r';
   [exact: contract_ereal_ball_fin_le | exact: ball_ereal_ball_fin_lt].
 Qed.
@@ -1156,7 +1156,7 @@ pose e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R.
 have e'0 : (0 < e')%R.
   rewrite /e' subr_gt0 -lte_fin -[in ltLHS](contractK r%:E).
   by rewrite fine_expand // lt_expand ?inE ?contract_le1 ?ltrDl ?ltW.
-apply/nbhs_ballP; exists e' => // r' r'e'r; apply reA.
+apply/nbhs_ballP; exists e' => // r' r'e'r; apply: reA.
 by have [?|?] := lerP r r';
   [exact: ball_ereal_ball_fin_le | exact: contract_ereal_ball_fin_lt].
 Qed.
@@ -1168,11 +1168,11 @@ Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) :
   nbhs r%:E A.
 Proof.
 move=> reA reN1 re1; suff : A = setT by move->; apply: filterT.
-rewrite predeqE => x; split => // _; apply reA.
+rewrite predeqE => x; split => // _; apply: reA.
 case: x => [r'| |] //.
 - have [?|?] := lerP r r'.
   + by apply: contract_ereal_ball_fin_le => //; exact/ltW.
-  + by apply contract_ereal_ball_fin_lt => //; exact/ltW.
+  + by apply: contract_ereal_ball_fin_lt => //; exact/ltW.
 - exact/contract_ereal_ball_pinfty.
 - apply/ereal_ballN/contract_ereal_ball_pinfty.
   by rewrite EFinN contractN -(opprK 1%R) ltrNl opprD opprK.
@@ -1189,15 +1189,15 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
     rewrite opprK -mulr2n mulrn_eq0 orFb contract_eq0 => /eqP[r0].
     move: re1; rewrite r0 contract0 add0r => /eqP e1.
     apply/nbhs_ballP; exists 1%R => //= r'; rewrite /ball /= sub0r normrN => r'1.
-    apply reA.
+    apply: reA.
     by rewrite /ereal_ball r0 contract0 sub0r normrN e1 contract_lt1.
   rewrite neq_lt => /orP[re1|re1].
-    by apply (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r.
+    by apply: (@nbhs_fin_out_below _ e) => //; rewrite reN1 addrAC subrr sub0r.
   have e1 : (1 < e%:num)%R.
     move: re1; rewrite reN1 addrAC ltrBrDl -!mulr2n -(mulr_natl e%:num).
     by rewrite -{1}(mulr1 2%:R) => ?; rewrite -(@ltr_pM2l _ 2).
   have Aoo : setT `\ -oo `<=` A.
-    move=> x [_]; rewrite /set1 /= => xnoo; apply reA.
+    move=> x [_]; rewrite /set1 /= => xnoo; apply: reA.
     case: x xnoo => [r' _ | _ |//].
       have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
         apply: contract_ereal_ball_fin_le; last exact/ltW.
@@ -1212,7 +1212,7 @@ have [|reN1] := boolP (contract r%:E - e%:num == -1)%R.
   by apply/nbhs_ballP; exists e'%:num => //= y /h; apply: Aoo.
 move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
   have [re1|re1] := eqVneq (contract r%:E + e%:num)%R 1%R.
-    by apply (@nbhs_fin_out_above _ e) => //; rewrite re1.
+    by apply: (@nbhs_fin_out_above _ e) => //; rewrite re1.
   move: re1; rewrite neq_lt => /orP[re1|re1].
     have ? : (`|contract r%:E - e%:num| < 1)%R.
       rewrite ltr_norml reN1 andTb ltrBlDl.
@@ -1231,7 +1231,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
         by rewrite ltrBlDl ltrDr.
       rewrite subr_gt0 -lte_fin -[in ltLHS](contractK r%:E).
       by rewrite fine_expand// lt_expand ?inE ?contract_le1 ?ltrDl ?ltW.
-    apply/nbhs_ballP; exists e' => // r' re'r'; apply reA.
+    apply/nbhs_ballP; exists e' => // r' re'r'; apply: reA.
     have [|r'r] := lerP r r'.
       move=> rr'; apply: ball_ereal_ball_fin_le => //.
       by apply: le_ball re'r'; rewrite ge_min lexx orbT.
@@ -1239,7 +1239,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
     rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl.
     rewrite opprK -lte_fin fine_expand // => r'e'r _.
     exact: expand_ereal_ball_fin_lt.
-  by apply (@nbhs_fin_out_above _ e) => //; rewrite ltW.
+  by apply :(@nbhs_fin_out_above _ e) => //; rewrite ltW.
 have [re1|re1] := ltrP 1 (contract r%:E + e%:num).
   exact: (@nbhs_fin_out_above_below _ e).
 move: re1; rewrite le_eqVlt => /orP[re1|re1].
@@ -1251,7 +1251,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
     rewrite -(mulr_natl e%:num) -{1}(mulr1 2%:R) => ?.
     by rewrite -(@ltr_pM2l _ 2).
   have Aoo : (setT `\ +oo `<=` A).
-    move=> x [_]; rewrite /set1 /= => xpoo; apply reA.
+    move=> x [_]; rewrite /set1 /= => xpoo; apply: reA.
     case: x xpoo => [r' _ | // |_].
       rewrite /ereal_ball.
       have [rr'|r'r] := lerP (contract r%:E) (contract r'%:E).
@@ -1268,7 +1268,7 @@ move: re1; rewrite le_eqVlt => /orP[re1|re1].
    have : nbhs r%:E (setT `\ +oo) by exists 1%R => /=.
    case => _/posnumP[x] /=; rewrite /ball_ => h.
    by exists x%:num => //= y /h; exact: Aoo.
-by apply (@nbhs_fin_out_below _ e) => //; rewrite ltW.
+by apply: (@nbhs_fin_out_below _ e) => //; rewrite ltW.
 Qed.
 
 Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ (@ereal_ball R)).
@@ -1371,7 +1371,7 @@ rewrite predeq2E => x A; split.
     * rewrite /ereal_ball /= => _; exact: MA.
 - case: x => [r [E [_/posnumP[e] reA] sEA] | [E [_/posnumP[e] reA] sEA] |
                [E [_/posnumP[e] reA] sEA]] //=.
-  + by apply nbhs_fin_inbound with e => ? ?; exact/sEA/xsectionP/reA.
+  + by apply: (@nbhs_fin_inbound _ e) => ? ?; exact/sEA/xsectionP/reA.
   + have [|] := boolP (e%:num <= 1)%R.
       by move/nbhs_oo_up_e1; apply => ? ?; exact/sEA/xsectionP/reA.
     by rewrite -ltNge => /nbhs_oo_up_1e; apply => ? ?; exact/sEA/xsectionP/reA.
diff --git a/theories/kernel.v b/theories/kernel.v
index 18926aedb..71c065e5a 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -644,7 +644,7 @@ Let measurable_fun_kprobability U : measurable U ->
 Proof.
 move=> mU.
 apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
-rewrite setTI preimage_itv_infty_o -/(P @^-1` mset U r).
+rewrite setTI preimage_itvNyo -/(P @^-1` mset U r).
 have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0.
 have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT.
 move: mP => /(_ measurableT (mset U r)); rewrite setTI; apply.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 48afe4f58..c0abfbdd3 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -434,16 +434,16 @@ Hypotheses (mD : measurable D) (mf : measurable_fun D f).
 Implicit Types y : \bar R.
 
 Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]).
-Proof. by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvcy; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_o_infty y :  measurable (D `&` [set x | y < f x]).
-Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvoy; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]).
-Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvNyo; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]).
-Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvNyc; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).
 Proof.
@@ -908,7 +908,7 @@ Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) :
 Proof.
 move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)).
 move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable.
-by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact.
+by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact.
 Qed.
 
 Section standard_measurable_fun.
@@ -986,12 +986,12 @@ Lemma measurable_funD D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
 Proof.
 move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy.
 rewrite [X in measurable X](_ : _ = \bigcup_(q : rat)
   ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))).
   apply: bigcupT_measurable_rat => q; apply: measurableI.
-  - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv.
-  - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv.
+  - by rewrite -preimage_itvoy; apply: mf => //; exact: measurable_itv.
+  - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv.
 rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]].
   rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
   exists r => //; rewrite setIACA setIid; split => //; split => /=.
@@ -1026,7 +1026,7 @@ Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
 Proof.
 move=> mf mg mD; apply: (measurable_fun_bool true) => //.
 under eq_fun do rewrite -subr_gt0.
-by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB.
+by rewrite preimage_true -preimage_itvoy; exact: measurable_funB.
 Qed.
 
 Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
@@ -1034,7 +1034,7 @@ Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
 Proof.
 move=> mf mg mD; apply: (measurable_fun_bool true) => //.
 under eq_fun do rewrite -subr_ge0.
-by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
+by rewrite preimage_true -preimage_itvcy; exact: measurable_funB.
 Qed.
 
 Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g ->
@@ -1257,12 +1257,12 @@ Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x + g x)%N.
 Proof.
 move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))).
   apply: bigcupT_measurable => q; apply: measurableI.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_c_infty; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvcy; exact: mg.
 rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]].
 - move=> afxgx; exists (a - g x)%N => //=; split; split => //.
     by rewrite leEnat leq_subLR// addnC -leEnat.
@@ -1279,8 +1279,8 @@ move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
 move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ =
   ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))).
   apply: measurableU.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_c_infty; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvcy; exact: mg.
 rewrite predeqE => x; split => [[Dx /=]|].
 - by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto.
 - move=> [[Dx /= afx]|[Dx /= agx]].
@@ -1295,13 +1295,13 @@ Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N ->
   measurable_fun D (fun x => f x - g x)%N.
 Proof.
 move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | maxn a q <= f x]%O) `&`
    (D `&` [set x | g x <= (q - a)%N]%O))).
   apply: bigcupT_measurable => q; apply: measurableI.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_infty_c; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvNyc; exact: mg.
 rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]].
 - move=> afxgx; exists (g x + a)%N => //; split; split => //=.
     rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a.
@@ -1335,15 +1335,15 @@ move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
     apply/funext => n; apply/idP/idP.
       by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0.
     by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0.
-  by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_fun_subn.
+  by rewrite preimage_true -preimage_itvoy; exact: measurable_fun_subn.
 - under eq_fun do rewrite ltnNge.
   rewrite preimage_false set_predC setCK.
   rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f)
       ([set y | g y <= i]%O `&` [set t | i <= f t]%O)).
     rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
     rewrite setIIr; apply: measurableI => //.
-    + by rewrite -preimage_itv_infty_c; exact: mg.
-    + by rewrite -preimage_itv_c_infty; exact: mf.
+    + by rewrite -preimage_itvNyc; exact: mg.
+    + by rewrite -preimage_itvcy; exact: mf.
   apply/funext => n/=.
   suff : (g n <= f n)%N <->
       (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n.
@@ -1363,8 +1363,8 @@ move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
       \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)).
     rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
     rewrite setIIr; apply: measurableI => //.
-    + by rewrite -preimage_itv_infty_c; exact: mf.
-    + by rewrite -preimage_itv_c_infty; exact: mg.
+    + by rewrite -preimage_itvNyc; exact: mf.
+    + by rewrite -preimage_itvcy; exact: mg.
   apply/funext => n/=.
   suff : (f n <= g n)%N <->
     (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n.
@@ -1396,7 +1396,7 @@ Lemma EFin_measurable (D : set R) : measurable_fun D EFin.
 Proof.
 move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [x ->]] <-; apply: measurableI => //.
-by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv.
+by rewrite preimage_itvoy EFin_itv; exact: measurable_itv.
 Qed.
 
 Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse.
diff --git a/theories/measure.v b/theories/measure.v
index ef3c416c8..b26b412db 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -866,13 +866,6 @@ case=> ? DC DU; split => [| |? ? ?]; last exact: DU.
 - by move=> A GA; rewrite -setTD; apply: DC.
 Qed.
 
-Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G -> setI_closed G ->
-  (forall n, G (F n)) -> forall n, G (\big[setI/setT]_(i < n) F i).
-Proof.
-move=> dG GI GF; elim => [|n ih]; last by rewrite big_ord_recr /=; apply: GI.
-by rewrite big_ord0; exact: (dynkinT dG).
-Qed.
-
 Lemma dynkin_setI_sigma_algebra G : dynkin G -> setI_closed G ->
   sigma_algebra setT G.
 Proof.
@@ -882,7 +875,8 @@ move=> dG GI; split => [|//|F DF].
 - rewrite seqDU_bigcup_eq; apply/(dynkinU dG) => //.
   move=> n; rewrite /seqDU setDE; apply GI => //.
   rewrite -bigcup_mkord setC_bigcup bigcap_mkord.
-  by apply: (@dynkin_setI_bigsetI _ (fun x => ~` F x)) => // ?; exact/(dynkinC dG).
+  apply: big_ind => //; first by case: dG.
+  by move=> i _; exact/(dynkinC dG).
 Qed.
 
 Lemma setI_closed_g_dynkin_g_sigma_algebra G :
@@ -1070,7 +1064,7 @@ HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
 HB.structure Definition SemiRingOfSets d :=
   {T of Pointed T & isSemiRingOfSets d T}.
 
-Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.
+Arguments measurable {d}%_measure_display_scope {s} _%_classical_set_scope.
 
 Lemma measurable_curry (T1 T2 : Type) d (T : semiRingOfSetsType d)
     (G : T1 * T2 -> set T) (x : T1 * T2) :
diff --git a/theories/numfun.v b/theories/numfun.v
index f3361cce0..3a892df55 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -184,12 +184,12 @@ Qed.
 
 Lemma ge0_funeposM r f : (0 <= r)%R ->
   (fun x => r%:E * f x)^\+ = (fun x => r%:E * (f^\+ x)).
-Proof. by move=> ?; rewrite funeqE => x; rewrite /funepos maxeMr// mule0. Qed.
+Proof. by move=> ?; rewrite funeqE => x; rewrite /funepos maxe_pMr// mule0. Qed.
 
 Lemma ge0_funenegM r f : (0 <= r)%R ->
   (fun x => r%:E * f x)^\- = (fun x => r%:E * (f^\- x)).
 Proof.
-by move=> r0; rewrite funeqE => x; rewrite /funeneg -muleN maxeMr// mule0.
+by move=> r0; rewrite funeqE => x; rewrite /funeneg -muleN maxe_pMr// mule0.
 Qed.
 
 Lemma le0_funeposM r f : (r <= 0)%R ->
diff --git a/theories/realfun.v b/theories/realfun.v
index b11415d1c..5028c4d1b 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1516,7 +1516,7 @@ have fwcte : {within `[x - e, x + e], continuous f}.
 have fKe : {in `[x - e, x + e], cancel f g}
   by near: e; apply/at_right_in_segment.
 have nearfx : \forall y \near f x, y \in f @`](x - e), (x + e)[.
-  apply: near_in_itv; apply: mono_mem_image_itvoo; last first.
+  apply: near_in_itvoo; apply: mono_mem_image_itvoo; last first.
     by rewrite in_itv/= -ltr_distlC subrr normr0.
   apply: itv_continuous_inj_mono => //.
   by apply: (@can_in_inj _ _ _ _ g); near: e; apply/at_right_in_segment.