# HG changeset patch
# User paulson
# Date 1604083741 0
# Node ID 41bae8c80c9c6bc8496a1e769d5e875ac644138f
# Parent  4be6ae020fc4faf7b36eb597ec3cc9fdd7165c1d# Parent  546eb2882a841b254fbef1b3475427825e7e6a06
merged

diff -r 4be6ae020fc4 -r 41bae8c80c9c src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Oct 29 16:07:41 2020 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Oct 30 18:49:01 2020 +0000
@@ -14,6 +14,10 @@
     Cartesian_Euclidean_Space
 begin
 
+lemma LIMSEQ_if_less: "(\<lambda>k. if i < k then a else b) \<longlonglongrightarrow> a"
+  by (rule_tac k="Suc i" in LIMSEQ_offset) auto
+
+text \<open>Note that the rhs is an implication. This lemma plays a specific role in one proof.\<close>
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
   by (auto intro: order_trans)
 
@@ -227,8 +231,8 @@
         also have "\<dots> = ?\<mu> E - ?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})"
           using \<open>E \<in> sets ?L\<close> fin[of X] sets[of X] by (auto intro!: emeasure_Diff)
         finally have "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}}) \<le> e"
-          using \<open>0 < e\<close> e_less_M apply (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})")
-          by (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
+          using \<open>0 < e\<close> e_less_M 
+          by (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})") (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
         note this }
       note upper_bound = this
 
@@ -345,12 +349,8 @@
     proof cases
       assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
       then show ?thesis
-        apply simp
-        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
-        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
         using has_integral_const[of "1::real" l u]
-        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
-        done
+        by (simp flip: has_integral_restrict[OF box_subset_cbox] add: has_integral_spike_interior)
     next
       assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
       then have "box l u = {}"
@@ -405,11 +405,8 @@
           by (intro sum_mono2) auto
         from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
           by (auto simp add: disjoint_family_on_def)
-        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)"
-          apply (auto simp: * sum.If_cases Iio_Int_singleton)
-          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
-          apply simp
-          done
+        show "(\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)" for x
+          by (auto simp: * sum.If_cases Iio_Int_singleton if_distrib LIMSEQ_if_less cong: if_cong)
         have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
           by (intro emeasure_mono) auto
 
@@ -486,14 +483,8 @@
   case (seq U)
   note seq(1)[measurable] and f[measurable]
 
-  { fix i x
-    have "U i x \<le> f x"
-      using seq(5)
-      apply (rule LIMSEQ_le_const)
-      using seq(4)
-      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
-      done }
-  note U_le_f = this
+  have U_le_f: "U i x \<le> f x" for i x
+    by (metis (no_types) LIMSEQ_le_const UNIV_I incseq_def le_fun_def seq.hyps(4) seq.hyps(5) space_borel)
 
   { fix i
     have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
@@ -910,9 +901,7 @@
     using assms has_integral_integral_lborel
     unfolding set_integrable_def set_lebesgue_integral_def by blast
   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
-    apply (subst has_integral_restrict_UNIV [symmetric])
-    apply (rule has_integral_eq)
-    by auto
+    by (simp add: indicator_scaleR_eq_if)
   thus "f integrable_on S"
     by (auto simp add: integrable_on_def)
   with 1 have "(f has_integral (integral S f)) S"
@@ -1088,8 +1077,8 @@
 lemma absolutely_integrable_reflect[simp]:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "(\<lambda>x. f(-x)) absolutely_integrable_on cbox (-b) (-a) \<longleftrightarrow> f absolutely_integrable_on cbox a b"
-  apply (auto simp: absolutely_integrable_on_def dest: integrable_reflect [THEN iffD1])
-  unfolding integrable_on_def by auto
+  unfolding absolutely_integrable_on_def
+  by (metis (mono_tags, lifting) integrable_eq integrable_reflect)
 
 lemma absolutely_integrable_reflect_real[simp]:
   fixes f :: "real \<Rightarrow> 'b::euclidean_space"
@@ -1168,15 +1157,16 @@
 proof -
   have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
     by (meson indicator_def)
-  moreover
-  have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
+  moreover have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
     using assms by (simp add: lmeasurable_iff_has_integral)
   ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
     by (metis (no_types) integral_unique)
-  then show ?thesis
-    using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
-    apply (simp add: integral_restrict_Int [symmetric])
+  moreover have "integral T (\<lambda>a. if a \<in> S then 1::real else 0) = integral (S \<inter> T \<inter> UNIV) (\<lambda>a. 1)"
+    by (simp add: Henstock_Kurzweil_Integration.integral_restrict_Int)
+  moreover have "integral T (indicat_real S) = integral T (\<lambda>a. if a \<in> S then 1 else 0)"
     by (meson indicator_def)
+  ultimately show ?thesis
+    by (simp add: assms lmeasure_integral)
 qed
 
 lemma measurable_integrable:
@@ -1234,9 +1224,8 @@
     by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
 next
   assume RHS [rule_format]: ?rhs
-  show ?lhs
+  then show ?lhs
     apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
-    using RHS
     by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
 qed
 
@@ -1305,14 +1294,13 @@
   assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
 proof -
   obtain x where x: "a \<bullet> x \<noteq> b"
-    using assms
-    apply auto
-     apply (metis inner_eq_zero_iff inner_zero_right)
-    using inner_zero_right by fastforce
+    using assms by (metis euclidean_all_zero_iff inner_zero_right)
+  moreover have "c = 1" if "a \<bullet> (x + c *\<^sub>R w) = b" "a \<bullet> (x + w) = b" for c w
+    using that
+    by (metis (no_types, hide_lams) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
+  ultimately
   show ?thesis
-    apply (rule starlike_negligible [OF closed_hyperplane, of x])
-    using x apply (auto simp: algebra_simps)
-    done
+    using starlike_negligible [OF closed_hyperplane, of x] by simp
 qed
 
 lemma negligible_lowdim:
@@ -1348,12 +1336,15 @@
            (simp_all add: frontier_def negligible_lowdim 1)
     next
       case 2
-      obtain a where a: "a \<in> interior S"
-        apply (rule interior_simplex_nonempty [OF indB])
-          apply (simp add: indB independent_finite)
-         apply (simp add: cardB 2)
-        apply (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
-        done
+      obtain a where "a \<in> interior (convex hull insert 0 B)"
+      proof (rule interior_simplex_nonempty [OF indB])
+        show "finite B"
+          by (simp add: indB independent_finite)
+        show "card B = DIM('N)"
+          by (simp add: cardB 2)
+      qed
+      then have a: "a \<in> interior S"
+        by (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
       show ?thesis
       proof (rule starlike_negligible_strong [where a=a])
         fix c::real and x
@@ -1361,10 +1352,9 @@
           by (simp add: algebra_simps)
         assume "0 \<le> c" "c < 1" "a + x \<in> frontier S"
         then show "a + c *\<^sub>R x \<notin> frontier S"
-          apply (clarsimp simp: frontier_def)
-          apply (subst eq)
-          apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"], auto)
-          done
+          using eq mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"]
+          unfolding frontier_def
+          by (metis Diff_iff add_diff_cancel_left' add_diff_eq diff_gt_0_iff_gt group_cancel.rule0 not_le)
       qed auto
     qed
   qed
@@ -1426,10 +1416,7 @@
 
 lemma negligible_convex_interior:
    "convex S \<Longrightarrow> (negligible S \<longleftrightarrow> interior S = {})"
-  apply safe
-  apply (metis interior_subset negligible_subset open_interior open_not_negligible)
-   apply (metis Diff_empty closure_subset frontier_def negligible_convex_frontier negligible_subset)
-  done
+  by (metis Diff_empty closure_subset frontier_def interior_subset negligible_convex_frontier negligible_subset open_interior open_not_negligible)
 
 lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
   by (auto simp: measure_def null_sets_def)
@@ -1441,8 +1428,7 @@
   by (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
 
 lemma negligible_iff_measure0: "S \<in> lmeasurable \<Longrightarrow> (negligible S \<longleftrightarrow> measure lebesgue S = 0)"
-  apply (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
-  by (metis completion.null_sets_outer subsetI)
+  by (metis (full_types) completion.null_sets_outer negligible_iff_null_sets negligible_imp_measure0 order_refl)
 
 lemma negligible_imp_sets: "negligible S \<Longrightarrow> S \<in> sets lebesgue"
   by (simp add: negligible_iff_null_sets null_setsD2)
@@ -1474,12 +1460,7 @@
 qed
 
 lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
-proof
-  assume ?rhs
-  then show "negligible S"
-    apply (auto simp: negligible_def has_integral_iff integrable_on_indicator)
-    by (metis negligible integral_unique lmeasure_integral_UNIV negligible_iff_measure0)
-qed (simp add: negligible)
+  by (metis lmeasurable_iff_indicator_has_integral negligible_iff_measure)
 
 lemma sets_negligible_symdiff:
    "\<lbrakk>S \<in> sets lebesgue; negligible((S - T) \<union> (T - S))\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
@@ -1688,11 +1669,7 @@
     then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
       by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
     then show ?thesis
-      apply (rule_tac x="min (1/2) \<epsilon>" in exI)
-      apply (simp del: divide_const_simps)
-      apply (intro allI impI conjI)
-       apply (metis dist_commute dist_norm mem_ball subsetCE)
-      by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
+      by (rule_tac x="min (1/2) \<epsilon>" in exI) (simp add: U dist_norm norm_minus_commute subset_iff)
   next
     case False
     then show ?thesis
@@ -1709,10 +1686,13 @@
     obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
       using \<open>bounded S\<close> bounded_iff by blast
     show ?thesis
-      apply (rule_tac c = "abs B + 1" in that)
-      using norm_bound_Basis_le Basis_le_norm
-       apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
-      done
+    proof (rule_tac c = "abs B + 1" in that)
+      show "S \<subseteq> cbox (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One)"
+        using norm_bound_Basis_le Basis_le_norm
+        by (fastforce simp: mem_box dest!: B intro: order_trans)
+      show "box (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One) \<noteq> {}"
+        by (simp add: box_eq_empty(1))
+    qed
   qed
   obtain \<D> where "countable \<D>"
      and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
@@ -1728,10 +1708,7 @@
     obtain u v where "K = cbox u v"
       using \<open>K \<in> \<D>\<close> cbox by blast
     with that show ?thesis
-      apply (rule_tac x=u in exI)
-      apply (rule_tac x=v in exI)
-      apply (metis Int_iff interior_cbox cbox Ksub)
-      done
+      by (metis Int_iff interior_cbox cbox Ksub)
   qed
   then obtain uf vf zf
     where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
@@ -1771,8 +1748,7 @@
       have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
         by (rule prod_constant [symmetric])
       also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
-        apply (rule prod.cong [OF refl])
-        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
+        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem cong: prod.cong)
       finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
       have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
         using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
@@ -1788,11 +1764,9 @@
       have 0: "0 \<le> prj1 (vf X - uf X)"
         using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
       have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
-        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close>)
-        apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
+        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> \<open>0 < B\<close> flip: prj1_eq)
         using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
-        apply (fastforce simp add: box_ne_empty power_decreasing)
-        done
+        by (fastforce simp add: box_ne_empty power_decreasing)
       also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
         by (subst (3) ufvf[symmetric]) simp
       finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
@@ -1801,11 +1775,11 @@
       by (simp add: sum_distrib_left)
     also have "\<dots> \<le> e/2"
     proof -
-      have div: "\<D>' division_of \<Union>\<D>'"
-        apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
-        using cbox that apply blast
-        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
-        done
+      have "\<And>K. K \<in> \<D>' \<Longrightarrow> \<exists>a b. K = cbox a b"
+        using cbox that by blast
+      then have div: "\<D>' division_of \<Union>\<D>'"
+        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def
+        by (force simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
       have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
       proof (rule measure_mono_fmeasurable)
         show "(\<Union>\<D>') \<in> sets lebesgue"
@@ -1830,10 +1804,8 @@
                  (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
         using content_division [OF div] by auto
       also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
-        apply (rule mult_left_mono [OF le_meaT])
-        using \<open>0 < B\<close>
-        apply (simp add: algebra_simps)
-        done
+        using \<open>0 < B\<close> 
+        by (intro mult_left_mono [OF le_meaT]) (force simp add: algebra_simps)
       also have "\<dots> \<le> e/2"
         using T \<open>0 < B\<close> by (simp add: field_simps)
       finally show ?thesis .
@@ -1924,12 +1896,10 @@
       then show ?thesis
         using B order_trans that by blast
     qed
-    have "x \<in> ?S (nat (ceiling (max B (norm x))))"
-      apply (simp add: \<open>x \<in> S \<close>, rule)
-      using real_nat_ceiling_ge max.bounded_iff apply blast
-      using T no
-      apply (force simp: algebra_simps)
-      done
+    have "norm x \<le> real (nat \<lceil>max B (norm x)\<rceil>)"
+      by linarith
+    then have "x \<in> ?S (nat (ceiling (max B (norm x))))"
+      using T no by (force simp: \<open>x \<in> S\<close> algebra_simps)
     then show "x \<in> (\<Union>n. ?S n)" by force
   qed auto
   then show ?thesis
@@ -1946,9 +1916,9 @@
         if "x \<in> S" for x
   proof -
     obtain f' where "linear f'"
-      and f': "\<And>e. e>0 \<Longrightarrow>
-                  \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
-                              norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
+       and f': "\<And>e. e>0 \<Longrightarrow>
+                        \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
+                                    norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
       using diff_f \<open>x \<in> S\<close>
       by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
     obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
@@ -1957,24 +1927,21 @@
               and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
                           norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
       using f' [of 1] by (force simp:)
-    have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
-              if "y \<in> S" "norm (y - x) < d" for y
-    proof -
-      have "norm (f y - f x) -B *  norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
-        by (simp add: B)
-      also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
-        by (rule norm_triangle_ineq2)
-      also have "... \<le> norm (y - x)"
-        by (rule d [OF that])
-      finally show ?thesis
-        by (simp add: algebra_simps)
-    qed
     show ?thesis
-      apply (rule_tac x="ball x d" in exI)
-      apply (rule_tac x="B+1" in exI)
-      using \<open>d>0\<close>
-      apply (auto simp: dist_norm norm_minus_commute intro!: *)
-      done
+    proof (intro exI conjI ballI)
+      show "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
+        if "y \<in> S \<inter> ball x d" for y
+      proof -
+        have "norm (f y - f x) - B * norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
+          by (simp add: B)
+        also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
+          by (rule norm_triangle_ineq2)
+        also have "... \<le> norm (y - x)"
+          by (metis IntE d dist_norm mem_ball norm_minus_commute that)
+        finally show ?thesis
+          by (simp add: algebra_simps)
+      qed
+    qed (use \<open>d>0\<close> in auto)
   qed
   with negligible_locally_Lipschitz_image assms show ?thesis by metis
 qed
@@ -1990,25 +1957,28 @@
     where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
       and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
     using lowerdim_embeddings [OF MlessN] by metis
-  have "negligible {x. x\<bullet>j = 0}"
-    by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
-  then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
-    apply (rule negligible_subset)
-    by (simp add: image_subsetI j)
-  have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
+  have "negligible ((\<lambda>x. lift (x, 0)) ` S)"
+  proof -
+    have "negligible {x. x\<bullet>j = 0}"
+      by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
+    moreover have "(\<lambda>m. lift (m, 0)) ` S \<subseteq> {n. n \<bullet> j = 0}"
+      using j by force
+    ultimately show ?thesis
+      using negligible_subset by auto
+  qed
+  moreover
+  have "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
     using diff_f
     apply (clarsimp simp add: differentiable_on_def)
     apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
              linear_imp_differentiable [OF linear_fst])
     apply (force simp: image_comp o_def)
     done
-  have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
+  moreover
+  have "f = f \<circ> fst \<circ> drop \<circ> (\<lambda>x. lift (x, 0))"
     by (simp add: o_def)
-  then show ?thesis
-    apply (rule ssubst)
-    apply (subst image_comp [symmetric])
-    apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
-    done
+  ultimately show ?thesis
+    by (metis (no_types) image_comp negligible_differentiable_image_negligible order_refl)
 qed
 
 subsection\<open>Measurability of countable unions and intersections of various kinds.\<close>
@@ -2020,21 +1990,24 @@
   shows measurable_nested_Union: "(\<Union>n. S n) \<in> lmeasurable"
   and measure_nested_Union:  "(\<lambda>n. measure lebesgue (S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. S n)" (is ?Lim)
 proof -
-  have 1: "\<And>n. (indicat_real (S n)) integrable_on UNIV"
-    using S measurable_integrable by blast
-  have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
-    by (simp add: indicator_leI nest rev_subsetD)
-  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
-    apply (rule tendsto_eventually)
-    apply (simp add: indicator_def)
-    by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
-  have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
-    using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
-  have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
-    apply (simp add: lmeasure_integral_UNIV S cong: conj_cong)
-    apply (simp add: measurable_integrable)
-    apply (rule monotone_convergence_increasing [OF 1 2 3 4])
-    done
+  have "indicat_real (\<Union> (range S)) integrable_on UNIV \<and>
+    (\<lambda>n. integral UNIV (indicat_real (S n)))
+    \<longlonglongrightarrow> integral UNIV (indicat_real (\<Union> (range S)))"
+  proof (rule monotone_convergence_increasing)
+    show "\<And>n. (indicat_real (S n)) integrable_on UNIV"
+      using S measurable_integrable by blast
+    show "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
+      by (simp add: indicator_leI nest rev_subsetD)
+    have "\<And>x. (\<exists>n. x \<in> S n) \<longrightarrow> (\<forall>\<^sub>F n in sequentially. x \<in> S n)"
+      by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
+    then
+    show "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
+      by (simp add: indicator_def tendsto_eventually)
+    show "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
+      using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
+  qed
+  then have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
+    by (simp add: lmeasure_integral_UNIV S cong: conj_cong) (simp add: measurable_integrable)
   then show "(\<Union>n. S n) \<in> lmeasurable" "?Lim"
     by auto
 qed
@@ -2094,8 +2067,9 @@
       using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
       by (metis S finite_atMost subset_UNIV)
     also have "\<dots> \<le> measure lebesgue (cbox a b)"
-      apply (rule measure_mono_fmeasurable)
-      using ab S by force+
+    proof (rule measure_mono_fmeasurable)
+      show "\<Union> (S ` {..n}) \<in> sets lebesgue" using S by blast
+    qed (use ab in auto)
     finally show ?thesis .
   qed
   show "(\<Union>n. S n) \<in> lmeasurable"
@@ -2167,12 +2141,9 @@
     using negligible_subset by blast
 qed
 
-lemma locally_negligible:
-     "locally negligible S \<longleftrightarrow> negligible S"
+lemma locally_negligible: "locally negligible S \<longleftrightarrow> negligible S"
   unfolding locally_def
-  apply safe
-   apply (meson negligible_subset openin_subtopology_self locally_negligible_alt)
-  by (meson negligible_subset openin_imp_subset order_refl)
+  by (metis locally_negligible_alt negligible_subset openin_imp_subset openin_subtopology_self)
 
 
 subsection\<open>Integral bounds\<close>
@@ -2237,15 +2208,17 @@
 qed
 
 lemma absdiff_norm_less:
-  assumes "sum (\<lambda>x. norm (f x - g x)) s < e"
-    and "finite s"
-  shows "\<bar>sum (\<lambda>x. norm(f x)) s - sum (\<lambda>x. norm(g x)) s\<bar> < e"
-  unfolding sum_subtractf[symmetric]
-  apply (rule le_less_trans[OF sum_abs])
-  apply (rule le_less_trans[OF _ assms(1)])
-  apply (rule sum_mono)
-  apply (rule norm_triangle_ineq3)
-  done
+  assumes "sum (\<lambda>x. norm (f x - g x)) S < e"
+  shows "\<bar>sum (\<lambda>x. norm(f x)) S - sum (\<lambda>x. norm(g x)) S\<bar> < e" (is "?lhs < e")
+proof -
+  have "?lhs \<le> (\<Sum>i\<in>S. \<bar>norm (f i) - norm (g i)\<bar>)"
+    by (metis (no_types) sum_abs sum_subtractf)
+  also have "... \<le> (\<Sum>x\<in>S. norm (f x - g x))"
+    by (simp add: norm_triangle_ineq3 sum_mono)
+  also have "... < e"
+    using assms(1) by blast
+  finally show ?thesis .
+qed
 
 proposition bounded_variation_absolutely_integrable_interval:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
@@ -2344,17 +2317,6 @@
       next
         have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
           unfolding p'_def using d' by blast
-        have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
-        proof -
-          obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
-            using y unfolding p'(6)[symmetric] by auto
-          obtain i where i: "i \<in> d" "y \<in> i"
-            using y unfolding d'(6)[symmetric] by auto
-          have "x \<in> i"
-            using fineD[OF p(3) xl(1)] using k(2) i xl by auto
-          then show ?thesis
-            unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
-        qed
         show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
         proof
           show "\<Union>{k. \<exists>x. (x, k) \<in> p'} \<subseteq> cbox a b"
@@ -2370,17 +2332,24 @@
               using y unfolding d'(6)[symmetric] by auto
             have "x \<in> I"
               using fineD[OF p(3) xl(1)] using k(2) i xl by auto
-            then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
-              apply (rule_tac X="I \<inter> L" in UnionI)
-              using i xl by (auto simp: p'_def)
+            then show "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}"
+            proof -
+              obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
+                using y unfolding p'(6)[symmetric] by auto
+              obtain i where i: "i \<in> d" "y \<in> i"
+                using y unfolding d'(6)[symmetric] by auto
+              have "x \<in> i"
+                using fineD[OF p(3) xl(1)] using k(2) i xl by auto
+              then show ?thesis
+                unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+            qed
           qed
         qed
       qed
-
       then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
         using g(2) gp' tagged_division_of_def by blast
 
-      have "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
+      have in_p': "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
         for x I L y
       proof -
         have "x \<in> I"
@@ -2391,7 +2360,8 @@
           by (simp add: p'_def)
         with y show ?thesis by auto
       qed
-      moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+      moreover 
+      have Ex_p_p': "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
         if xK: "(x,K) \<in> p'" for x K
       proof -
         obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
@@ -2402,9 +2372,10 @@
       ultimately have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
         by auto
       have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
-        apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
-         apply (auto intro: integral_null simp: content_eq_0_interior)
-        done
+      proof (rule sum.over_tagged_division_lemma[OF p''])
+        show "\<And>u v. box u v = {} \<Longrightarrow> norm (integral (cbox u v) f) = 0"
+          by (auto intro: integral_null simp: content_eq_0_interior)
+      qed
       have snd_p_div: "snd ` p division_of cbox a b"
         by (rule division_of_tagged_division[OF p(1)])
       note snd_p = division_ofD[OF snd_p_div]
@@ -2432,28 +2403,30 @@
             define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
             have uvab: "cbox u v \<subseteq> cbox a b"
               using d(1) k uv by blast
-            have "d' division_of cbox u v"
+            have d'_div: "d' division_of cbox u v"
               unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
-            moreover then have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+            moreover have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
               by (simp add: sum_norm_le)
+            moreover have "f integrable_on K"
+              using f integrable_on_subcbox uv uvab by blast
+            moreover have "d' division_of K"
+              using d'_div uv by blast
             ultimately have "norm (integral K f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
-              apply (subst integral_combine_division_topdown[of _ _ d'])
-                apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab])
-              done
+              by (simp add: integral_combine_division_topdown)
             also have "\<dots> = (\<Sum>I\<in>{K \<inter> L |L. L \<in> snd ` p}. norm (integral I f))"
-            proof -
-              have *: "norm (integral I f) = 0"
-                if "I \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-                  "I \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for I
-                using that by auto
-              show ?thesis
-                apply (rule sum.mono_neutral_left)
-                  apply (simp add: snd_p(1))
-                unfolding d'_def uv using * by auto
+            proof (rule sum.mono_neutral_left)
+              show "finite {K \<inter> L |L. L \<in> snd ` p}"
+                by (simp add: snd_p(1))
+              show "\<forall>i\<in>{K \<inter> L |L. L \<in> snd ` p} - d'. norm (integral i f) = 0"
+                "d' \<subseteq> {K \<inter> L |L. L \<in> snd ` p}"
+                using d'_def image_eqI uv by auto
             qed
             also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
-            proof -
-              have *: "norm (integral (K \<inter> l) f) = 0"
+              unfolding Setcompr_eq_image
+            proof (rule sum.reindex_nontrivial [unfolded o_def])
+              show "finite (snd ` p)"
+                using snd_p(1) by blast
+              show "norm (integral (K \<inter> l) f) = 0"
                 if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "K \<inter> l = K \<inter> y" for l y
               proof -
                 have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
@@ -2468,12 +2441,6 @@
                   unfolding uv Int_interval content_eq_0_interior
                   by (metis (mono_tags, lifting) norm_eq_zero)
               qed
-              show ?thesis
-                unfolding Setcompr_eq_image
-                apply (rule sum.reindex_nontrivial [unfolded o_def])
-                 apply (rule finite_imageI)
-                 apply (rule p')
-                using * by auto
             qed
             finally show "norm (integral K f) \<le> (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))" .
           qed
@@ -2485,7 +2452,7 @@
           proof -
             have eq0: " (integral (l1 \<inter> k1) f) = 0"
               if "l1 \<inter> k1 = l2 \<inter> k2" "(l1, k1) \<noteq> (l2, k2)"
-                "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
+                 "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
               for l1 l2 k1 k2 j1 j2
             proof -
               obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
@@ -2508,26 +2475,14 @@
               by (metis eq0 fst_conv snd_conv)
           qed
           also have "\<dots> = (\<Sum>(x,k) \<in> p'. norm (integral k f))"
-          proof -
-            have 0: "integral (ia \<inter> snd (a, b)) f = 0"
-              if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for ia a b
-            proof -
-              have "ia \<inter> b = {}"
-                using that unfolding p'alt image_iff Bex_def not_ex
-                apply (erule_tac x="(a, ia \<inter> b)" in allE)
-                apply auto
-                done
-              then show ?thesis by auto
-            qed
-            have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
-              using that
-              apply (clarsimp simp: p'_def image_iff)
-              by (metis (no_types, hide_lams) snd_conv)
-            show ?thesis
-              unfolding sum_p'
-              apply (rule sum.mono_neutral_right)
-                apply (metis * finite_imageI[OF fin_d_sndp])
-              using 0 1 by auto
+            unfolding sum_p'
+          proof (rule sum.mono_neutral_right)
+            show "finite {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+              by (metis * finite_imageI[OF fin_d_sndp])
+            show "snd ` p' \<subseteq> {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+              by (clarsimp simp: p'_def) (metis image_eqI snd_conv)
+            show "\<forall>i\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p} - snd ` p'. norm (integral i f) = 0"
+              by clarsimp (metis Henstock_Kurzweil_Integration.integral_empty disjoint_iff image_eqI in_p' snd_conv)
           qed
           finally show ?thesis .
         qed
@@ -2540,11 +2495,10 @@
             using finite_cartesian_product[OF p'(1) d'(1)] by metis
           have "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> ?S. \<bar>content k\<bar> * norm (f x))"
             unfolding norm_scaleR
-            apply (rule sum.mono_neutral_left)
-              apply (subst *)
-              apply (rule finite_imageI [OF fin_pd])
-            unfolding p'alt apply auto
-            by fastforce
+          proof (rule sum.mono_neutral_left)
+            show "finite {(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+              by (simp add: "*" fin_pd)
+          qed (use p'alt in \<open>force+\<close>)
           also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
           proof -
             have "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
@@ -2557,8 +2511,7 @@
               have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
                 using that by auto
               then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-                apply (rule disjE)
-                using that p'(5) d'(5) by auto
+                using that p'(5) d'(5) by (metis snd_conv)
               moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
                 unfolding that ..
               ultimately have "interior (l1 \<inter> k1) = {}"
@@ -2570,8 +2523,7 @@
               unfolding *
               apply (subst sum.reindex_nontrivial [OF fin_pd])
               unfolding split_paired_all o_def split_def prod.inject
-               apply force+
-              done
+              by force+
           qed
           also have "\<dots> = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
           proof -
@@ -2601,20 +2553,17 @@
                 qed
                 then show ?thesis
                   unfolding Setcompr_eq_image
-                  apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
-                  by auto
+                  by (fastforce intro: sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
               qed
               also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
-                apply (rule sum.mono_neutral_right)
-                unfolding Setcompr_eq_image
-                  apply (rule finite_imageI [OF \<open>finite d\<close>])
-                 apply (fastforce simp: inf.commute)+
-                done
-              finally show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
-                unfolding sum_distrib_right[symmetric] real_scaleR_def
-                apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
-                using xl(2)[unfolded uv] unfolding uv apply auto
-                done
+              proof (rule sum.mono_neutral_right)
+                show "finite {k \<inter> cbox u v |k. k \<in> d}"
+                  by (simp add: d'(1))
+              qed (fastforce simp: inf.commute)+
+              finally have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = content (cbox u v)"
+                using additive_content_division[OF division_inter_1[OF d(1)]] uv xl(2) by auto
+              then show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"              
+                unfolding sum_distrib_right[symmetric] using uv by auto
             qed
             show ?thesis
               by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
@@ -2636,66 +2585,55 @@
     and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> sum (\<lambda>k. norm (integral k f)) d \<le> B"
   shows "f absolutely_integrable_on UNIV"
 proof (rule absolutely_integrable_onI, fact)
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
+  let ?f = "\<lambda>D. \<Sum>k\<in>D. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
+  define SDF where "SDF \<equiv> SUP d\<in>?D. ?f d"
   have D_1: "?D \<noteq> {}"
     by (rule elementary_interval) auto
   have D_2: "bdd_above (?f`?D)"
-    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
-  note D = D_1 D_2
-  let ?S = "SUP d\<in>?D. ?f d"
-  have "\<And>a b. f integrable_on cbox a b"
-    using assms(1) integrable_on_subcbox by blast
-  then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
-    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
-    using assms(2) apply blast
-    done
-  have "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
-    apply (subst has_integral_alt')
-    apply safe
-  proof goal_cases
-    case (1 a b)
-    show ?case
-      using f_int[of a b] unfolding absolutely_integrable_on_def by auto
-  next
-    case prems: (2 e)
-    have "\<exists>y\<in>sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
+    using assms(2) by auto
+  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
+    using assms integrable_on_subcbox 
+    by (blast intro!: bounded_variation_absolutely_integrable_interval)
+  have "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
+                    \<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
+    if "0 < e" for e
+  proof -
+    have "\<exists>y \<in> ?f ` ?D. \<not> y \<le> SDF - e"
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      then have "?S \<le> ?S - e"
-        by (intro cSUP_least[OF D(1)]) auto
+      then have "SDF \<le> SDF - e"
+        unfolding SDF_def
+        by (metis (mono_tags) D_1 cSUP_least image_eqI)
       then show False
-        using prems by auto
+        using that by auto
     qed
-    then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
-      "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
+    then obtain d K where ddiv: "d division_of \<Union>d" and "K = ?f d" "SDF - e < K"
       by (auto simp add: image_iff not_le)
-    then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
-                  < (\<Sum>k\<in>d. norm (integral k f))"
+    then have d: "SDF - e < ?f d"
       by auto
     note d'=division_ofD[OF ddiv]
     have "bounded (\<Union>d)"
-      by (rule elementary_bounded,fact)
-    from this[unfolded bounded_pos] obtain K where
-       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
-    show ?case
+      using ddiv by blast
+    then obtain K where K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K"
+      using bounded_pos by blast
+    show ?thesis
     proof (intro conjI impI allI exI)
       fix a b :: 'n
       assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
-      have *: "\<And>s s1. \<lbrakk>?S - e < s1; s1 \<le> s; s < ?S + e\<rbrakk> \<Longrightarrow> \<bar>s - ?S\<bar> < e"
+      have *: "\<And>s s1. \<lbrakk>SDF - e < s1; s1 \<le> s; s < SDF + e\<rbrakk> \<Longrightarrow> \<bar>s - SDF\<bar> < e"
         by arith
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
+      show "\<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
         unfolding real_norm_def
       proof (rule * [OF d])
-        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
+        have "?f d \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
         proof (intro sum_mono)
           fix k assume "k \<in> d"
           with d'(4) f_int show "norm (integral k f) \<le> integral k (\<lambda>x. norm (f x))"
             by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
         qed
         also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
-          apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
-          using absolutely_integrable_on_def d'(4) f_int by blast
-        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
+          by (metis (full_types) absolutely_integrable_on_def d'(4) ddiv f_int integral_combine_division_bottomup)
+        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. norm (f x))"
         proof -
           have "\<Union>d \<subseteq> cbox a b"
             using K(2) ab by fastforce
@@ -2703,8 +2641,7 @@
             using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
             by (auto intro!: integral_subset_le)
         qed
-        finally show "(\<Sum>k\<in>d. norm (integral k f))
-                      \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" .
+        finally show "?f d \<le> integral (cbox a b) (\<lambda>x. norm (f x))" .
       next
         have "e/2>0"
           using \<open>e > 0\<close> by auto
@@ -2723,31 +2660,39 @@
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
           by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
             (auto simp add: fine_Int)
-        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;
-                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> SDF; \<bar>sf - si\<bar> < e/2;
+                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < SDF + e"
           by arith
-        have "integral (cbox a b) (\<lambda>x. norm (f x)) < ?S + e"
+        have "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
         proof (rule *)
           show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
             unfolding split_def
-            apply (rule absdiff_norm_less)
-            using d2[of p] p(1,3) apply (auto simp: tagged_division_of_def split_def)
-            done
+          proof (rule absdiff_norm_less)
+            show "(\<Sum>p\<in>p. norm (content (snd p) *\<^sub>R f (fst p) - integral (snd p) f)) < e/2"
+              using d2[of p] p(1,3) by (auto simp: tagged_division_of_def split_def)
+          qed
           show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
             using d1[OF p(1,2)] by (simp only: real_norm_def)
           show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
             by (auto simp: split_paired_all sum.cong [OF refl])
-          show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
+          have "(\<Sum>(x,k) \<in> p. norm (integral k f)) = (\<Sum>k\<in>snd ` p. norm (integral k f))"
+            apply (rule sum.over_tagged_division_lemma[OF p(1)])
+            by (metis Henstock_Kurzweil_Integration.integral_empty integral_open_interval norm_zero)
+          also have "... \<le> SDF"
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
-            apply (subst sum.over_tagged_division_lemma[OF p(1)])
-            apply (auto simp: content_eq_0_interior tagged_partial_division_of_def intro!: cSUP_upper2 D)
-            done
+            by (auto simp: SDF_def tagged_partial_division_of_def intro!: cSUP_upper2 D_1 D_2)
+          finally show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> SDF" .
         qed
-        then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+        then show "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
           by simp
       qed
-    qed (insert K, auto)
+    qed (use K in auto)
   qed
+  moreover have "\<And>a b. (\<lambda>x. norm (f x)) integrable_on cbox a b"
+    using absolutely_integrable_on_def f_int by auto
+  ultimately
+  have "((\<lambda>x. norm (f x)) has_integral SDF) UNIV"
+    by (auto simp: has_integral_alt')
   then show "(\<lambda>x. norm (f x)) integrable_on UNIV"
     by blast
 qed
@@ -2844,10 +2789,13 @@
       have "?\<mu> (\<Union>\<F>) \<le> ?\<mu> S + e"
       proof (rule *)
         have "(\<Sum>K\<in>\<F>. ?\<mu> (K \<inter> S)) = ?\<mu> (\<Union>C\<in>\<F>. C \<inter> S)"
-          apply (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
-          using \<F>div \<open>S \<in> lmeasurable\<close> apply blast
-          unfolding pairwise_def
-          by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+        proof (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
+          show "\<And>K. K \<in> \<F> \<Longrightarrow> K \<inter> S \<in> lmeasurable"
+            using \<F>div \<open>S \<in> lmeasurable\<close> by blast
+          show "pairwise (\<lambda>K y. negligible (K \<inter> S \<inter> (y \<inter> S))) \<F>"
+            unfolding pairwise_def
+            by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+        qed
         also have "\<dots> = ?\<mu> (\<Union>\<F> \<inter> S)"
           by simp
         also have "\<dots> \<le> ?\<mu> S"
@@ -3007,8 +2955,7 @@
               by (metis True empty_imp_negligible image_Int image_empty interior_Int interior_injective_linear_image that(1))
           qed
           moreover have "g ` K \<inter> g ` L \<subseteq> frontier (g ` K \<inter> g ` L) \<union> interior (g ` K \<inter> g ` L)"
-            apply (auto simp: frontier_def)
-            using closure_subset contra_subsetD by fastforce+
+            by (metis Diff_partition Int_commute calculation closure_Un_frontier frontier_def inf.absorb_iff2 inf_bot_right inf_sup_absorb negligible_Un_eq open_interior open_not_negligible sup_commute)
           ultimately show ?thesis
             by (rule negligible_subset)
         next
@@ -3090,8 +3037,6 @@
             and DD: "cbox a b - S \<subseteq> \<Union>\<D>" "\<Union>\<D> \<in> lmeasurable"
             and le: "?\<mu> (\<Union>\<D>) \<le> ?\<mu> (cbox a b - S) + e/(1 + \<bar>m\<bar>)"
           by (rule measurable_outer_intervals_bounded [of "cbox a b - S" a b "e/(1 + \<bar>m\<bar>)"]; use 1 2 pairwise_def in force)
-        have meq: "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
-          by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
         show "\<exists>T \<in> lmeasurable. T \<subseteq> f ` S \<and> m * ?\<mu> S - e \<le> ?\<mu> T"
         proof (intro bexI conjI)
           show "f ` (cbox a b) - f ` (\<Union>\<D>) \<subseteq> f ` S"
@@ -3099,16 +3044,24 @@
           have "m * ?\<mu> S - e \<le> m * (?\<mu> S - e / (1 + \<bar>m\<bar>))"
             using \<open>m \<ge> 0\<close> \<open>e > 0\<close> by (simp add: field_simps)
           also have "\<dots> \<le> ?\<mu> (f ` cbox a b) - ?\<mu> (f ` (\<Union>\<D>))"
-            using le \<open>m \<ge> 0\<close> \<open>e > 0\<close>
-            apply (simp add: im fUD [OF \<open>countable \<D>\<close> cbox intdisj] right_diff_distrib [symmetric])
-            apply (rule mult_left_mono; simp add: algebra_simps meq)
-            done
+          proof -
+            have "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
+              by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
+            then have "(?\<mu> S - e / (1 + m)) \<le> (content (cbox a b) - ?\<mu> (\<Union> \<D>))"
+              using \<open>m \<ge> 0\<close> le by auto
+            then show ?thesis
+              using \<open>m \<ge> 0\<close> \<open>e > 0\<close>
+              by (simp add: mult_left_mono im fUD [OF \<open>countable \<D>\<close> cbox intdisj] flip: right_diff_distrib)
+          qed
           also have "\<dots> = ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)"
-            apply (rule measurable_measure_Diff [symmetric])
-            apply (simp add: assms(1) measurable_linear_image_interval)
-            apply (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
-             apply (simp add: Sup_le_iff cbox image_mono)
-            done
+          proof (rule measurable_measure_Diff [symmetric])
+            show "f ` cbox a b \<in> lmeasurable"
+              by (simp add: assms(1) measurable_linear_image_interval)
+            show "f ` \<Union> \<D> \<in> sets lebesgue"
+              by (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
+            show "f ` \<Union> \<D> \<subseteq> f ` cbox a b"
+              by (simp add: Sup_le_iff cbox image_mono)
+          qed
           finally show "m * ?\<mu> S - e \<le> ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)" .
           show "f ` cbox a b - f ` \<Union>\<D> \<in> lmeasurable"
             by (simp add: fUD \<open>countable \<D>\<close> \<open>linear f\<close> cbox fmeasurable.Diff intdisj measurable_linear_image_interval)
@@ -3166,7 +3119,7 @@
         moreover have fim: "f ` (S \<inter> h ` (cbox a b)) = (f ` S) \<inter> cbox a b"
           by (auto simp: hf rev_image_eqI fh)
         ultimately have 1: "(f ` S) \<inter> cbox a b \<in> lmeasurable"
-              and 2: "m * ?\<mu> (S \<inter> h ` cbox a b) = ?\<mu> ((f ` S) \<inter> cbox a b)"
+              and 2: "?\<mu> ((f ` S) \<inter> cbox a b) = m * ?\<mu> (S \<inter> h ` cbox a b)"
           using fBS [of "S \<inter> (h ` (cbox a b))"] by auto
         have *: "\<lbrakk>\<bar>z - m\<bar> < e; z \<le> w; w \<le> m\<rbrakk> \<Longrightarrow> \<bar>w - m\<bar> \<le> e"
           for w z m and e::real by auto
@@ -3192,20 +3145,12 @@
           show "?\<mu> (S \<inter> h ` cbox a b) \<le> ?\<mu> S"
             by (simp add: S Shab fmeasurableD measure_mono_fmeasurable)
         qed
-        have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> m * e / (1 + \<bar>m\<bar>)"
-        proof -
-          have mm: "\<bar>m\<bar> = m"
-            by (simp add: \<open>0 \<le> m\<close>)
-          then have "\<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m \<le> e / (1 + m) * m"
-            by (metis (no_types) \<open>0 \<le> m\<close> meas_adiff abs_minus_commute mult_right_mono)
-          moreover have "\<forall>r. \<bar>r * m\<bar> = m * \<bar>r\<bar>"
-            by (metis \<open>0 \<le> m\<close> abs_mult_pos mult.commute)
-          ultimately show ?thesis
-            apply (simp add: 2 [symmetric])
-            by (metis (no_types) abs_minus_commute mult.commute right_diff_distrib' mm)
-        qed
+        have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> \<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m"
+          by (metis "2" \<open>m \<ge> 0\<close> abs_minus_commute abs_mult_pos mult.commute order_refl right_diff_distrib')
+        also have "\<dots> \<le> e / (1 + m) * m"
+          by (metis \<open>m \<ge> 0\<close> abs_minus_commute abs_of_nonneg meas_adiff mult.commute mult_left_mono)
         also have "\<dots> < e"
-          using \<open>e > 0\<close> by (cases "m \<ge> 0") (simp_all add: field_simps)
+          using \<open>e > 0\<close> \<open>m \<ge> 0\<close> by (simp add: field_simps)
         finally have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> < e" .
         with 1 show ?thesis by auto
       qed
@@ -3293,23 +3238,21 @@
 proposition absolutely_integrable_componentwise_iff:
   shows "f absolutely_integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A)"
 proof -
-  have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)"
-          if "f integrable_on A"
-  proof -
-    have 1: "\<And>i. \<lbrakk>(\<lambda>x. norm (f x)) integrable_on A; i \<in> Basis\<rbrakk>
-                 \<Longrightarrow> (\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
-      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. norm(f x)"])
-      using Basis_le_norm integrable_component that apply fastforce+
-      done
-    have 2: "\<forall>i\<in>Basis. (\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on A \<Longrightarrow> f absolutely_integrable_on A"
-      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)"])
-      using norm_le_l1 that apply (force intro: integrable_sum)+
-      done
-    show ?thesis
-      apply auto
-       apply (metis (full_types) absolutely_integrable_on_def set_integrable_abs 1)
-      apply (metis (full_types) absolutely_integrable_on_def 2)
-      done
+  have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)" (is "?lhs = ?rhs")
+    if "f integrable_on A"
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (metis absolutely_integrable_on_def Topology_Euclidean_Space.norm_nth_le absolutely_integrable_integrable_bound integrable_component that)
+  next
+    assume R: ?rhs
+    have "f absolutely_integrable_on A"
+    proof (rule absolutely_integrable_integrable_bound)
+      show "(\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)) integrable_on A"
+        using R by (force intro: integrable_sum)
+    qed (use that norm_le_l1 in auto)
+    then show ?lhs
+      using absolutely_integrable_on_def by auto
   qed
   show ?thesis
     unfolding absolutely_integrable_on_def
@@ -3331,8 +3274,7 @@
   shows "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S"
 proof -
   have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
-    apply (rule absolutely_integrable_linear [OF assms])
-    by (simp add: bounded_linear_scaleR_right)
+    by (simp add: absolutely_integrable_linear assms bounded_linear_scaleR_right)
   then show ?thesis
     using assms by blast
 qed
@@ -3354,10 +3296,6 @@
   shows "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) absolutely_integrable_on S"
         (is "?g absolutely_integrable_on S")
 proof -
-  have eq: "?g =
-        (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
-               (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
-    by (simp)
   have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
            (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
            absolutely_integrable_on S"
@@ -3367,19 +3305,20 @@
       by (simp add: linear_linear algebra_simps linearI)
     moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
                    absolutely_integrable_on S"
+      using assms \<open>i \<in> Basis\<close>
       unfolding o_def
-      apply (rule absolutely_integrable_norm [unfolded o_def])
-      using assms \<open>i \<in> Basis\<close>
-      apply (auto simp: algebra_simps dest: absolutely_integrable_component[where b=i])
-      done
+      by (intro absolutely_integrable_norm [unfolded o_def])
+         (auto simp: algebra_simps dest: absolutely_integrable_component)
     ultimately show ?thesis
       by (subst comp_assoc) (blast intro: absolutely_integrable_linear)
   qed
+  have eq: "?g =
+        (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
+               (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
+    by (simp)
   show ?thesis
-    apply (rule ssubst [OF eq])
-    apply (rule absolutely_integrable_sum)
-     apply (force simp: intro!: *)+
-    done
+    unfolding eq
+    by (rule absolutely_integrable_sum) (force simp: intro!: *)+
 qed
 
 lemma abs_absolutely_integrableI_1:
@@ -3447,10 +3386,8 @@
   qed
   moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
-    apply (intro set_integral_add absolutely_integrable_scaleR_left assms)
     using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
-    apply (simp add: algebra_simps)
-    done
+    by (intro set_integral_add absolutely_integrable_scaleR_left assms) (simp add: algebra_simps)
   ultimately show ?thesis by metis
 qed
 
@@ -3482,10 +3419,9 @@
   qed
   moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
-    apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
     using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
-    apply (simp add: algebra_simps)
-    done
+    by (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
+       (simp add: algebra_simps)
   ultimately show ?thesis by metis
 qed
 
@@ -3522,9 +3458,10 @@
   shows "f absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
-    apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
-    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
-    by (simp add: comp inner_diff_left)
+  proof (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
+    show "(\<lambda>x. g x - f x) integrable_on A"
+      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+  qed (simp add: comp inner_diff_left)
   then show ?thesis
     by simp
 qed
@@ -3536,9 +3473,10 @@
   shows "g absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
-    apply (rule set_integral_add [OF f nonnegative_absolutely_integrable])
-    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
-    by (simp add: comp inner_diff_left)
+  proof (rule set_integral_add [OF f nonnegative_absolutely_integrable])
+    show "(\<lambda>x. g x - f x) integrable_on A"
+      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+  qed (simp add: comp inner_diff_left)
   then show ?thesis
     by simp
 qed
@@ -3613,9 +3551,10 @@
     apply (subst has_integral_alt)
     apply (subst (asm) has_integral_alt)
     apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
-    apply (metis vector_one_nth)
-    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
-    apply (blast intro!: *)
+    subgoal by (metis vector_one_nth)
+    subgoal
+      apply (erule all_forward imp_forward ex_forward asm_rl)+
+      by (blast intro!: *)+
     done
 qed
 
@@ -3653,10 +3592,12 @@
       and B: "ball 0 B \<subseteq> cbox a b" for e B and a b::"real^1"
   proof -
     have B': "ball 0 B \<subseteq> {a$1..b$1}"
-      using B
-      apply (simp add: subset_iff Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
-      apply (metis (full_types) norm_real vec_component)
-      done
+    proof (clarsimp)
+      fix t
+      assume "\<bar>t\<bar> < B" then show "a $ 1 \<le> t \<and> t \<le> b $ 1"
+        using subsetD [OF B]
+        by (metis (mono_tags, hide_lams) mem_ball_0 mem_box_cart(2) norm_real vec_component)
+    qed
     have eq: "(\<lambda>x. if vec x \<in> S then f (vec x) else 0) = (\<lambda>x. if x \<in> S then f x else 0) \<circ> vec"
       by force
     have [simp]: "(\<exists>y\<in>S. x = y $ 1) \<longleftrightarrow> vec x \<in> S" for x
@@ -3670,11 +3611,10 @@
     apply (subst (asm) has_integral_alt)
     apply (simp add: has_integral_vec1_D_cbox eq_cbox split: if_split_asm, blast)
     apply (intro conjI impI)
-     apply (metis vector_one_nth)
+    subgoal by (metis vector_one_nth)
     apply (erule thin_rl)
-    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
-    using * apply blast
-    done
+    apply (erule all_forward ex_forward conj_forward)+
+      by (blast intro!: *)+
 qed
 
 
@@ -3988,11 +3928,8 @@
     by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
   also have "\<dots> = T - F a"
   proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
-      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
-      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
-      apply (rule filterlim_real_sequentially)
-      done
+     have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
+       by (auto intro: filterlim_compose[OF lim filterlim_tendsto_add_at_top] filterlim_real_sequentially)
     then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
       by (simp add: F_mono F_le_T tendsto_diff)
   qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
@@ -4028,17 +3965,22 @@
   shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
             =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
 proof-
-  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
-    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
-      (auto intro!: DERIV_isCont)
-
-  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
-    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
-    apply (subst Bochner_Integration.integral_add[symmetric])
-    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
-    by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
-
-  thus ?thesis using 0 by auto
+  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) 
+      = LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x"
+    by (meson vector_space_over_itself.scale_left_distrib)
+  also have "... = (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+  proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+      using DERIV_isCont by blast+
+  qed
+  finally have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+                (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" .
+  moreover have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
+  proof (intro integral_FTC_Icc_real derivative_eq_intros cont_f cont_g continuous_intros)
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+      using DERIV_isCont by blast+
+  qed auto
+  ultimately show ?thesis by auto
 qed
 
 lemma integral_by_parts':
@@ -4737,10 +4679,8 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes "S \<in> sets lebesgue"
   shows "f absolutely_integrable_on S \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S) \<and> (\<lambda>x. \<bar>f x\<bar>) integrable_on S"
-  using assms
-  apply (auto simp: absolutely_integrable_measurable integrable_on_lebesgue_on)
-  apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
-  using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
+  by (metis abs_absolutely_integrableI_1 absolutely_integrable_measurable_real assms 
+            measurable_bounded_by_integrable_imp_integrable order_refl real_norm_def set_integrable_abs set_lebesgue_integral_eq_integral(1))
 
 lemma absolutely_integrable_imp_borel_measurable:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -4782,8 +4722,8 @@
       have "\<exists>T' B. open T' \<and> f x \<in> T' \<and>
                    (\<forall>y\<in>f ` V \<inter> T \<inter> T'. norm (g y - g (f x)) \<le> B * norm (y - f x))"
         if "f x \<in> T" "x \<in> V" for x
-        apply (rule_tac x = "ball (f x) 1" in exI)
-        using that noxy by (force simp: g)
+        using that noxy 
+        by (rule_tac x = "ball (f x) 1" in exI) (force simp: g)
       then have "negligible (g ` (f ` V \<inter> T))"
         by (force simp: \<open>negligible T\<close> negligible_Int intro!: negligible_locally_Lipschitz_image)
       moreover have "V \<subseteq> g ` (f ` V \<inter> T)"
@@ -4826,12 +4766,12 @@
       using less by linarith
     with \<delta> \<open>y \<in> S\<close> have le: "norm (f y - f x - f' x (y - x)) \<le> B * norm (y - x) - norm (y - x)/i"
       by (auto simp: algebra_simps)
-    have *: "\<lbrakk>norm(f - f' - y) \<le> b - c; b \<le> norm y; d \<le> c\<rbrakk> \<Longrightarrow> d \<le> norm(f - f')"
-      for b c d and y f f'::'a
-      using norm_triangle_ineq3 [of "f - f'" y] by simp
-    show ?thesis
-      apply (rule * [OF le B])
+    have "norm (y - x) / real (max i j) \<le> norm (y - x) / real i"
       using \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> by (simp add: field_split_simps max_mult_distrib_left of_nat_max less_max_iff_disj)
+    also have "... \<le> norm (f y - f x)"
+      using B [of "y-x"] le norm_triangle_ineq3 [of "f y - f x" "f' x (y - x)"]
+      by linarith 
+    finally show ?thesis .
   qed
   with \<open>x \<in> S\<close> \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> show "\<exists>n\<in>{0<..}. x \<in> U n"
     by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj)
@@ -5069,11 +5009,11 @@
       qed
     finally show ?thesis .
     qed
-    then show "\<exists>d>0. \<forall>y\<in>f ` S.
+    with \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close> 
+    show "\<exists>d>0. \<forall>y\<in>f ` S.
                norm (y - f a) < d \<longrightarrow>
                norm (g y - g (f a) - g' (y - f a)) \<le> e * norm (y - f a)"
-      apply (rule_tac x="min k (d / B)" in exI)
-      using \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close> by (auto simp: gf)
+      by (rule_tac x="min k (d / B)" in exI) (auto simp: gf)
   qed
 qed