test with hints

Author: affeldt-aist

theories/kernel.v

@@ -120,8 +120,7 @@ Definition kseries : X -> {measure set Y -> \bar R} :=
   fun x => [the measure _ _ of mseries (k ^~ x) 0].
 
 Lemma measurable_fun_kseries (U : set Y) :
-  measurable U ->
-  measurable_fun setT (kseries ^~ U).
+  measurable U -> measurable_fun setT (kseries ^~ U).
 Proof.
 move=> mU.
 by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel.
@@ -210,8 +209,7 @@ Definition kzero : X -> {measure set Y -> \bar R} :=
   fun _ : X => [the measure _ _ of mzero].
 
 Let measurable_fun_kzero U : measurable U ->
-  measurable_fun setT (kzero ^~ U).
-Proof. by move=> ?/=; exact: measurable_fun_cst. Qed.
+  measurable_fun setT (kzero ^~ U). Proof. by []. Qed.
 
 HB.instance Definition _ :=
   @isKernel.Build _ _ X Y R kzero measurable_fun_kzero.
@@ -422,13 +420,12 @@ have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT.
 have CXY : C `<=` XY.
   move=> _ [A mA [B mB <-]]; split; first exact: measurableM.
   rewrite phiM.
-  apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI.
-  by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA).
+  by apply: emeasurable_funM => //; [exact/measurable_kernel/measurableI|auto].
 suff monoB : monotone_class setT XY by exact: monotone_class_subset.
 split => //; [exact: CXY| |exact: xsection_ndseq_closed].
 move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD.
 suff : phi (A `\` B) = (fun x => phi A x - phi B x).
-  by move=> ->; exact: emeasurable_funB.
+  by move=> ->; auto.
 rewrite funeqE => x; rewrite /phi/= xsectionD// measureD.
 - by rewrite setIidr//; exact: le_xsection.
 - exact: measurable_xsection.
@@ -454,9 +451,9 @@ Let phi A := fun x => k x (xsection A x).
 Let XY := [set A | measurable A /\ measurable_fun setT (phi A)].
 
 Lemma measurable_fun_xsection_finite_kernel A :
-  A \in measurable -> measurable_fun setT (phi A).
+  measurable A -> measurable_fun setT (phi A).
 Proof.
-move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[].
+move: A; suff : measurable `<=` XY by move=> + A => /[apply] -[].
 move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ =
     (fun x => mrestr (k x) measurableT (xsection A x))); last first.
   by apply/funext => x//=; rewrite /mrestr setIT.
@@ -487,15 +484,12 @@ rewrite (_ : (fun x => _) =
   transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first.
     rewrite is_cvg_lim_esupE//.
     apply: ereal_nondecreasing_is_cvg => m n mn.
-    apply: ge0_le_integral => //.
+    apply: ge0_le_integral => //; [|by auto| |by auto|].
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurable_fun_prod1.
     - by move=> y _; rewrite lee_fin.
-    - exact/EFin_measurable_fun/measurable_fun_prod1.
     - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
-  rewrite -monotone_convergence//.
+  rewrite -monotone_convergence//; [|by auto| |].
   - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k.
-  - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1.
   - by move=> n y _; rewrite lee_fin.
   - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
 apply: measurable_fun_lim_esup => n.
@@ -505,22 +499,15 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y
   by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE.
 rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
     (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first.
-  apply/funext => x; rewrite -ge0_integral_fsum//.
+  apply/funext => x; rewrite -ge0_integral_fsum//; [|by auto|].
   - by apply: eq_integral => y _; rewrite -fsumEFin.
-  - move=> r.
-    apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=.
-    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//.
-    exact/measurable_funP.
   - by move=> m y _; rewrite nnfun_muleindic_ge0.
 apply: emeasurable_fun_fsum => // r.
 rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
     \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.
   apply/funext => x; under eq_integral do rewrite EFinM.
   have [r0|r0] := leP 0%R r.
-    rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin.
-    apply/EFin_measurable_fun/measurable_fun_prod1 => /=.
-    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//.
-    exact/measurable_funP.
+    by rewrite ge0_integralM//; [auto|move=> y _; rewrite lee_fin].
   rewrite integral0_eq; last first.
     by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
   by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0.
@@ -785,16 +772,14 @@ apply: measurable_fun_if => //.
                            [set t | k t setT == +oo]); last first.
     by apply/seteqP; split=> x /= /orP//.
   by apply: measurableU; exact: kernel_measurable_eq_cst.
-- exact: measurable_fun_cst.
 - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
   apply/EFin_measurable_fun; rewrite setTI.
   apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
   + exact: open_measurable.
   + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
   + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
     exact: inv_continuous.
-  + apply: measurable_funT_comp; last exact/measurable_funS/measurable_kernel.
-    exact: measurable_fun_fine.
+  + by apply: measurable_funT_comp => //; exact/measurable_funS/measurable_kernel.
 Qed.
 
 Section knormalize.
@@ -815,15 +800,12 @@ rewrite (_ : (fun _ => _) = (fun x =>
      else f x U * (fine (f x setT))^-1%:E)); last first.
   apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn.
   by rewrite negb_or=> /andP[/negbTE -> /negbTE ->].
-apply: measurable_fun_if => //;
-  [exact: kernel_measurable_fun_eq_cst|exact: measurable_fun_cst|].
+apply: measurable_fun_if => //; first exact: kernel_measurable_fun_eq_cst.
 apply: measurable_fun_if => //.
 - rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]).
     exact: kernel_measurable_neq_cst.
   by apply/seteqP; split => [x /negbT//|x /negbTE].
-- apply: (@measurable_funS _ _ _ _ setT) => //.
-  exact: kernel_measurable_fun_eq_cst.
-- exact: measurable_fun_cst.
+- exact/measurable_funTS/kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
     by have := measurable_kernel f U mU; exact: measurable_funS.
   apply/EFin_measurable_fun.
@@ -834,7 +816,7 @@ apply: measurable_fun_if => //.
     by rewrite ge0_fin_numE// lt_neqAle leey ftoo.
   + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
     exact: inv_continuous.
-  + apply: measurable_funT_comp => /=; first exact: measurable_fun_fine.
+  + apply: measurable_funT_comp => //=.
     by have := measurable_kernel f _ measurableT; exact: measurable_funS.
 Qed.
 
@@ -937,7 +919,6 @@ apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)).
   apply: ge0_le_integral => //.
   - have /measurable_fun_prod1 := measurable_kernel k _ measurableT.
     exact.
-  - exact/measurable_fun_cst.
   - by move=> y _; exact/ltW/hr.
 by rewrite integral_cst//= EFinM lte_pmul2l.
 Qed.
@@ -1026,7 +1007,7 @@ Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed.
 HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n).
 
 Let mk_2 n : measurable_fun setT (k_2 n).
-Proof. by apply: measurable_funT_comp => //; exact: measurable_fun_snd. Qed.
+Proof. exact: measurable_funT_comp. Qed.
 
 HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n).
 
@@ -1086,19 +1067,13 @@ Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) :
   \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E).
 Proof.
 under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//.
-rewrite ge0_integral_fsum//; last 2 first.
-  - move=> r; apply/EFin_measurable_fun/measurable_funrM.
-    have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
-    by rewrite (_ : \1__ = mindic R fr).
+rewrite ge0_integral_fsum//; [|by auto|]; last first.
   - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
 under [in RHS]eq_integral.
   move=> y _.
   under eq_integral.
     by move=> z _; rewrite fimfunE -fsumEFin//; over.
-  rewrite /= ge0_integral_fsum//; last 2 first.
-    - move=> r; apply/EFin_measurable_fun/measurable_funrM.
-      have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
-      by rewrite (_ : \1__ = mindic R fr).
+  rewrite /= ge0_integral_fsum//; [|by auto|]; last first.
     - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
   under eq_fsbigr.
     move=> r _.
@@ -1138,32 +1113,27 @@ move=> f0 mf.
 have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
 transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))).
   by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f.
-rewrite monotone_convergence//; last 3 first.
-  by move=> n; exact/EFin_measurable_fun.
+rewrite monotone_convergence//; [|by auto| |]; last 2 first.
   by move=> n z _; rewrite lee_fin.
   by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
 rewrite (_ : (fun _ => _) =
     (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first.
   by apply/funext => n; rewrite integral_kcomp_nnsfun.
 transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)).
   rewrite -monotone_convergence//; last 3 first.
-  - move=> n; apply: measurable_fun_integral_kernel => //.
+  - move=> n; apply: measurable_fun_integral_kernel => //; last by auto.
     + move=> U mU; have := measurable_kernel k _ mU.
       by move=> /measurable_fun_prod1; exact.
     + by move=> z; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
   - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin.
-  - move=> y _ a b ab; apply: ge0_le_integral => //.
+  - move=> y _ a b ab; apply: ge0_le_integral => //; [|by auto| |by auto|].
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
     + by move=> z _; rewrite lee_fin.
-    + exact/EFin_measurable_fun.
     + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin.
-apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.
-  - by move=> n; exact/EFin_measurable_fun.
-  - by move=> n z _; rewrite lee_fin.
-  - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
-by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
+apply: eq_integral => y _; rewrite -monotone_convergence//; [|auto| |].
+- by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
+- by move=> n z _; rewrite lee_fin.
+- by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
 Qed.
 
 End integral_kcomp.