fixes #2045

CHANGELOG_UNRELEASED.md

@@ -260,6 +260,9 @@
 - in `real_interval.v`:
   + lemma `set1_bigcap_oo`
 
+- in `subspace_topology.v`:
+  + lemma `cst_within_continuous`
+
 ### Changed
 
 - in `realsum.v`:

theories/derive.v

@@ -348,7 +348,7 @@ rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
   by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
 rewrite /g2.
 have [->|v0] := eqVneq v 0.
-  rewrite (_ : (fun _ => _) = cst 0); last exact: cvg_cst.
+  rewrite (_ : (fun _ => _) = cst 0)//.
   by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
 apply/cvgrPdist_lt => e e0.
 rewrite nearE /=; apply/nbhs_ballP.
@@ -1372,8 +1372,8 @@ have fn0 : 0^' [set h | f (h *: v + x) != 0].
 have : (fun h => - ((f x)^-1 * (f (h *: v + x))^-1) *:
   (h^-1 *: (f (h *: v + x) - f x))) @ 0^' -->
   - (f x) ^- 2 *: 'D_v f x.
-  by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM;
-     [exact: cvg_cst|  exact: cvgV].
+  by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM => //;
+     exact: cvgV.
 apply: cvg_trans => A [_/posnumP[e] /= Ae].
 move: fn0; apply: filter_app; near=> h => /= fhvxn0.
 have he : ball 0 e%:num (h : R) by near: h; exists e%:num => /=.
@@ -2149,9 +2149,8 @@ move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
         h (shift x (k *: v)) @[k --> nbhs 0^'] --> h x.
       move=> ch.
       apply: cvg_comp; last exact: ch.
-      rewrite -[in nbhs x](add0r x).
-      apply: cvgD; last exact: cvg_cst.
-      rewrite -(scale0r v); apply: cvgZ; last exact: cvg_cst.
+      rewrite -[in nbhs x](add0r x); apply: cvgD => //.
+      rewrite -(scale0r v); apply: cvgZ => //.
       exact: nbhs_dnbhs.
     apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
     by apply: cvgB; exact: Hf.

theories/esum.v

@@ -877,7 +877,7 @@ suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R.
   rewrite [X in  X - _]summable_nneseries_lim//; first exact/summable_funepos.
   rewrite [X in _ - X]summable_nneseries_lim//; first exact/summable_funeneg.
   rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
-    by apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB) => //; exact: cvg_cst.
+    exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB).
   apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
   by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge.
 have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R.

theories/ftc.v

@@ -1181,11 +1181,11 @@ Lemma integration_by_substitution_oppr G a b : (a <= b)%R ->
 Proof.
 move=> ab cG; have Dopp: (@GRing.opp R)^`() = cst (-1)%R.
   by apply/funext => z; rewrite derive1E derive_val.
-rewrite (@integration_by_substitution_decreasing -%R)//.
+rewrite (@integration_by_substitution_decreasing -%R _ _ _ ab _ _ _ _ _ cG).
 - by move=> ? ? _ _; rewrite ltrN2.
-- by rewrite Dopp => ? _; exact: cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
+- by rewrite Dopp//; apply: in1W; exact: cst_continuous.
+- by rewrite Dopp.
+- by rewrite Dopp.
 - split => //.
   + by rewrite -at_leftN; exact: cvg_at_left_filter.
   + by rewrite -at_rightN; exact: cvg_at_right_filter.
@@ -1426,19 +1426,17 @@ Proof.
 move=> /continuous_within_itvNycP[cG GNa] G0.
 have Dopp : (@GRing.opp R)^`() = cst (- 1)%R.
   by apply/funext => z; rewrite derive1E derive_val.
-rewrite decreasing_ge0_integration_by_substitutiony//.
+rewrite (decreasing_ge0_integration_by_substitutiony _ _ _ _ _ _ _ G0).
 - by move=> x y _ _; rewrite ltrN2.
-- by rewrite Dopp => ? _; exact: cst_continuous.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- by rewrite Dopp; apply: is_cvgN; exact: is_cvg_cst.
-- split.
-  + by [].
-  + by apply: cvgN; exact: cvg_at_right_filter.
-  exact/cvgNrNy.
+- by rewrite Dopp; apply: in1W; exact: cst_continuous.
+- by rewrite Dopp.
+- by rewrite Dopp.
+- by split => //; apply: cvgN; exact: cvg_at_right_filter.
+- exact/cvgNrNy.
 - exact/continuous_within_itvNycP.
-apply: eq_integral => x _; congr EFin.
-rewrite fctE -[RHS]mulr1; congr *%R.
-by rewrite fctE derive1E deriveN// opprK derive_id.
+- apply: eq_integral => x _; congr EFin.
+  rewrite fctE -[RHS]mulr1; congr *%R.
+  by rewrite fctE derive1E deriveN// opprK derive_id.
 Qed.
 
 Lemma increasing_ge0_integration_by_substitutiony F G a :
@@ -1804,11 +1802,11 @@ have dshiftE : (shift e)^`() = cst 1.
   by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutiony _ (shift e))//=.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE => ? _; exact: cst_continuous.
-- by rewrite dshiftE; exact: is_cvg_cst.
-- by rewrite dshiftE; exact: is_cvg_cst.
+- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
+- by rewrite dshiftE.
+- by rewrite dshiftE.
 - split; first by move=> x _; exact: ex_derive.
-  by apply/cvg_at_right_filter; apply: cvgD => //; exact: cvg_cst.
+  by apply/cvg_at_right_filter; exact: cvgD.
 - exact: cvg_addrr.
 by rewrite dshiftE mulr1.
 Qed.
@@ -1824,11 +1822,11 @@ have dshiftE : (shift e)^`() = cst 1.
   by apply/funext => x; rewrite derive1E -(derive_shift 1 e).
 rewrite (@increasing_ge0_integration_by_substitutionNy _ (shift e))//.
 - by move=> x y _ _ xy; rewrite ltr_leD.
-- by rewrite dshiftE => ? _; exact: cst_continuous.
-- by rewrite dshiftE; exact: is_cvg_cst.
-- by rewrite dshiftE; exact: cvg_cst.
+- by rewrite dshiftE; apply: in1W; exact: cst_continuous.
+- by rewrite dshiftE.
+- by rewrite dshiftE.
 - split; first by move=> x _; exact: ex_derive.
-  by apply/cvg_at_left_filter; apply: cvgD => //; exact: cvg_cst.
+  by apply/cvg_at_left_filter; exact: cvgD.
 - exact: cvg_addrr_Ny.
 by rewrite dshiftE mulr1.
 Qed.
@@ -1855,16 +1853,16 @@ rewrite onemK onem1 => -> //; last 1 first.
 - by apply: eq_integral => x xr; rewrite !fctE derive1_onem opprK mulr1.
 - by rewrite lerBlDl lerDr ltW.
 - by move=> x y _ _ xy; rewrite ler_ltB.
-- by rewrite derive1_onem; move=> ? ?; exact: cvg_cst.
-- by rewrite derive1_onem; exact: is_cvg_cst.
-- by rewrite derive1_onem; exact: is_cvg_cst.
+- by rewrite derive1_onem; apply: in1W; exact: cst_continuous.
+- by rewrite derive1_onem.
+- by rewrite derive1_onem.
 split => /=.
 - by move=> x xr1; exact: derivableB.
 - apply: cvg_at_right_filter; rewrite onemK.
   apply: (@continuous_comp_cvg _ _ _ _ onem)=> //=.
-    by move=> x; apply: continuousB => //; exact: cvg_cst.
+    by move=> x; apply: continuousB => //; exact: cst_continuous.
   by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id.
-- by apply: cvg_at_left_filter; apply: cvgB => //; exact: cvg_cst.
+- by apply: cvg_at_left_filter; exact: cvgB.
 Qed.
 
 Lemma Rintegration_by_substitution_onem (G : R -> R) (r : R) :

theories/gauss_integral.v

@@ -255,14 +255,12 @@ have := @integration_by_substitution_increasing R (fun t => t * x)
 rewrite -/mu mul0r mul1r => ->//=.
 - move=> a b; rewrite !in_itv/= => /andP[a0 a1] /andP[b0 b1] ab.
     by rewrite ltr_pM2r.
-- by rewrite derM => z _; exact: cvg_cst.
-- by rewrite derM; exact: is_cvg_cst.
-- by rewrite derM; exact: is_cvg_cst.
+- by rewrite derM; apply: in1W; exact: cst_continuous.
+- by rewrite derM.
+- by rewrite derM.
 - split => //.
-  + apply: cvg_at_right_filter.
-    by apply: cvgM => //; exact: cvg_cst.
-  + apply: cvg_at_left_filter.
-    by apply: cvgM => //; exact: cvg_cst.
+  + by apply: cvg_at_right_filter; exact: cvgM.
+  + by apply: cvg_at_left_filter; exact: cvgM.
 - by apply: continuous_subspaceT; exact: continuous_gauss_fun.
 rewrite derM.
 under eq_integral do rewrite fctE/= EFinM.
@@ -300,7 +298,7 @@ rewrite fine_le//.
   by apply: continuous_in_subspaceT => z _; exact: continuous_u.
 - apply: integrable_fin_num => //=.
   apply: continuous_compact_integrable; first exact: segment_compact.
-  by apply: continuous_subspaceT => z; exact: cvg_cst.
+  exact: cst_within_continuous.
 apply: ge0_le_integral => //=.
 - by move=> y _; rewrite lee_fin u_ge0.
 - by apply/measurable_EFinP => /=; apply/measurable_funTS; exact: measurable_u.
@@ -309,9 +307,8 @@ Qed.
 
 Let cvg_integral01_u : integral01_u x @[x --> +oo] --> 0.
 Proof.
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss_fun).
+apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss_fun) => //.
 - by near=> n => /=; rewrite integral01_u_gauss_fun integral01_u_ge0.
-- exact: cvg_cst.
 - exact: cvg_gauss_fun.
 Unshelve. all: end_near. Qed.
 
@@ -342,8 +339,7 @@ have Ig2 x : 0 < x -> (integral0_gauss x) ^+ 2 = pi / 4 - integral01_u x.
 suff: pi / 4 - integral01_u x @[x --> +oo] --> pi / 4.
   apply: cvg_trans; apply: near_eq_cvg.
   by near=> x; rewrite Ig2.
-rewrite -[in X in _ --> X](subr0 (pi / 4)).
-by apply: cvgB => //; exact: cvg_cst.
+by rewrite -[in X in _ --> X](subr0 (pi / 4)); exact: cvgB.
 Unshelve. end_near. Qed.
 
 End gauss_integral_proof.

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -225,17 +225,16 @@ have intRf : mu.-integrable `[x - r, x + r] (EFin \o f).
   exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf).
 rewrite /= -mulrBr -fineB.
 - by rewrite integrable_fin_num.
-- rewrite integrable_fin_num// continuous_compact_integrable// => ?.
-  exact: cvg_cst.
+- rewrite integrable_fin_num// continuous_compact_integrable//.
+  exact: cst_within_continuous.
 rewrite -integralB_EFin //.
-  by apply: continuous_compact_integrable => // ?; exact: cvg_cst.
+  by apply: continuous_compact_integrable => //; exact: cst_within_continuous.
 under [fun _ => _ + _ ]eq_fun => ? do rewrite -EFinD.
 have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E).
   under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB.
-  rewrite integrableB// continuous_compact_integrable// => ?.
-  exact: cvg_cst.
-rewrite normrM ger0_norm // -fine_abse //.
-  by rewrite integrable_fin_num.
+  rewrite integrableB// continuous_compact_integrable//.
+  exact: cst_within_continuous.
+rewrite normrM ger0_norm// -fine_abse//; first by rewrite integrable_fin_num.
 suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
     (r *+ 2 * eps)%:E)%E.
   move=> intfeps; apply: le_trans.
@@ -1130,7 +1129,7 @@ apply: (sube_cvg0 _ _).1 => //.
 move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax.
 have : (mu (ball x r))^-1 *
        `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0.
-  apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //; [|exact: cvg_cst].
+  apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //.
   near=> a; rewrite mule_ge0 ?inve_ge0///= lee_pmul2l//.
     by rewrite lebesgue_measure_ball// fin_numV// eqe mulrn_eq0/= gt_eqF.
     rewrite lebesgue_measure_ball// inver mulrn_eq0/= gt_eqF// lte_fin.
@@ -1243,11 +1242,10 @@ have E_r_ n : E x n `<=` ball x (r_ x n)%:num.
 have muEr_ n : mu (ball x (r_ x n)%:num) <= C%:E * mu (E x n).
   by rewrite /C /r_ /sval/=; case: cid => -[? ?] [].
 apply: (@squeeze_cvge _ _ _ _ (cst 0) _
-  (fun n => C%:E * davg f x (r_ x n)%:num)); last 2 first.
-  exact: cvg_cst.
+    (fun n => C%:E * davg f x (r_ x n)%:num)) => //; last first.
   move/cvge_at_rightP: fx => /(_ (fun r => (r_ x r)%:num)) fx.
-  by rewrite -(mule0 C%:E); apply: cvgeM => //;
-    [exact: cvg_cst | apply: fx; split => //; exact: r_0].
+  by rewrite -(mule0 C%:E); apply: cvgeM => //; apply: fx; split => //;
+    exact: r_0.
 near=> n.
 apply/andP; split => //=.
 apply: (@le_trans _ _ ((mu (E x n))^-1 *
@@ -1289,7 +1287,7 @@ rewrite muleA lee_pmul//.
   rewrite -(@invrK _ C) -invfM lee_fin lef_pV2//.
     rewrite posrE fine_gt0// (nicely_shrinking_gt0 (hE x))//=.
     by rewrite (nicely_shrinking_lty (hE x)).
-    by rewrite posrE mulr_gt0// ?invr_gt0// fine_gt0//.
+    by rewrite posrE mulr_gt0 ?invr_gt0 ?fine_gt0.
   rewrite lter_pdivrMl // -lee_fin EFinM fineK.
     by rewrite (nicely_shrinking_fin_num (hE x)).
   by have := muEr_ n; rewrite lebesgue_measure_ball.

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -156,9 +156,8 @@ suff: `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | @[n \oo] --> 0.
    rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl.
    move: dominated_integrable => /integrableP[?]; apply: le_lt_trans.
    by apply: (le_trans _ (@le_abse_integral _ _ _ mu D f mD _)).
-apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)).
+apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)) => //.
 - by apply: nearW => n; rewrite abse_ge0//=; exact: h.
-- exact: cvg_cst.
 - exact: dominated_cvg0.
 Qed.
 
@@ -193,7 +192,7 @@ pose f' := f \_ (D `\` N); pose g' := g \_ (D `\` N).
 pose f_' := fun n => f_ n \_ (D `\` N).
 have f_f' x : D x -> f_' ^~ x @ \oo --> f' x.
   move=> Dx; rewrite /f_' /f' /restrict in_setD mem_set//=.
-  have [/= xN|/= xN] := boolP (x \in N); first exact: cvg_cst.
+  have [//=|/= xN] := boolP (x \in N).
   apply: contraPP (xN) => h; apply/negP; rewrite negbK inE; left; left.
   by apply: subN1 => /= /(_ Dx); exact: contra_not h.
 have f_g' n x : D x -> `|f_' n x| <= g' x.

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -293,8 +293,8 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
     near: n; exists (truncn (M / r)).+1 => // m /= Mrm.
     by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
   - rewrite -fx0 mule0 /g -fx0.
-    under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
-    exact: cvg_cst.
+    rewrite [X in X @ _](_ : _ = cst 0)//.
+    by under eq_fun do rewrite mule0.
 rewrite (monotone_convergence mu mD mg g0 nd_g).
 under eq_fun do rewrite /g ge0_integralZl_EFin//.
 have : 0 <= \int[mu]_(x in D) f x by exact: integral_ge0.

theories/lebesgue_integral_theory/lebesgue_integral_under.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
 From mathcomp Require Import interval_inference archimedean finmap.
@@ -270,11 +270,10 @@ apply: norm_cvg0.
 have {}g_d1f_0 : (\int[mu]_(y in B) `|g_ n y - ('d1 f) a y|) @[n --> \oo] --> 0.
   exact/fine_cvg.
 apply: (@squeeze_cvgr _ _ _ _ (cst 0) _ _ _ _ _ g_d1f_0) => //.
-- apply/nearW => n.
-  rewrite /= normr_ge0/= le_normr_Rintegral//.
-  rewrite /comp; under eq_fun do rewrite EFinB.
-  by apply: integrableB => //; exact: intg_.
-- exact: cvg_cst.
+apply/nearW => n.
+rewrite /= normr_ge0/= le_normr_Rintegral//.
+rewrite /comp; under eq_fun do rewrite EFinB.
+by apply: integrableB => //; exact: intg_.
 Unshelve. all: end_near. Qed.
 
 Lemma differentiation_under_integral :

theories/lebesgue_integral_theory/measurable_fun_approximation.v

@@ -753,9 +753,9 @@ exists (\bigcup_(i in range f) dK i); split.
   + by move=> ? ? [? ?][? ?]; split; [exact: closedU|exact: withinU_continuous].
   + move=> i _; split; first by apply: compact_closed; have [] := dkP i.
     apply: (continuous_subspaceW (dKsub i)).
-    apply: (@subspace_eq_continuous _ _ _ (fun=> i)).
+    apply: (@subspace_eq_continuous _ _ _ (cst i)).
       by rewrite /from_subspace => ? /set_mem ->.
-    by apply: continuous_subspaceT => ?; exact: cvg_cst.
+    exact: cst_continuous.
 Qed.
 
 Let measurable_almost_continuous' (f : rT -> rT) (eps : rT) :

theories/measure_theory/counting_measure.v

@@ -65,9 +65,8 @@ have [cvg_u|dvg_u] := pselect (cvg (nseries u @ \oo)).
       rewrite [X in _ `|` X](_ : _ = set0) ?setU0// bigcup0// => i [_ /negP].
       by rewrite -leqNgt => /Nu/eqP/[!cardfs_eq0]/eqP/fset_set_set0 ->.
     by rewrite /counting /= asboolT ?sumFE// -bigcup_mkord; exact: bigcup_finite.
-  rewrite -(cvg_shiftn N)/=.
-  rewrite (_ : (fun n => _) = (fun=> \sum_(i < N) counting (F i))); last first.
-    exact: cvg_cst.
+  set l := (X in _ --> X); rewrite -(cvg_shiftn N)/= -[X in _ --> X]/(nbhs l).
+  rewrite [X in X @ _](_ : _ = cst l)//.
   apply/funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
   rewrite [X in _ + X](_ : _ = 0) ?adde0; last first.
     by rewrite -{1}(subn0 N) big_mkord.

theories/measure_theory/dirac_measure.v

@@ -50,7 +50,7 @@ move=> F mF tF mUF; rewrite /dirac indicE; have [|aFn] /= := boolP (a \in _).
   rewrite big_mkord (bigID (xpred1 (Ordinal mn)))//= big_pred1_eq/= big1/=.
     by move=> j ij; rewrite indicE (negbTE (naF _ _)).
   by rewrite adde0 indicE mem_set//; exact: ballxx.
-rewrite [X in X @ \oo --> _](_ : _ = cst 0); last exact: cvg_cst.
+rewrite [X in X @ _ --> _](_ : _ = cst 0)//.
 apply/funext => n; rewrite big1// => i _; rewrite indicE; apply/eqP.
 by rewrite eqe pnatr_eq0 eqb0; apply: contra aFn => /[!inE] aFn; exists i.
 Unshelve. all: by end_near. Qed.

theories/measure_theory/measure_extension.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
@@ -199,11 +199,10 @@ Lemma le_outer_measureIC (R : realFieldType) T
 Proof.
 pose B : (set T) ^nat := bigcup2 (X `&` A) (X `&` ~` A).
 have cvg_mu : (fun n => \sum_(i < n) mu (B i)) @ \oo --> mu (B 0%N) + mu (B 1%N).
-  rewrite -2!cvg_shiftS /=.
-  rewrite [X in X @ \oo --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N))).
-    rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
-    by rewrite /B /bigcup2 /=.
-  exact: cvg_cst.
+  set l := (X in _ --> X); rewrite -2!cvg_shiftS -[X in _ --> X]/(nbhs l)/=.
+  rewrite [X in X @ _ --> _](_ : _ = cst l)//.
+  rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _.
+  by rewrite /B /bigcup2 /=.
 have := outer_measure_sigma_subadditive mu B.
 suff : \bigcup_n B n = X.
   move=> -> /le_trans; apply; under eq_fun do rewrite big_mkord.
@@ -637,18 +636,19 @@ Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
   measurable X -> mu^* X = mu X.
 Proof.
 move=> mX; apply/eqP; rewrite eq_le; apply/andP; split.
-  apply: ereal_inf_lbound; exists (fun n => if n is 0%N then X else set0).
-    by split=> [[]// _|t Xt]; exists 0%N.
-  apply/cvg_lim => //; rewrite -cvg_shiftS.
-  rewrite (_ : [sequence _]_n = cst (mu X)); last exact: cvg_cst.
+  set f := fun n => if n is 0%N then X else set0.
+  apply: ereal_inf_lbound; exists f.
+    by split=> [[]//=|t Xt]; exists 0%N.
+  apply/cvg_lim => //; rewrite -cvg_shiftS -[X in _ --> X]/(nbhs (mu X)).
+  rewrite [X in X @ _](_ : _ = cst (mu X))//.
   by rewrite funeqE => n /=; rewrite big_nat_recl//= big1 ?adde0.
 apply/le_ereal_inf_tmp => x [A [mA XA] <-{x}].
 have XUA : X = \bigcup_n (X `&` A n).
   rewrite predeqE => t; split => [Xt|[i _ []//]].
   by have [i _ Ait] := XA _ Xt; exists i.
 apply: (@le_trans _ _ (\sum_(i <oo) mu (X `&` A i))%E).
-  by rewrite measure_sigma_subadditive//= -?XUA => // i; apply: measurableI.
-apply: lee_lim; [exact: is_cvg_nneseries|exact: is_cvg_nneseries|].
+  by rewrite measure_sigma_subadditive//= -?XUA => // i; exact: measurableI.
+apply: lee_lim; [exact: is_cvg_nneseries..|].
 by apply: nearW => n; apply: lee_sum => i  _; exact: measureIr.
 Qed.