adapt to rocq-prover/rocq#20707

analysis_stdlib/showcase/uniform_bigO.v

@@ -53,7 +53,7 @@ wlog lex12 : x / (`|x.1| <= `|x.2|).
   by rewrite addrC [`|_|]maxC (ler_norm (x.2, x.1)).
 rewrite [`|_|]max_r // -[X in X * _]ger0_norm // -normrM.
 rewrite -sqrtr_sqr ler_wsqrtr // exprMn sqr_sqrtr // mulr_natl mulr2n lerD2r.
-rewrite -[_ ^+ 2]ger0_norm ?sqr_ge0 // -[X in _ <=X]ger0_norm ?sqr_ge0 //.
+rewrite -[leLHS]ger0_norm ?sqr_ge0 // -[leRHS]ger0_norm ?sqr_ge0 //.
 by rewrite !normrX lerXn2r // nnegrE normr_ge0.
 Qed.
 

classical/classical_sets.v

@@ -2808,7 +2808,7 @@ apply/trivIsetP => i j Di Dj ij.
 rewrite {}s12 {s2}; have [si|si] := ltnP i (size s); last first.
   by rewrite (nth_default set0) ?size_map// set0I.
 rewrite (nth_map O) //; have [sj|sj] := ltnP j (size s); last first.
-  by rewrite (nth_default set0) ?size_map// setI0.
+  by rewrite setIC (nth_default set0) ?size_map// set0I.
 have nth_mem k : k < size s -> nth O s k \in iota 0 (size s1).
   by move=> ?; rewrite -(perm_mem ss1) mem_nth.
 rewrite (nth_map O)// ts1 ?(nth_uniq,(perm_uniq ss1),iota_uniq)//; apply/s1D.

classical/contra.v

@@ -510,7 +510,7 @@ Proof. by move: b => [] [] /= <-; exact/propext. Qed.
 Canonical false_neq P b := BoolNeqRHS (@false_neqP P b).
 
 Local Fact eqType_neqP (T : eqType) (x y : T) : (x <> y) = (x != y).
-Proof. by rewrite (reflect_eq eqP) (reflect_eq negP). Qed.
+Proof. by rewrite [in LHS](reflect_eq eqP) (reflect_eq negP). Qed.
 Canonical eqType_neq (T : eqType) x y :=
   @NeqRHS (x != y) T x (Wrap y) (eqType_neqP x y).
 Local Fact eq_op_posP (T : eqType) x y : (x == y :> T : Prop) = (x = y).

classical/functions.v

@@ -2455,7 +2455,7 @@ End set_bij_lemmas.
 Lemma bij_II_D1 T n (A : set T) (f : nat -> T) :
   set_bij `I_n.+1 A f -> set_bij `I_n (A `\ f n) f.
 Proof.
-rewrite IIS -image_set1; apply: bij_sub_setUll.
+rewrite IIS -[[set f n]]image_set1; apply: bij_sub_setUll.
 by apply/disj_setPS => i [/= /[swap]->]; rewrite ltnn.
 Qed.
 

reals/constructive_ereal.v

@@ -820,7 +820,7 @@ Proof. exact: raddfMn. Qed.
 
 Lemma prodEFin T s (P : pred T) (f : T -> R) :
   \prod_(i <- s | P i) (f i)%:E = (\prod_(i <- s | P i) f i)%:E.
-Proof. by elim/big_ind2 : _ => // _ x _ y -> ->; rewrite EFinM. Qed.
+Proof. by elim/big_ind2 : _ => // ? x ? y -> ->; rewrite EFinM. Qed.
 
 Lemma sumEFin I s P (F : I -> R) :
   \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
@@ -916,7 +916,7 @@ Lemma adde_defNN x y : - x +? - y = x +? y.
 Proof. by rewrite adde_defN oppeK. Qed.
 
 Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.
-Proof. by rewrite -(can_eq oppeK) oppe0. Qed.
+Proof. by rewrite -[RHS](can_eq oppeK) oppe0. Qed.
 
 Lemma oppeD x y : x +? y -> - (x + y) = - x - y.
 Proof. by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.
@@ -2483,7 +2483,7 @@ move: x => [x|_|//].
   move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r.
   - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey.
   - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye.
-  - by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e.
+  - by move=> _; rewrite mulNyr mulyr gtr0_sg// 2!mul1e.
 move=> [y| |] [z| |]//.
 - rewrite lee_fin => yz.
   have [z0|z0|] := ltgtP 0%R z.

theories/convex.v

@@ -336,9 +336,9 @@ have LfE : L x - f x =
 have {Hc1 Hc2} -> : L x - f x = (b - x) * (x - a) * (c2 - c1) / (b - a) *
                                 (('D_1 f c2 - 'D_1 f c1) / (c2 - c1)).
   rewrite LfE Hc2 Hc1.
-  rewrite -(mulrC (b - x)) mulrA -mulrBr.
+  rewrite -(mulrC (b - x)) [in LHS]mulrA -mulrBr.
   rewrite (mulrC ('D_1 f c2 - _)) ![in RHS]mulrA; congr *%R.
-  rewrite -2!mulrA; congr *%R.
+rewrite -2![RHS]mulrA; congr *%R.
   by rewrite mulrCA divff ?mulr1// subr_eq0 gt_eqF.
 rewrite {}h mulr_ge0//; last first.
   rewrite DDf_ge0//; apply/andP; split.

theories/derive.v

@@ -542,7 +542,8 @@ exists df; split=> //; apply: eqaddoEx => z.
 rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK.
 rewrite -addrA -[LHS]addr0; congr (_ + _).
 apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
-by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
+rewrite [in LHS]littleo_center0 (comp_centerK x id).
+by rewrite -[- _ in RHS](comp_centerK x).
 Qed.
 
 Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0.
@@ -1910,7 +1911,7 @@ have Dhx : D° (h + x).
       by near: h; apply: dnbhs0_lt; exact: mulr_gt0.
     by rewrite normrM ger0_norm// mulr_gt0// normr_gt0.
   apply: ball_sym; rewrite /ball/= addrK.
-  by rewrite normrM ger0_norm// ltr_pMl ?normr_gt0// ltr1n.
+  by rewrite normrM (@ger0_norm _ 2)// ltr_pMl ?normr_gt0// ltr1n.
 move: h0; rewrite neq_lt => /orP[h0|h0].
 - rewrite nmulr_rle0 ?invr_lt0// subr_ge0 ltW//.
   by apply: decrf; rewrite ?in_itv ?andbT ?gtrDr// inE; exact: interior_subset.

theories/ftc.v

@@ -1031,7 +1031,7 @@ Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
 Proof.
 have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN.
+by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN.
 Qed.
 
 (* PR in progress *)
@@ -1040,7 +1040,7 @@ Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
   f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l.
 Proof.
 have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty.
+by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty.
 Qed.
 
 Section integration_by_substitution.
@@ -1606,7 +1606,7 @@ rewrite (@increasing_ge0_integration_by_substitutiony (\- (F \o -%R))%R); last 8
     apply: dFcompN.
     rewrite ltrNl.
     by near: z; exact: nbhs_right_gt.
-  rewrite fctE derive1_comp; last 2 first.
+  rewrite fctE [LHS]derive1_comp; last 2 first.
     exact: derivable_id.
     apply: dFN; rewrite ltrNl.
     by near: z; exact: nbhs_right_gt.

theories/function_spaces.v

@@ -707,8 +707,8 @@ Lemma uniform_set1 F (f : U -> V) (x : U) :
   Filter F -> {uniform [set x], F --> f} = (g x @[g --> F] --> f x).
 Proof.
 move=> FF; rewrite propeqE; split.
-  move=> + W => /(_ [set t | W (t x)]) +; rewrite -nbhs_entourageE.
-  rewrite uniform_nbhs => + [Q entQ subW].
+  move=> + W => /(_ [set t | W (t x)]) +.
+  rewrite -[in X in _ -> X]nbhs_entourageE uniform_nbhs => + [Q entQ subW].
   by apply; exists Q; split => // h Qf; exact/subW/xsectionP/Qf.
 move=> Ff W; rewrite uniform_nbhs => [[E] [entE subW]].
 apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -772,8 +772,8 @@ Lemma integral_pushforward : measurable D ->
   \int[mu]_(x in phi @^-1` D) (f \o phi) x.
 Proof.
 move=> mD.
-rewrite integralE.
-under [X in X - _]eq_integral do rewrite funepos_comp.
+rewrite [RHS]integralE.
+under [X in X - _]eq_integral do rewrite funepos_comp/=.
 under [X in _ - X]eq_integral do rewrite funeneg_comp.
 rewrite -[X in _ = X - _]ge0_integral_pushforward//; last first.
   exact/measurable_funepos/measurable_funTS.

theories/measure.v

@@ -5439,7 +5439,7 @@ move=> /(_ F') /=.
 have -> : F' Y = F (f @^-1` Y) by rewrite /F' /image_set_system /= setTI.
 move=> /[swap] bigF; apply; split; first exact: sigma_algebra_image.
 move=> A; rewrite /= {}/F' /image_set_system /= setTI.
-set bign := (X in X A) => bignA.
+set bign := (X in X A -> _) => bignA.
 apply: bigF; rewrite big_ord_recl /=; right.
 set bign1 := (X in X (_ @^-1` _)).
 have -> : bign1 = preimage_set_system [set: n.+1.-tuple T] f bign.

theories/normedtype_theory/normed_module.v

@@ -810,7 +810,7 @@ Proof. by move=> /cvg_ex[l fl]; apply: (cvgP (- l)); exact: cvgeN. Qed.
 Lemma is_cvgeNE f : cvg (\- f @ F) = cvg (f @ F).
 Proof.
 rewrite propeqE; split=> /cvgeNP/cvgP//.
-by under eq_is_cvg do rewrite oppeK.
+by under [X in X -> _]eq_is_cvg do rewrite oppeK.
 Qed.
 
 Lemma mule_continuous (r : R) : continuous (mule r%:E).

theories/normedtype_theory/num_normedtype.v

@@ -533,7 +533,7 @@ Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
 Proof.
 have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN.
+by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN.
 Qed.
 #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `cvgNy_compNP`")]
 Notation cvgyNP := cvgNy_compNP (only parsing).
@@ -543,7 +543,7 @@ Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
   f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l.
 Proof.
 have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty.
+by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty.
 Qed.
 
 Section monotonic_itv_bigcup.

theories/probability.v

@@ -1592,7 +1592,7 @@ Let integral_normal_fun : sigma != 0 ->
   (\int[mu]_x (normal_fun x)%:E)%E = normal_peak^-1%:E.
 Proof.
 move=> s0; rewrite -integral_gaussFF'//; apply: eq_integral => /= x _.
-rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1.
+rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1 ?mule1.
   by rewrite normal_gauss_fun.
 by rewrite gt_eqF// sqrtr_gt0 pmulrn_lgt0// exprn_even_gt0.
 Qed.

theories/sequences.v

@@ -834,7 +834,7 @@ case => [|n].
   rewrite /arithmetic_mean/= invr1 mul1r !seriesEnat/=.
   by rewrite big_nat1 subrr big_geq.
 rewrite /arithmetic_mean /= seriesEnat /= big_nat_recl //=.
-under eq_bigr do rewrite eq_sum_telescope.
+under eq_bigr do rewrite [u_ _]eq_sum_telescope.
 rewrite big_split /= big_const_nat iter_addr addr0 addrA -mulrS mulrDr.
 rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA.
 rewrite eq_sum_telescope (addrC (u_ O)) addrK.

theories/topology_theory/num_topology.v

@@ -212,7 +212,7 @@ Qed.
 
 Lemma nearN {R : numFieldType} (x : R) (P : R -> Prop) :
   (\forall y \near - x, P y) <-> \near x, P (- x).
-Proof. by rewrite -near_simpl nbhsN. Qed.
+Proof. by rewrite -[X in X <-> _]near_simpl nbhsN. Qed.
 
 Lemma openN {R : numFieldType} (A : set R) : open A -> open [set - x | x in A].
 Proof.