minor fix

theories/lebesgue_measure.v

@@ -400,6 +400,20 @@ exists (`|floor (x - y)^-1|%N); rewrite -ltr_subr_addl -{2}(invrK (x - y)%R) ltr
 - by rewrite invr_gt0 subr_gt0 yx andbT unitfE invr_eq0 gt_eqF// subr_gt0.
 Qed.
 
+(* NB: PR in progress *)
+Lemma setIM T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) :
+  (X1 `&` Y1) `*` (X2 `&` Y2) = X1 `*` X2 `&` Y1 `*` Y2.
+Proof.
+by rewrite predeqE => -[x y]; split=> [[/= [? ?] [? ?]//]|[] [? ?] [? ?]].
+Qed.
+
+Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A.
+Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed.
+
+Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B.
+Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed.
+(* NB: /PR in progress *)
+
 (******************************************************************************)
 (*                        /lemmas waiting to be PRed                          *)
 (******************************************************************************)
@@ -6172,19 +6186,6 @@ Definition prod_measurableType := [the measurableType of prod_measurable T1 T2].
 
 End product_salgebra_instance.
 
-(* TODO: move *)
-Lemma setIM T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) :
-  (X1 `&` Y1) `*` (X2 `&` Y2) = X1 `*` X2 `&` Y1 `*` Y2.
-Proof.
-by rewrite predeqE => -[x y]; split=> [[/= [? ?] [? ?]//]|[] [? ?] [? ?]].
-Qed.
-
-Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A.
-Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed.
-
-Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B.
-Proof. by rewrite predeqE => -[x y]; split => //= -[]. Qed.
-
 (* TODO: move *)
 Lemma measurableM (T1 T2 : measurableType) (A : set T1) (B : set T2) :
   measurable A -> measurable B -> measurable (A `*` B).
@@ -6256,15 +6257,13 @@ Qed.
 End product_salgebra_g_measurableType.
 
 Section prod_measurable_fun.
-Variables (T T1 T2 : measurableType).
+Variables (T T1 T2 : measurableType) (f : T -> prod_measurableType T1 T2).
 
-Lemma prod_measurable_funP (f : T -> prod_measurableType T1 T2) :
-  measurable_fun setT f <->
+Lemma prod_measurable_funP : measurable_fun setT f <->
   measurable_fun setT (fst \o f) /\ measurable_fun setT (snd \o f).
 Proof.
-apply: (@iff_trans _ (preimage_classes (fst \o f) (snd \o f) `<=` @measurable T)).
-- rewrite preimage_classes_comp.
-  split=> [mf A [C HC <-]|f12]; first exact: mf.
+apply: (@iff_trans _ (preimage_classes (fst \o f) (snd \o f) `<=` measurable)).
+- rewrite preimage_classes_comp; split=> [mf A [C HC <-]|f12]; first exact: mf.
   by move=> A mA; apply: f12; exists A.
 - split => [h|[mf1 mf2]].
     by split => A mA; apply/h/g_salgebra_self; [left; exists A|right; exists A].
@@ -6275,17 +6274,29 @@ Qed.
 End prod_measurable_fun.
 
 Section partial_measurable_fun.
-Variables (T T1 T2 : measurableType).
+Variables (T T1 T2 : measurableType) (f : prod_measurableType T1 T2 -> T).
 
-Lemma partial_measurable_fun (f : prod_measurableType T1 T2 -> T) (x : T1) :
+Lemma measurable_fun_prod1 x :
   measurable_fun setT f -> measurable_fun setT (fun y => f (x, y)).
 Proof.
-move=> mf; pose Ix := fun y : T2 => (x, y).
-have m_fstIx : measurable_fun setT (fst \o Ix).
+move=> mf; pose pairx := fun y : T2 => (x, y).
+have m1pairx : measurable_fun setT (fst \o pairx).
   exact/measurable_fun_cst/measurableT.
-have m_sndIx : measurable_fun setT (snd \o Ix).
+have m2pairx : measurable_fun setT (snd \o pairx).
   exact/measurable_fun_id/measurableT.
-have mIx : measurable_fun setT Ix by exact/(proj2 (prod_measurable_funP Ix)).
+have : measurable_fun setT pairx by exact/(proj2 (prod_measurable_funP _)).
+exact: measurable_fun_comp.
+Qed.
+
+Lemma measurable_fun_prod2 y :
+  measurable_fun setT f -> measurable_fun setT (fun x => f (x, y)).
+Proof.
+move=> mf; pose pairy := fun x : T1 => (x, y).
+have m1pairy : measurable_fun setT (fst \o pairy).
+  exact/measurable_fun_id/measurableT.
+have m2pairy : measurable_fun setT (snd \o pairy).
+  exact/measurable_fun_cst/measurableT.
+have : measurable_fun setT pairy by exact/(proj2 (prod_measurable_funP _)).
 exact: measurable_fun_comp.
 Qed.
 

theories/normedtype.v

@@ -365,7 +365,7 @@ by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e;
 Qed.
 
 Lemma in_segment_addgt0Pl (R : numFieldType) (x y z : R) :
-  reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]%R) (y \in `[x, z]%R).
+  reflect (forall e, e > 0 -> y \in `[(- e + x), (e + z)]) (y \in `[x, z]).
 Proof.
 apply/(equivP (in_segment_addgt0Pr x y z)).
 by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC.
@@ -2759,13 +2759,13 @@ End at_left_right.
 Typeclasses Opaque at_left at_right.
 
 (* TODO: backport to mathcomp in progress *)
-Lemma itvxx d (T : porderType d) (x : T) : `[x, x]%O =i pred1 x.
+Lemma itvxx d (T : porderType d) (x : T) : `[x, x] =i pred1 x.
 Proof. by move=> y; rewrite in_itv/= -eq_le eq_sym. Qed.
 
-Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]%O).
+Lemma itvxxP d (T : porderType d) (x y : T) : reflect (y = x) (y \in `[x, x]).
 Proof. by rewrite itvxx; apply/eqP. Qed.
 
-Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ <= `[a, b]}%O.
+Lemma subset_itv_oo_cc d (T : porderType d) (a b : T) : {subset `]a, b[ <= `[a, b]}.
 Proof. by apply: subitvP; rewrite subitvE !bound_lexx. Qed.
 (* /TODO: backport to mathcomp in progress *)
 
@@ -2988,7 +2988,7 @@ Qed.
 Lemma interval_is_interval (i : interval R) : is_interval [set` i].
 Proof.
 by case: i => -[[]a|[]] [[]b|[]] // x y /=; do ?[by rewrite ?itv_ge//];
-  move=> xi yi z; rewrite -[x <= z <= y]/(z \in `[x, y]%O); apply/subitvP;
+  move=> xi yi z; rewrite -[x <= z <= y]/(z \in `[x, y]); apply/subitvP;
   rewrite subitvE /Order.le/= ?(itvP xi, itvP yi).
 Qed.
 
@@ -3082,7 +3082,7 @@ Definition Rhull (X : set R) : interval R := Interval
   (if `[< has_ubound X >] then BSide (~~ `[< X (sup X) >]) (sup X)
                           else BInfty _ false).
 
-Lemma Rhull0 : Rhull set0 = `]0, 0[%R :> interval R.
+Lemma Rhull0 : Rhull set0 = `]0, 0[ :> interval R.
 Proof.
 rewrite /Rhull  (asboolT (has_lbound0 R)) (asboolT (has_ubound0 R)) asboolF //.
 by rewrite sup0 inf0.
@@ -3242,7 +3242,7 @@ apply: segment_connected.
     by have := xe_y; rewrite /ball_ => /ltr_distlC_subl.
   by rewrite subr_ge0; apply/ltW.
 exists A; last by rewrite predeqE => x; split=> [[] | []].
-move=> x clAx; have abx : x \in `[a, b]%R.
+move=> x clAx; have abx : x \in `[a, b].
   by apply: interval_closed; have /closureI [] := clAx.
 split=> //; have /sabUf [i Di fx] := abx.
 have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi].
@@ -3274,12 +3274,12 @@ rewrite {1}(splitr x) ger_addl pmulr_lle0 // => /(lt_le_trans x0);
 Qed.
 
 Lemma IVT (R : realType) (f : R -> R) (a b v : R) :
-  a <= b -> {in `[a, b]%R, continuous f} ->
+  a <= b -> {in `[a, b], continuous f} ->
   minr (f a) (f b) <= v <= maxr (f a) (f b) ->
-  exists2 c, c \in `[a, b]%R & f c = v.
+  exists2 c, c \in `[a, b] & f c = v.
 Proof.
 move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
-    exists2 c, c \in `[a, b]%R & f c = v; last first.
+    exists2 c, c \in `[a, b] & f c = v; last first.
   case: (leP (f a) (f b)) => [] _ fabv; first exact: ivt.
   have [||c cab /oppr_inj] := ivt (- f) (- v); last by exists c.
     by move=> x /fcont; apply: continuousN.
@@ -3291,7 +3291,7 @@ rewrite le_eqVlt => /orP [/eqP->|ltvfb].
 set A := [set c | (c <= b) && (f c <= v)].
 have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW.
 have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP [].
-have supAab : sup A \in `[a, b]%R.
+have supAab : sup A \in `[a, b].
   rewrite inE; apply/andP; split; last first.
     by apply: sup_le_ub => //; apply/ubP => ? /andP [].
   by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leab andTb ltW.
@@ -3315,7 +3315,7 @@ have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x.
 have /supdfe /= : ball (sup A) d%:num x.
   by near: x; rewrite /= nbhs_simpl; exists d%:num => //.
 rewrite /= => /ltr_distlC_subl; apply: le_lt_trans.
-rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b]%R -> v < f t.
+rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
   apply; rewrite inE; apply/andP; split; first by near: x; exists 1.
   near: x; exists (b - sup A) => /=.
     rewrite subr_gt0 lt_def (itvP supAab) andbT; apply/negP => /eqP besup.
@@ -3954,7 +3954,7 @@ Lemma bound_itvE (R : numDomainType) (a b : R) :
 Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed.
 
 Lemma near_in_itv {R : realFieldType} (a b : R) :
-  {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}%O.
+  {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
 Proof.
 move=> y ayb; rewrite (near_shift 0 y).
 have mingt0 : 0 < Num.min (y - a) (b - y).
@@ -4012,10 +4012,10 @@ move=> leab fmono; apply: surj_image_eq => _ /= [x xab <-];
 exact: mono_mem_image_segment.
 Qed.
 
-Lemma inc_segment_image a b f : f a <= f b -> f @`[a, b] = `[f a, f b]%O.
+Lemma inc_segment_image a b f : f a <= f b -> f @`[a, b] = `[f a, f b].
 Proof. by case: ltrP. Qed.
 
-Lemma dec_segment_image a b f : f b <= f a -> f @`[a, b] = `[f b, f a]%O.
+Lemma dec_segment_image a b f : f b <= f a -> f @`[a, b] = `[f b, f a].
 Proof. by case: ltrP. Qed.
 
 Lemma inc_surj_image_segment a b f : a <= b ->

theories/topology.v

@@ -5227,8 +5227,8 @@ Qed.
 Lemma dense_rat (R : realType) : dense (@ratr R @` setT).
 Proof.
 move=> A [r Ar]; rewrite openE => /(_ _ Ar)/nbhs_ballP[_/posnumP[e] reA].
-have /rat_in_itvoo[q] : r < r + e%:num by rewrite ltr_addl.
-rewrite inE /= => /itvP qre; exists (ratr q) => //; split; last by exists q.
+have /rat_in_itvoo[q /itvP qre] : r < r + e%:num by rewrite ltr_addl.
+exists (ratr q) => //; split; last by exists q.
 apply: reA; rewrite /ball /= distrC ltr_distl qre andbT.
 by rewrite (@le_lt_trans _ _ r)// ?qre// ler_subl_addl ler_addr ltW.
 Qed.