Analysis builds using set_borel_measurable_def, etc.

--- a/src/HOL/Analysis/Ball_Volume.thy	Wed Apr 11 16:34:52 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy	Thu Apr 12 12:16:34 2018 +0100
@@ -43,7 +43,7 @@
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
                           indicator {0..1} x) \<partial>lborel)"
     by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
-       (auto intro!: derivative_eq_intros continuous_intros)
+       (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
   also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
     by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
        (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)

--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 11 16:34:52 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 12 12:16:34 2018 +0100
@@ -1545,7 +1545,7 @@
     using that by (subst Ln_minus) (auto simp: Ln_of_real)
   have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
     using *[of "-x"] that by simp
-  have cont: "set_borel_measurable borel (- \<real>\<^sub>\<le>\<^sub>0) Ln"
+  have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
     by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
   have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
     (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto

--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 11 16:34:52 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 12 12:16:34 2018 +0100
@@ -876,9 +876,9 @@
      using of_nat_neq_0[of "2*n"] by (simp only: of_nat_Suc) (simp add: add_ac)
   hence nz': "of_nat n + (1/2::'a) \<noteq> 0" by (simp add: field_simps)
   have "Digamma (of_nat (Suc n) + 1/2 :: 'a) = Digamma (of_nat n + 1/2 + 1)" by simp
-  also from nz' have "\<dots> = Digamma (of_nat n + 1 / 2) + 1 / (of_nat n + 1 / 2)"
+  also from nz' have "\<dots> = Digamma (of_nat n + 1/2) + 1 / (of_nat n + 1/2)"
     by (rule Digamma_plus1)
-  also from nz nz' have "1 / (of_nat n + 1 / 2 :: 'a) = 2 / (2 * of_nat n + 1)"
+  also from nz nz' have "1 / (of_nat n + 1/2 :: 'a) = 2 / (2 * of_nat n + 1)"
     by (subst divide_eq_eq) simp_all
   also note Suc
   finally show ?case by (simp add: add_ac)
@@ -2048,7 +2048,7 @@
   from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
   from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \<notin> \<int>\<^sub>\<le>\<^sub>0"
     by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all
-  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real)
+  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real)
   from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis
     by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
 qed
@@ -2735,11 +2735,12 @@
   have "?f absolutely_integrable_on ({0<..x0} \<union> {x0..})"
   proof (rule set_integrable_Un)
     show "?f absolutely_integrable_on {0<..x0}"
+      unfolding set_integrable_def
     proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
-      show "set_integrable lebesgue {0<..x0} (\<lambda>x. x powr (Re z - 1))" using x0(1) assms
-        by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto
-      show "set_borel_measurable lebesgue {0<..x0}
-              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))"
+      show "integrable lebesgue (\<lambda>x. indicat_real {0<..x0} x *\<^sub>R x powr (Re z - 1))"         
+        using x0(1) assms
+        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_powr_from_0') auto
+      show "(\<lambda>x. indicat_real {0<..x0} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue"
         by (intro measurable_completion)
            (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
       fix x :: real 
@@ -2751,11 +2752,11 @@
     qed
   next
     show "?f absolutely_integrable_on {x0..}"
+      unfolding set_integrable_def
     proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
-      show "set_integrable lebesgue {x0..} (\<lambda>x. exp (-(a/2) * x))" using assms
-        by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto
-      show "set_borel_measurable lebesgue {x0..}
-              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1)
+      show "integrable lebesgue (\<lambda>x. indicat_real {x0..} x *\<^sub>R exp (- (a / 2) * x))" using assms
+        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_exp_minus_to_infinity) auto
+      show "(\<lambda>x. indicat_real {x0..} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue" using x0(1)
         by (intro measurable_completion)
            (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
       fix x :: real 
@@ -3015,14 +3016,15 @@
   qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 D_def)
   have [simp]: "C \<ge> 0" "D \<ge> 0" by (simp_all add: C_def D_def)
 
-  have I1: "set_integrable lborel {0..1 / 2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  have I1: "set_integrable lborel {0..1/2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+    unfolding set_integrable_def
   proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
-    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1 / 2}"
+    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1/2}"
       by (rule integrable_on_powr_from_0) (use assms in auto)
-    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1 / 2}"
+    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1/2}"
       by (subst absolutely_integrable_on_iff_nonneg) auto
-    from integrable_mult_right[OF this, of C]
-      show "set_integrable lborel {0..1 / 2} (\<lambda>t. C * t powr (a - 1))"
+    from integrable_mult_right[OF this [unfolded set_integrable_def], of C]
+    show "integrable lborel (\<lambda>x. indicat_real {0..1/2} x *\<^sub>R (C * x powr (a - 1)))"
       by (subst (asm) integrable_completion) (auto simp: mult_ac)
   next
     fix x :: real
@@ -3033,7 +3035,8 @@
       by (auto simp: indicator_def abs_mult mult_ac)
   qed (auto intro!: AE_I2 simp: indicator_def)
 
-  have I2: "set_integrable lborel {1 / 2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+  have I2: "set_integrable lborel {1/2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
+    unfolding set_integrable_def
   proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
     have "(\<lambda>t. t powr (b - 1)) integrable_on {0..1/2}"
       by (rule integrable_on_powr_from_0) (use assms in auto)
@@ -3042,8 +3045,8 @@
       have "(\<lambda>t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp
     hence "(\<lambda>t. (1 - t) powr (b - 1)) absolutely_integrable_on {1/2..1}"
       by (subst absolutely_integrable_on_iff_nonneg) auto
-    from integrable_mult_right[OF this, of D]
-      show "set_integrable lborel {1 / 2..1} (\<lambda>t. D * (1 - t) powr (b - 1))"
+    from integrable_mult_right[OF this [unfolded set_integrable_def], of D]
+    show "integrable lborel (\<lambda>x. indicat_real {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))"
       by (subst (asm) integrable_completion) (auto simp: mult_ac)
   next
     fix x :: real
@@ -3204,9 +3207,9 @@
 proof -
   from tendsto_inverse[OF tendsto_mult[OF
          sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
-    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
+    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
     by (simp add: prod_inversef [symmetric])
-  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
+  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) =
                (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
     by (intro ext prod.cong refl) (simp add: divide_simps)
   finally show ?thesis .

--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Wed Apr 11 16:34:52 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Apr 12 12:16:34 2018 +0100
@@ -74,10 +74,12 @@
                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
             by (simp only: u'v' max_absorb2 min_absorb1)
                (auto simp: has_field_derivative_iff_has_vector_derivative)
-        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
-          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
+          have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
+            using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
+            by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
         hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
                    LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
+          unfolding set_lebesgue_integral_def
           by (subst nn_integral_eq_integral[symmetric])
              (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
         also from interval_integral_FTC_finite[OF A B]
@@ -129,28 +131,29 @@
       also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
         by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
       also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
+        unfolding set_lebesgue_integral_def
         by (intro integral_FTC_atLeastAtMost[symmetric])
            (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
                  has_vector_derivative_at_within)
       also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
-        using borel_integrable_atLeastAtMost'[OF contg']
+        using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
         by (subst nn_integral_eq_integral)
-           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
+           (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
       also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x))
                             \<in> borel_measurable borel" using Mg'
         by (intro borel_measurable_times_ennreal borel_measurable_indicator)
-           (simp_all add: mult.commute)
+           (simp_all add: mult.commute set_borel_measurable_def)
       have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
                         (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
          by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
       note integrable = borel_integrable_atLeastAtMost'[OF contg']
       with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> top"
-          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique)
+          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
       have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I =
                   \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) -
                         indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel"
         apply (intro nn_integral_diff[symmetric])
-        apply (insert Mg', simp add: mult.commute) []
+        apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
         apply (insert Mg'', simp) []
         apply (simp split: split_indicator add: derivg_nonneg)
         apply (rule notinf)
@@ -185,7 +188,7 @@
       also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
         using Mg'
         apply (intro nn_integral_suminf[symmetric])
-        apply (rule borel_measurable_times_ennreal, simp add: mult.commute)
+        apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
         apply (rule borel_measurable_indicator, subst sets_lborel)
         apply (simp_all split: split_indicator add: derivg_nonneg)
         done
@@ -209,7 +212,7 @@
     let ?I = "indicator {a..b}"
     have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
       by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
-         (simp_all add: mult.commute)
+         (simp_all add: mult.commute set_borel_measurable_def)
     also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
       by (intro ext) (simp split: split_indicator)
     finally have Mf': "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
@@ -223,7 +226,7 @@
       fix f :: "real \<Rightarrow> ennreal" assume Mf: "f \<in> borel_measurable borel"
       have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
         by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
-           (simp_all add:  mult.commute)
+           (simp_all add:  mult.commute set_borel_measurable_def)
       also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
         by (intro ext) (simp split: split_indicator)
       finally have "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
@@ -250,7 +253,7 @@
     let ?I = "indicator {a..b}"
     have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
       by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
-         (simp_all add: mult.commute)
+         (simp_all add: mult.commute set_borel_measurable_def)
     also have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ennreal (g' x) * ?I x)"
       by (intro ext) (simp split: split_indicator)
      finally have "... \<in> borel_measurable borel" .
@@ -306,7 +309,7 @@
        (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
   also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
     by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \<open>a < b\<close>])
-       (auto simp add: mult.commute)
+       (auto simp add: mult.commute set_borel_measurable_def)
   also have "... = \<integral>\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
     by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
   also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
@@ -334,13 +337,14 @@
            (\<lambda>x. ennreal (f x * indicator {g a..g b} x))"
     by (intro ext) (simp split: split_indicator)
   with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
-    unfolding real_integrable_def by (force simp: mult.commute)
+    by (force simp: mult.commute set_integrable_def)
   from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
-    unfolding real_integrable_def by (force simp: mult.commute)
+    by (force simp: mult.commute set_integrable_def)
 
   have "LBINT x. (f x :: real) * indicator {g a..g b} x =
           enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
           enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
+    unfolding set_integrable_def
     by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
   also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
       (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
@@ -348,32 +352,33 @@
   also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
                             (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
-       (auto simp: nn_integral_set_ennreal mult.commute)
+       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
       (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
     by (intro nn_integral_cong) (simp split: split_indicator)
   also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
         (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
-       (auto simp: nn_integral_set_ennreal mult.commute)
+       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
 
   also {
     from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
-      unfolding real_integrable_def by simp
-    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
-      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
+      unfolding set_borel_measurable_def set_integrable_def by simp
+    from measurable_compose Mg Mf Mg' borel_measurable_times
+    have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
                      (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _")
-      by (simp add: mult.commute)
+      by (simp add: mult.commute set_borel_measurable_def)
     also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
       using monog by (intro ext) (auto split: split_indicator)
     finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
-      using A B integrable unfolding real_integrable_def
+      using A B integrable unfolding real_integrable_def set_integrable_def
       by (simp_all add: nn_integral_set_ennreal mult.commute)
   } note integrable' = this
 
   have "enn2real (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
                   enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
-                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
+                (LBINT x. f (g x) * g' x * indicator {a..b} x)" 
+    using integrable' unfolding set_integrable_def
     by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   finally show "(LBINT x. f x * indicator {g a..g b} x) =
                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
@@ -391,11 +396,11 @@
   apply (subst (1 2) interval_integral_Icc, fact)
   apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   using integral_substitution(2)[OF assms]
-  apply (simp add: mult.commute)
+  apply (simp add: mult.commute set_lebesgue_integral_def)
   done
 
-lemma set_borel_integrable_singleton[simp]:
-  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
+lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
+  unfolding set_integrable_def
   by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
 
 end