# HG changeset patch
# User paulson
# Date 1756568221 -3600
# Node ID cb5fc74454b067b7502e3772f39446495a757797
# Parent  aad65db60c80b9d5d604adaa2767286f7a3a2284# Parent  d39e4284805a71bf65fc268a712198277f362fa6
merged

diff -r aad65db60c80 -r cb5fc74454b0 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 29 16:51:55 2025 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 30 16:37:01 2025 +0100
@@ -13,7 +13,7 @@
 
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   \<Longrightarrow> norm(y-x) \<le> e"
-  by (smt (verit, ccfv_SIG) norm_diff_triangle_ineq)
+  by (simp add: add_diff_add norm_add_rule_thm)
 
 lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   by auto
@@ -28,7 +28,7 @@
   by blast
 (* END MOVE *)
 
-subsection \<open>Content (length, area, volume...) of an interval\<close>
+subsection \<open>Content (length, area, volume, etc.) of an interval\<close>
 
 abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
   where "content s \<equiv> measure lborel s"
@@ -92,7 +92,7 @@
   unfolding content_eq_0 interior_cbox box_eq_empty by auto
 
 lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
-  by (auto simp add: content_cbox_cases less_le prod_nonneg)
+  by (auto simp: content_cbox_cases less_le prod_nonneg)
 
 lemma content_empty [simp]: "content {} = 0"
   by simp
@@ -109,8 +109,8 @@
 
 lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
   unfolding measure_lborel_cbox_eq Basis_prod_def
-  apply (subst prod.union_disjoint)
-  apply (auto simp: bex_Un ball_Un)
+  using Basis_zero 
+  apply (simp add: prod.union_disjoint disjoint_iff image_iff ball_Un prod.reindex_nontrivial)
   apply (subst (1 2) prod.reindex_nontrivial)
   apply auto
   done
@@ -176,24 +176,22 @@
     by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove)
   have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
     x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
-    by  (auto simp add: field_simps)
+    by  (auto simp: field_simps)
   moreover
-  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
+  have 3: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
       (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
     "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
       (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
-    by (auto intro!: prod.cong)
+    by (simp_all cong: prod.cong)
   have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
     unfolding not_le using True assms by auto
   ultimately show ?thesis
-    using assms unfolding simps ** 1[of "\<lambda>i x. b\<bullet>i - x"] 1[of "\<lambda>i x. x - a\<bullet>i"] 2
+    using assms unfolding simps 1[of "\<lambda>i x. b\<bullet>i - x"] 1[of "\<lambda>i x. x - a\<bullet>i"] 2 3
     by auto
 next
   case False
-  then have "cbox a b = {}"
-    unfolding box_eq_empty by (auto simp: not_le)
   then show ?thesis
-    by (auto simp: not_le)
+    using box_ne_empty(1) by force
 qed
 
 lemma division_of_content_0:
@@ -224,7 +222,7 @@
   rewrites "comm_monoid_set.F plus 0 = sum"
 proof -
   interpret operative plus 0 content
-    by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
+    by standard (auto simp: content_split [symmetric] content_eq_0_interior)
   show "operative plus 0 content"
     by standard
   show "comm_monoid_set.F plus 0 = sum"
@@ -248,7 +246,7 @@
     using partial_division_extend_interval by metis
   then have "sum content \<D> \<le> sum content \<D>'"
     using sum_mono2 by blast
-  also have "... \<le> content(cbox a b)"
+  also have "\<dots> \<le> content(cbox a b)"
     by (simp add: \<open>\<D>' division_of cbox a b\<close> additive_content_division less_eq_real_def)
   finally show ?thesis .
 qed
@@ -281,7 +279,7 @@
 
 lemma has_integral_cbox:
   "(f has_integral I) (cbox a b) \<longleftrightarrow> ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter (cbox a b))"
-  by (auto simp add: has_integral_def)
+  by (auto simp: has_integral_def)
 
 lemma has_integral:
   "(f has_integral y) (cbox a b) \<longleftrightarrow>
@@ -312,7 +310,7 @@
      then (f has_integral y) i
      else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
       (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
-  by (subst has_integral_def) (auto simp add: has_integral_cbox)
+  by (subst has_integral_def) (auto simp: has_integral_cbox)
 
 lemma has_integral_altD:
   assumes "(f has_integral y) i"
@@ -382,7 +380,7 @@
     using has_integral_unique_cbox[OF w(1) z(1)] by auto
   then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
     using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
-    by (auto simp add: norm_minus_commute)
+    by (auto simp: norm_minus_commute)
   also have "\<dots> < norm (k1 - k2)/2 + norm (k1 - k2)/2"
     by (metis add_strict_mono z(2) w(2))
   finally show False by auto
@@ -444,10 +442,10 @@
 next
   case False
   have *: "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. 0)"
-    by (auto simp add: assms)
+    by (auto simp: assms)
   show ?thesis
     using has_integral_is_0_cbox False
-    by (subst has_integral_alt) (force simp add: *)
+    by (subst has_integral_alt) (force simp: *)
 qed
 
 lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) S"
@@ -556,7 +554,7 @@
 next
   case False then have "\<not> (\<lambda>x. f x * c) integrable_on S"
     using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ S "inverse c"]
-    by (auto simp add: mult.assoc)
+    by (auto simp: mult.assoc)
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 
@@ -862,7 +860,7 @@
   by (metis box_real(2) has_integral_null)
 
 lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
-  by (auto simp add: has_integral_null dest!: integral_unique)
+  by (auto simp: has_integral_null dest!: integral_unique)
 
 lemma integral_null [simp]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
   by (metis has_integral_null integral_unique)
@@ -874,7 +872,7 @@
   by (meson ex_in_conv has_integral_is_0)
 
 lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
-  by (auto simp add: has_integral_empty has_integral_unique)
+  by (auto simp: has_integral_empty has_integral_unique)
 
 lemma integrable_on_empty[intro]: "f integrable_on {}"
   unfolding integrable_on_def by auto
@@ -905,24 +903,26 @@
 lemma integral_blinfun_apply:
   assumes "f integrable_on s"
   shows "integral s (\<lambda>x. blinfun_apply h (f x)) = blinfun_apply h (integral s f)"
-  by (subst integral_linear[symmetric, OF assms blinfun.bounded_linear_right]) (simp add: o_def)
+  using integral_linear[OF assms blinfun.bounded_linear_right]
+  by (metis (no_types, lifting) ext comp_def)
 
 lemma blinfun_apply_integral:
   assumes "f integrable_on s"
   shows "blinfun_apply (integral s f) x = integral s (\<lambda>y. blinfun_apply (f y) x)"
-  by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)
+  by (metis (no_types, lifting) ext assms blinfun.prod_left.rep_eq
+      integral_blinfun_apply)
 
 lemma has_integral_componentwise_iff:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   shows "(f has_integral y) A \<longleftrightarrow> (\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
-proof safe
+proof (intro iffI strip)
   fix b :: 'b assume "(f has_integral y) A"
   from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
     show "((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A" by (simp add: o_def)
 next
   assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
   hence "\<forall>b\<in>Basis. (((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f x \<bullet> b)) has_integral ((y \<bullet> b) *\<^sub>R b)) A"
-    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
+    using bounded_linear_scaleR_left has_integral_linear by blast
   hence "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. (y \<bullet> b) *\<^sub>R b)) A"
     by (intro has_integral_sum) (simp_all add: o_def)
   thus "(f has_integral y) A" by (simp add: euclidean_representation)
@@ -938,9 +938,8 @@
   shows "f integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
 proof
   assume "f integrable_on A"
-  then obtain y where "(f has_integral y) A" by (auto simp: integrable_on_def)
-  hence "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
-    by (subst (asm) has_integral_componentwise_iff)
+  then obtain y where "\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A"
+    using has_integral_componentwise_iff by blast
   thus "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)" by (auto simp: integrable_on_def)
 next
   assume "(\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) integrable_on A)"
@@ -964,8 +963,8 @@
   shows "integral A f = (\<Sum>b\<in>Basis. integral A (\<lambda>x. (f x \<bullet> b) *\<^sub>R b))"
 proof -
   from assms have integrable: "\<forall>b\<in>Basis. (\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. (f x \<bullet> b)) integrable_on A"
-    by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI)
-       (simp_all add: bounded_linear_scaleR_left)
+    using bounded_linear_scaleR_left integrable_componentwise_iff integrable_linear
+    by blast
   have "integral A f = integral A (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b)"
     by (simp add: euclidean_representation)
   also from integrable have "\<dots> = (\<Sum>a\<in>Basis. integral A (\<lambda>x. (f x \<bullet> a) *\<^sub>R a))"
@@ -1000,12 +999,11 @@
   proof -
     have "e/2 > 0" using that by auto
     with y obtain \<gamma> where "gauge \<gamma>"
-      and \<gamma>: "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<Longrightarrow>
+      and "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<Longrightarrow>
                   norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - y) < e/2"
       by meson
-    show ?thesis
-    apply (rule_tac x=\<gamma> in exI, clarsimp simp: \<open>gauge \<gamma>\<close>)
-        by (blast intro!: \<gamma> dist_triangle_half_l[where y=y,unfolded dist_norm])
+    then show ?thesis
+      by (metis norm_triangle_half_l)
     qed
 next
   assume "\<forall>e>0. \<exists>\<gamma>. ?P e \<gamma>"
@@ -1038,9 +1036,10 @@
     proof (intro exI allI impI)
       fix m n
       assume mn: "N \<le> m" "N \<le> n"
-      have "norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < 1 / (real N + 1)"
+      have "norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) 
+                - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < 1 / (real N + 1)"
         by (simp add: p(1) dp mn \<gamma>)
-      also have "... < e"
+      also have "\<dots> < e"
         using  N \<open>N \<noteq> 0\<close> \<open>0 < e\<close> by (auto simp: field_simps)
       finally show "norm ((\<Sum>(x,K) \<in> p m. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x)) < e" .
     qed
@@ -1066,10 +1065,11 @@
       show "norm ((\<Sum>(x,K) \<in> q. content K *\<^sub>R f x) - y) < e"
            if "q tagged_division_of cbox a b \<and> \<gamma> (N1+N2) fine q" for q
       proof (rule norm_triangle_half_r)
-        have "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> q. content K *\<^sub>R f x))
+        have "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x)
+                  - (\<Sum>(x,K) \<in> q. content K *\<^sub>R f x))
                < 1 / (real (N1+N2) + 1)"
           by (rule \<gamma>; simp add: dp p that)
-        also have "... < e/2"
+        also have "\<dots> < e/2"
           using N1 \<open>0 < e\<close> by (auto simp: field_simps intro: less_le_trans)
         finally show "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> q. content K *\<^sub>R f x)) < e/2" .
         show "norm ((\<Sum>(x,K) \<in> p (N1+N2). content K *\<^sub>R f x) - y) < e/2"
@@ -1126,9 +1126,7 @@
       and \<gamma>1norm:
         "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine \<D>\<rbrakk>
              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - i) < e/2"
-       apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
-       apply (simp add: interval_split[symmetric] k)
-      done
+      by (metis (no_types, lifting) ext e fi has_integral interval_split(1) k)
     obtain \<gamma>2 where \<gamma>2: "gauge \<gamma>2"
       and \<gamma>2norm:
         "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine \<D>\<rbrakk>
@@ -1156,9 +1154,9 @@
         by blast
       then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
         using Basis_le_norm[OF k, of "x - y"]
-        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
+        by (auto simp: dist_norm inner_diff_left intro: le_less_trans)
       with y show False
-        using ** by (auto simp add: field_simps)
+        using ** by (auto simp: field_simps)
     qed
     have xk_ge_c: "x\<bullet>k \<ge> c" if as: "(x,K) \<in> p" and K: "K \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}" for x K
     proof (rule ccontr)
@@ -1169,9 +1167,9 @@
         by blast
       then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
         using Basis_le_norm[OF k, of "x - y"]
-        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
+        by (auto simp: dist_norm inner_diff_left intro: le_less_trans)
       with y show False
-        using ** by (auto simp add: field_simps)
+        using ** by (auto simp: field_simps)
     qed
     have fin_finite: "finite {(x,f K) | x K. (x,K) \<in> s \<and> P x K}"
       if "finite s" for s and f :: "'a set \<Rightarrow> 'a set" and P :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
@@ -1185,7 +1183,7 @@
       fix i :: "'a \<times> 'a set"
       assume "i \<in> (\<lambda>(x, k). (x, \<G> k)) ` p - {(x, \<G> k) |x k. (x, k) \<in> p \<and> \<G> k \<noteq> {}}"
       then obtain x K where xk: "i = (x, \<G> K)"  "(x,K) \<in> p"
-                                 "(x, \<G> K) \<notin> {(x, \<G> K) |x K. (x,K) \<in> p \<and> \<G> K \<noteq> {}}"
+                                "(x, \<G> K) \<notin> {(x, \<G> K) |x K. (x,K) \<in> p \<and> \<G> K \<noteq> {}}"
         by auto
       have "content (\<G> K) = 0"
         using xk using content_empty by auto
@@ -1214,7 +1212,7 @@
       show "x \<in> L" "L \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
         using p xk_le_c xL' by auto
       show "\<exists>a b. L = cbox a b"
-        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])
+        using ab' interval_split(1) k xL'(2) by blast
 
       fix y R
       assume yR: "(y, R) \<in> ?M1"
@@ -1260,7 +1258,7 @@
       show "x \<in> L" "L \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
         using p xk_ge_c xL' by auto
       show "\<exists>a b. L = cbox a b"
-        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])
+        using p xL' ab' by (auto simp: interval_split[OF k,where c=c])
 
       fix y R
       assume yR: "(y, R) \<in> ?M2"
@@ -1372,10 +1370,7 @@
           using x interior_subset by fastforce
         have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon>/2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
               (\<Sum>i\<in>Basis. (if i = k then \<epsilon>/2 else 0))"
-        proof (rule sum.cong [OF refl])
-          show "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon>/2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
-            using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_not_same_Basis)
-        qed
+          using \<open>0 < \<epsilon>\<close> k by (intro sum.cong) (auto simp: inner_not_same_Basis)
         also have "\<dots> < \<epsilon>"
           by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
         finally have "x + (\<epsilon>/2) *\<^sub>R k \<in> ball x \<epsilon>"
@@ -1439,7 +1434,7 @@
         then show ?thesis
           using as norm_triangle_half_l[OF d[of p1 p] d[of p2 p]]
           unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
-          by (auto simp add: algebra_simps)
+          by (auto simp: algebra_simps)
       qed
     qed
   qed
@@ -1471,7 +1466,7 @@
         then show ?thesis
           using as norm_triangle_half_l[OF d[of p p1] d[of p p2]]
           unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
-          by (auto simp add: algebra_simps)
+          by (auto simp: algebra_simps)
       qed
     qed
   qed
@@ -1485,8 +1480,7 @@
     (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
 proof -
   interpret comm_monoid "lift_option plus" "Some (0::'b)"
-    by (rule comm_monoid_lift_option)
-      (rule add.comm_monoid_axioms)
+    by (simp add: add.comm_monoid_axioms comm_monoid_lift_option)
   show ?thesis
   proof
     fix a b c
@@ -1505,23 +1499,14 @@
       proof (rule ccontr)
         assume "\<not> ?thesis"
         then have "f integrable_on cbox a b"
-          unfolding integrable_on_def
-          apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
-          apply (auto intro: has_integral_split[OF _ _ k])
-          done
+          unfolding integrable_on_def using has_integral_split k by blast
         then show False
           using False by auto
       qed
       then show ?thesis
         using False by auto
     qed
-  next
-    fix a b :: 'a
-    assume "box a b = {}"
-    then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
-      using has_integral_null_eq
-      by (auto simp: integrable_on_null content_eq_0_interior)
-  qed
+  qed (auto simp: content_eq_0_interior)
 qed
 
 subsection \<open>Bounds on the norm of Riemann sums and the integral itself\<close>
@@ -1529,25 +1514,14 @@
 lemma dsum_bound:
   assumes p: "p division_of (cbox a b)"
     and "norm c \<le> e"
-  shows "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)"
-proof -
-  have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = sum content p"
-    by simp
-  have e: "0 \<le> e"
-    using assms(2) norm_ge_zero order_trans by blast
-  have "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
-    using norm_sum by blast
-  also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
-    by (simp add: sum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono sum_nonneg)
-  also have "... \<le> e * content (cbox a b)"
-    by (metis additive_content_division p eq_iff sumeq)
-  finally show ?thesis .
-qed
+  shows "norm (\<Sum>l\<in>p. content l *\<^sub>R c) \<le> e * content(cbox a b)"
+  by (metis abs_of_nonneg assms measure_nonneg mult.commute mult_right_mono norm_scaleR
+      scaleR_left.sum sum_content.division)
 
 lemma rsum_bound:
   assumes p: "p tagged_division_of (cbox a b)"
       and "\<forall>x\<in>cbox a b. norm (f x) \<le> e"
-    shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> e * content (cbox a b)"
+    shows "norm (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) \<le> e * content (cbox a b)"
 proof (cases "cbox a b = {}")
   case True show ?thesis
     using p unfolding True tagged_division_of_trivial by auto
@@ -1563,7 +1537,7 @@
     by force
   have "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))"
     by (rule norm_sum)
-  also have "...  \<le> e * content (cbox a b)"
+  also have "\<dots>  \<le> e * content (cbox a b)"
   proof -
     have "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e"
       using assms(2) p tag_in_interval by force
@@ -1625,14 +1599,12 @@
   assumes p: "p tagged_division_of (cbox a b)"
       and "\<And>x. x \<in> cbox a b \<Longrightarrow> (f x)\<bullet>i \<le> (g x)\<bullet>i"
     shows "(\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) \<bullet> i \<le> (\<Sum>(x, K)\<in>p. content K *\<^sub>R g x) \<bullet> i"
-unfolding inner_sum_left
-proof (rule sum_mono, clarify)
-  fix x K
-  assume ab: "(x, K) \<in> p"
-  with p obtain u v where K: "K = cbox u v"
-    by blast
-  then show "(content K *\<^sub>R f x) \<bullet> i \<le> (content K *\<^sub>R g x) \<bullet> i"
-    by (metis ab assms inner_scaleR_left measure_nonneg mult_left_mono tag_in_interval)
+proof -
+have "\<And>a b. (a, b) \<in> p \<Longrightarrow> content b *\<^sub>R f a \<bullet> i \<le> content b *\<^sub>R g a \<bullet> i"
+  by (metis assms(2) inner_commute inner_scaleR_right mult_left_mono
+      measure_nonneg p tag_in_interval)
+  then show ?thesis
+    by (simp add: inner_sum_left split_def sum_mono)
 qed
 
 lemma has_integral_component_le:
@@ -1643,9 +1615,8 @@
   shows "i\<bullet>k \<le> j\<bullet>k"
 proof -
   have ik_le_jk: "i\<bullet>k \<le> j\<bullet>k"
-    if f_i: "(f has_integral i) (cbox a b)"
-    and g_j: "(g has_integral j) (cbox a b)"
-    and le: "\<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k"
+    if f_i: "(f has_integral i) (cbox a b)" and g_j: "(g has_integral j) (cbox a b)"
+    and le: "\<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k" 
     for a b i and j :: 'b and f g :: "'a \<Rightarrow> 'b"
   proof (rule ccontr)
     assume "\<not> ?thesis"
@@ -1654,13 +1625,14 @@
     obtain \<gamma>1 where "gauge \<gamma>1" 
       and \<gamma>1: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma>1 fine p\<rbrakk>
                 \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < (i \<bullet> k - j \<bullet> k) / 3"
-      using f_i[unfolded has_integral,rule_format,OF *] by fastforce 
+      by (metis "*" f_i has_integral)
     obtain \<gamma>2 where "gauge \<gamma>2" 
       and \<gamma>2: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma>2 fine p\<rbrakk>
                 \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) < (i \<bullet> k - j \<bullet> k) / 3"
-      using g_j[unfolded has_integral,rule_format,OF *] by fastforce 
+      by (metis "*" g_j has_integral)
     obtain p where p: "p tagged_division_of cbox a b" and "\<gamma>1 fine p" "\<gamma>2 fine p"
-       using fine_division_exists[OF gauge_Int[OF \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close>], of a b] unfolding fine_Int
+      using fine_division_exists[OF gauge_Int[OF \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close>]] 
+      unfolding fine_Int
        by metis
     then have "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
          "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
@@ -1668,7 +1640,7 @@
     then show False
       unfolding inner_simps
       using rsum_component_le[OF p] le
-      by (fastforce simp add: abs_real_def split: if_split_asm)
+      by (fastforce simp: abs_real_def split: if_split_asm)
   qed
   show ?thesis
   proof (cases "\<exists>a b. S = cbox a b")
@@ -1737,7 +1709,8 @@
   assumes "k \<in> Basis"
     and  "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> (f x)\<bullet>k"
   shows "0 \<le> (integral S f)\<bullet>k"
-  by (smt (verit, ccfv_threshold) assms eq_integralD euclidean_all_zero_iff has_integral_component_nonneg)
+  by (metis assms order.refl has_integral_component_nonneg has_integral_integral
+      inner_zero_left not_integrable_integral)
 
 lemma has_integral_component_neg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1754,7 +1727,7 @@
     and "k \<in> Basis"
   shows "B * content (cbox a b) \<le> i\<bullet>k"
   using has_integral_component_le[OF assms(3) has_integral_const assms(1),of "(\<Sum>i\<in>Basis. B *\<^sub>R i)::'b"] assms(2-)
-  by (auto simp add: field_simps)
+  by (auto simp: field_simps)
 
 lemma has_integral_component_ubound:
   fixes f::"'a::euclidean_space => 'b::euclidean_space"
@@ -1763,7 +1736,7 @@
     and "k \<in> Basis"
   shows "i\<bullet>k \<le> B * content (cbox a b)"
   using has_integral_component_le[OF assms(3,1) has_integral_const, of "\<Sum>i\<in>Basis. B *\<^sub>R i"] assms(2-)
-  by (auto simp add: field_simps)
+  by (auto simp: field_simps)
 
 lemma integral_component_lbound:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1870,7 +1843,7 @@
       qed
       have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g n x) - (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g m x)) \<le> 2 / real M * content (cbox a b)"
         by (blast intro: norm_le rsum_diff_bound[OF \<D>(1), where e="2 / real M"])
-      also have "... \<le> e/2"
+      also have "\<dots> \<le> e/2"
         using M True
         by (auto simp: field_simps)
       finally have le_e2: "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g n x) - (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g m x)) \<le> e/2" .
@@ -1966,7 +1939,7 @@
   proof (intro tendsto_cong eventually_at_rightI)
     fix d :: real assume d: "d \<in> {0<..<1}"
     have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
-      using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
+      using * d k by (auto simp: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
     moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
       using * d k by (auto simp: a'_def b'_def)
     ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
@@ -2061,7 +2034,7 @@
     have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
     proof -
       have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
-        by (force simp add: indicator_def intro!: sum_mono)
+        by (force simp: indicator_def intro!: sum_mono)
       also have "\<dots> < e"
       proof (subst sum.over_tagged_division_lemma[OF p(1)])
         fix u v::'a
@@ -2169,7 +2142,7 @@
         by (rule sum_le_included[of \<D> T g snd f]; force)
       have "norm (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) \<le> (\<Sum>(x,K) \<in> \<D>. norm (content K *\<^sub>R f x))"
         unfolding split_def by (rule norm_sum)
-      also have "... \<le> (\<Sum>(i, j) \<in> Sigma {..N + 1} q.
+      also have "\<dots> \<le> (\<Sum>(i, j) \<in> Sigma {..N + 1} q.
                           (real i + 1) * (case j of (x, K) \<Rightarrow> content K *\<^sub>R indicator S x))"
       proof (rule sum_le_inc, safe)
         show "finite (Sigma {..N+1} q)"
@@ -2184,12 +2157,8 @@
           unfolding n_def by auto
         then have "n \<in> {0..N + 1}"
           using N[OF *] by auto
-        moreover have "K \<subseteq> \<gamma> (nat \<lfloor>norm (f x)\<rfloor>) x"
-          using that(2) xk by auto
-        moreover then have "(x, K) \<in> q (nat \<lfloor>norm (f x)\<rfloor>)"
-          by (simp add: q(3) xk)
-        moreover then have "(x, K) \<in> q n"
-          using n_def by blast
+        moreover have "(x, K) \<in> q n"
+          using n_def q(3) that(2) xk by fastforce
         moreover
         have "norm (content K *\<^sub>R f x) \<le> (real n + 1) * (content K * indicator S x)"
         proof (cases "x \<in> S")
@@ -2208,27 +2177,27 @@
           (real y + 1) * (content K *\<^sub>R indicator S x)"
           by force
       qed auto
-      also have "... = (\<Sum>i\<le>N + 1. \<Sum>j\<in>q i. (real i + 1) * (case j of (x, K) \<Rightarrow> content K *\<^sub>R indicator S x))"
+      also have "\<dots> = (\<Sum>i\<le>N + 1. \<Sum>j\<in>q i. (real i + 1) * (case j of (x, K) \<Rightarrow> content K *\<^sub>R indicator S x))"
         using q(1) by (intro sum_Sigma_product [symmetric]) auto
-      also have "... \<le> (\<Sum>i\<le>N + 1. (real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar>)"
-        by (rule sum_mono) (simp add: sum_distrib_left [symmetric])
-      also have "... \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
+      also have "\<dots> \<le> (\<Sum>i\<le>N + 1. (real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar>)"
+        by (rule sum_mono) (simp flip: sum_distrib_left)
+      also have "\<dots> \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
       proof (rule sum_mono)
         show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2/2 ^ i"
           if "i \<in> {..N + 1}" for i
           using \<gamma>[of "q i" i] q by (simp add: divide_simps mult.left_commute)
       qed
-      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1/2) ^ i)"
+      also have "\<dots> = e/2 * (\<Sum>i\<le>N + 1. (1/2) ^ i)"
         unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
       also have "\<dots> < e/2 * 2"
       proof (rule mult_strict_left_mono)
         have "sum (power (1/2)) {..N + 1} = sum (power (1/2::real)) {..<N + 2}"
           using lessThan_Suc_atMost by auto
-        also have "... < 2"
+        also have "\<dots> < 2"
           by (auto simp: geometric_sum)
         finally show "sum (power (1/2::real)) {..N + 1} < 2" .
       qed (use \<open>0 < e\<close> in auto)
-      finally  show ?thesis by auto
+      finally show ?thesis by simp
     qed
   qed
 qed
@@ -2302,8 +2271,7 @@
   using assms unfolding integrable_on_def by (blast intro: has_integral_spike)
 
 lemma integral_spike:
-  assumes "negligible S"
-    and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+  assumes "negligible S" and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
   shows "integral T f = integral T g"
   using has_integral_spike_eq[OF assms]
     by (auto simp: integral_def integrable_on_def)
@@ -2312,19 +2280,19 @@
 subsection \<open>Some other trivialities about negligible sets\<close>
 
 lemma negligible_subset:
-  assumes "negligible s" "t \<subseteq> s"
-  shows "negligible t"
+  assumes "negligible S" "T \<subseteq> S"
+  shows "negligible T"
   unfolding negligible_def
     by (metis (no_types) Diff_iff assms contra_subsetD has_integral_negligible indicator_simps(2))
 
 lemma negligible_diff[intro?]:
-  assumes "negligible s"
-  shows "negligible (s - t)"
+  assumes "negligible S"
+  shows "negligible (S - T)"
   using assms by (meson Diff_subset negligible_subset)
 
 lemma negligible_Int:
-  assumes "negligible s \<or> negligible t"
-  shows "negligible (s \<inter> t)"
+  assumes "negligible S \<or> negligible T"
+  shows "negligible (S \<inter> T)"
   using assms negligible_subset by force
 
 lemma negligible_Un:
@@ -2344,13 +2312,13 @@
     unfolding negligible_def by blast
 qed
 
-lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
+lemma negligible_Un_eq[simp]: "negligible (S \<union> T) \<longleftrightarrow> negligible S \<and> negligible T"
   using negligible_Un negligible_subset by blast
 
 lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
   using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
 
-lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
+lemma negligible_insert[simp]: "negligible (insert a S) \<longleftrightarrow> negligible S"
   by (metis insert_is_Un negligible_Un_eq negligible_sing)
 
 lemma negligible_empty[iff]: "negligible {}"
@@ -2361,23 +2329,18 @@
   by simp
 
 lemma negligible_finite[intro]:
-  assumes "finite s"
-  shows "negligible s"
-  using assms by (induct s) auto
+  assumes "finite S"
+  shows "negligible S"
+  using assms by (induct S) auto
 
 lemma negligible_Union[intro]:
   assumes "finite \<T>"
-    and "\<And>t. t \<in> \<T> \<Longrightarrow> negligible t"
+    and "\<And>T. T \<in> \<T> \<Longrightarrow> negligible T"
   shows "negligible(\<Union>\<T>)"
   using assms by induct auto
 
 lemma negligible: "negligible S \<longleftrightarrow> (\<forall>T. (indicat_real S has_integral 0) T)"
-proof (intro iffI allI)
-  fix T
-  assume "negligible S"
-  then show "(indicator S has_integral 0) T"
-    by (meson Diff_iff has_integral_negligible indicator_simps(2))
-qed (simp add: negligible_def)
+  by (meson DiffD2 has_integral_negligible indicator_simps(2) negligible_def)
 
 subsection \<open>Finite case of the spike theorem is quite commonly needed\<close>
 
@@ -2435,13 +2398,13 @@
 
 subsection \<open>In particular, the boundary of an interval is negligible\<close>
 
-lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
+lemma negligible_frontier_interval: "negligible(cbox a b - box a b)"
 proof -
   let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
   have "negligible ?A"
-    by (force simp add: negligible_Union[OF finite_imageI])
+    by (force simp: negligible_Union[OF finite_imageI])
   moreover have "cbox a b - box a b \<subseteq> ?A"
-    by (force simp add: mem_box)
+    by (force simp: mem_box)
   ultimately show ?thesis
     by (rule negligible_subset)
 qed
@@ -2544,7 +2507,7 @@
   obtain p where ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x d) fine p"
     using fine_division_exists[OF gauge_ball[OF \<open>0 < d\<close>], of a b] .
   have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
-  proof (safe, unfold snd_conv)
+  proof clarsimp 
     fix x l
     assume as: "(x, l) \<in> p"
     obtain a b where l: "l = cbox a b"
@@ -2606,10 +2569,10 @@
                    d fine p \<longrightarrow>
                    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<le> e * content (cbox a b))"
     using that [of 1]
-    by (force simp add: True sum_content_null[OF True] intro: fine_division_exists[of _ a b])
+    by (force simp: True sum_content_null[OF True] intro: fine_division_exists[of _ a b])
   ultimately show ?thesis
     unfolding has_integral_null_eq[OF True]
-    by (force simp add: )
+    by force
 next
   case False
   then have F: "0 < content (cbox a b)"
@@ -2625,7 +2588,7 @@
       by (meson F e less_imp_le mult_pos_pos)
     show "?P e (<)" if \<section>[rule_format]:  "\<forall>\<epsilon>>0. ?P (\<epsilon> * content (cbox a b)) (\<le>)"
       using \<section> [of "e/2 / content (cbox a b)"]
-        using F e by (force simp add: algebra_simps)
+        using F e by (force simp: algebra_simps)
   qed
 qed
 
@@ -2689,8 +2652,8 @@
       have "u \<in> K" "v \<in> K"
         by (simp_all add: \<open>u \<le> v\<close> k)
       have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) = norm (f u - f x - (u - x) *\<^sub>R f' x - (f v - f x - (v - x) *\<^sub>R f' x))"
-        by (auto simp add: algebra_simps)
-      also have "... \<le> norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
+        by (auto simp: algebra_simps)
+      also have "\<dots> \<le> norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
         by (rule norm_triangle_ineq4)
       finally have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
         norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" .
@@ -2699,12 +2662,12 @@
         show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
         proof (rule d)
           show "norm (u - x) < d x"
-            using \<open>u \<in> K\<close> ball by (auto simp add: dist_real_def)
+            using \<open>u \<in> K\<close> ball by (auto simp: dist_real_def)
         qed (use \<open>x \<in> K\<close> \<open>u \<in> K\<close> kab in auto)
         show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
         proof (rule d)
           show "norm (v - x) < d x"
-            using \<open>v \<in> K\<close> ball by (auto simp add: dist_real_def)
+            using \<open>v \<in> K\<close> ball by (auto simp: dist_real_def)
         qed (use \<open>x \<in> K\<close> \<open>v \<in> K\<close> kab in auto)
       qed
       also have "\<dots> \<le> e * (Sup K - Inf K)"
@@ -2781,7 +2744,6 @@
   by (meson DERIV_exp assms fundamental_theorem_of_calculus has_real_derivative_iff_has_vector_derivative
        has_vector_derivative_at_within integral_unique)
 
-
 lemma has_integral_sin_nx: "((\<lambda>x. sin(real_of_int n * x)) has_integral 0) {-pi..pi}"
 proof (cases "n = 0")
   case False
@@ -2839,10 +2801,7 @@
   from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
   note [derivative_intros] =
     has_derivative_subset[OF _ subset]
-    has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
-  note [continuous_intros] =
-    continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
-    continuous_on_subset[OF _ subset]
+    has_derivative_in_compose[where f="(\<lambda>u. x + u *\<^sub>R y)" and g = f]
   have "\<And>t. t \<in> {0..1} \<Longrightarrow>
     ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
     (at t within {0..1})"
@@ -2850,9 +2809,9 @@
     by (auto simp: has_vector_derivative_def
         linear_cmul[OF has_derivative_linear[OF f'], symmetric]
       intro!: derivative_eq_intros)
-  from fundamental_theorem_of_calculus[rule_format, OF _ this]
+  from fundamental_theorem_of_calculus[OF _ this]
   show ?thesis
-    by (auto intro!: integral_unique[symmetric])
+    by (simp add: integral_unique)
 qed
 
 lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
@@ -2916,7 +2875,7 @@
     "Dg n s = (if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0)" for n s
   have g0: "Dg 0 = g"
     using \<open>p > 0\<close>
-    by (auto simp add: Dg_def field_split_simps g_def split: if_split_asm)
+    by (auto simp: Dg_def field_split_simps g_def split: if_split_asm)
   have fact_eq: "real (p - Suc m) * fact (p - Suc (Suc m)) = fact (p - Suc m)" 
     if "p > Suc m" for m
     by (metis Suc_diff_Suc fact_Suc that)
@@ -2931,10 +2890,9 @@
     (?sum has_vector_derivative
       g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})"
     by auto
-  from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
+  from fundamental_theorem_of_calculus[OF \<open>a \<le> b\<close> deriv]
   have "(i has_integral ?sum b - ?sum a) {a..b}"
-    using atLeastatMost_empty'[simp del]
-    by (simp add: i_def g_def Dg_def)
+    using Dg_def g_def i_def by fastforce
   also
   have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)" "{..<p} \<inter> {i. p = Suc i} = {p - 1}" for p'
     using \<open>p > 0\<close> by (auto simp: power_mult_distrib)
@@ -2949,11 +2907,12 @@
       by (metis Suc_diff_Suc \<open>p>0\<close> diff_Suc_less diff_diff_cancel less_or_eq_imp_le)
     then show "{..<p} = (\<lambda>x. p - x - 1) ` {..<p}"
       by force
-  qed (auto simp add: inj_on_def Dg_def one)
+  qed (auto simp: inj_on_def Dg_def one)
   finally show c: ?case .
-  case 2 show ?case using c integral_unique
-    by (metis (lifting) add.commute diff_eq_eq integral_unique)
-  case 3 show ?case using c by force
+  case 2 show ?case
+    by (metis (lifting) add_diff_cancel_left' add_diff_eq c integral_unique) 
+  case 3 show ?case 
+    using c by force
 qed
 
 
@@ -2968,81 +2927,78 @@
 proof (induction "card \<D>" arbitrary: \<D> rule: less_induct)
   case less
   note \<D> = division_ofD[OF less.prems]
-  {
-    presume *: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D> \<Longrightarrow> ?case"
-    then show ?case
-      using less.prems by fastforce
-  }
-  assume noteq: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D>"
-  then obtain K c d where "K \<in> \<D>" and contk: "content K = 0" and keq: "K = cbox c d"
-    using \<D>(4) by blast 
-  then have "card \<D> > 0"
-    unfolding card_gt_0_iff using less by auto
-  then have card: "card (\<D> - {K}) < card \<D>"
-    using less \<open>K \<in> \<D>\<close> by (simp add: \<D>(1))
-  have closed: "closed (\<Union>(\<D> - {K}))"
-    using less.prems by auto
-  have "x islimpt \<Union>(\<D> - {K})" if "x \<in> K" for x 
-    unfolding islimpt_approachable
-  proof (intro allI impI)
-    fix e::real
-    assume "e > 0"
-    obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
-      using contk \<D>(3) [OF \<open>K \<in> \<D>\<close>] unfolding box_ne_empty keq
-      by (meson content_eq_0 dual_order.antisym)
-    then have xi: "x\<bullet>i = d\<bullet>i"
-      using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
-    define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i)/2 then c\<bullet>i +
+  show ?case
+  proof (cases "{k \<in> \<D>. content k \<noteq> 0} = \<D>")
+    case False
+    then obtain K c d where "K \<in> \<D>" and contk: "content K = 0" and keq: "K = cbox c d"
+      using \<D>(4) by blast 
+    then have "card \<D> > 0"
+      unfolding card_gt_0_iff using less by auto
+    then have card: "card (\<D> - {K}) < card \<D>"
+      using less \<open>K \<in> \<D>\<close> by (simp add: \<D>(1))
+    have closed: "closed (\<Union>(\<D> - {K}))"
+      using less.prems by auto
+    have "x islimpt \<Union>(\<D> - {K})" if "x \<in> K" for x 
+      unfolding islimpt_approachable
+    proof (intro allI impI)
+      fix e::real
+      assume "e > 0"
+      obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
+        using contk \<D>(3) [OF \<open>K \<in> \<D>\<close>] unfolding box_ne_empty keq
+        by (meson content_eq_0 dual_order.antisym)
+      then have xi: "x\<bullet>i = d\<bullet>i"
+        using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
+      define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i)/2 then c\<bullet>i +
       min e (b\<bullet>i - c\<bullet>i)/2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i)/2 else x\<bullet>j) *\<^sub>R j)"
-    show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
-    proof (intro bexI conjI)
-      have "d \<in> cbox c d"
-        using \<D>(3)[OF \<open>K \<in> \<D>\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
-      then have "d \<in> cbox a b"
-        using \<D>(2)[OF \<open>K \<in> \<D>\<close>] by (auto simp: keq)
-      then have di: "a \<bullet> i \<le> d \<bullet> i \<and> d \<bullet> i \<le> b \<bullet> i"
-        using \<open>i \<in> Basis\<close> mem_box(2) by blast
-      then have xyi: "y\<bullet>i \<noteq> x\<bullet>i"
-        unfolding y_def i xi using \<open>e > 0\<close> cont0 \<open>i \<in> Basis\<close>
-        by (auto simp: content_eq_0 elim!: ballE[of _ _ i])
-      then show "y \<noteq> x"
-        unfolding euclidean_eq_iff[where 'a='a] using i by auto
-      have "norm (y-x) \<le> (\<Sum>b\<in>Basis. \<bar>(y - x) \<bullet> b\<bar>)"
-        by (rule norm_le_l1)
-      also have "... = \<bar>(y - x) \<bullet> i\<bar> + (\<Sum>b \<in> Basis - {i}. \<bar>(y - x) \<bullet> b\<bar>)"
-        by (meson finite_Basis i(2) sum.remove)
-      also have "... <  e + sum (\<lambda>i. 0) Basis"
-      proof (rule add_less_le_mono)
-        show "\<bar>(y-x) \<bullet> i\<bar> < e"
-          using di \<open>e > 0\<close> y_def i xi by (auto simp: inner_simps)
-        show "(\<Sum>i\<in>Basis - {i}. \<bar>(y-x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
-          unfolding y_def by (auto simp: inner_simps)
-      qed 
-      finally have "norm (y-x) < e + sum (\<lambda>i. 0) Basis" .
-      then show "dist y x < e"
-        unfolding dist_norm by auto
-      have "y \<notin> K"
-        unfolding keq mem_box using i(1) i(2) xi xyi by fastforce
-      moreover have "y \<in> \<Union>\<D>"
-        using subsetD[OF \<D>(2)[OF \<open>K \<in> \<D>\<close>] \<open>x \<in> K\<close>] \<open>e > 0\<close> di i
-        by (auto simp: \<D> mem_box y_def field_simps elim!: ballE[of _ _ i])
-      ultimately show "y \<in> \<Union>(\<D> - {K})" by auto
+      show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
+      proof (intro bexI conjI)
+        have "d \<in> cbox c d"
+          using \<D>(3)[OF \<open>K \<in> \<D>\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
+        then have "d \<in> cbox a b"
+          using \<D>(2)[OF \<open>K \<in> \<D>\<close>] by (auto simp: keq)
+        then have di: "a \<bullet> i \<le> d \<bullet> i \<and> d \<bullet> i \<le> b \<bullet> i"
+          using \<open>i \<in> Basis\<close> mem_box(2) by blast
+        then have xyi: "y\<bullet>i \<noteq> x\<bullet>i"
+          unfolding y_def i xi using \<open>e > 0\<close> cont0 \<open>i \<in> Basis\<close>
+          by (auto simp: content_eq_0 elim!: ballE[of _ _ i])
+        then show "y \<noteq> x"
+          unfolding euclidean_eq_iff[where 'a='a] using i by auto
+        have "norm (y-x) \<le> (\<Sum>b\<in>Basis. \<bar>(y - x) \<bullet> b\<bar>)"
+          by (rule norm_le_l1)
+        also have "\<dots> = \<bar>(y - x) \<bullet> i\<bar> + (\<Sum>b \<in> Basis - {i}. \<bar>(y - x) \<bullet> b\<bar>)"
+          by (meson finite_Basis i(2) sum.remove)
+        also have "\<dots> <  e + sum (\<lambda>i. 0) Basis"
+        proof (rule add_less_le_mono)
+          show "\<bar>(y-x) \<bullet> i\<bar> < e"
+            using di \<open>e > 0\<close> y_def i xi by (auto simp: inner_simps)
+          show "(\<Sum>i\<in>Basis - {i}. \<bar>(y-x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
+            unfolding y_def by (auto simp: inner_simps)
+        qed 
+        finally have "norm (y-x) < e + sum (\<lambda>i. 0) Basis" .
+        then show "dist y x < e"
+          unfolding dist_norm by auto
+        have "y \<notin> K"
+          unfolding keq mem_box using i(1) i(2) xi xyi by fastforce
+        moreover have "y \<in> \<Union>\<D>"
+          using subsetD[OF \<D>(2)[OF \<open>K \<in> \<D>\<close>] \<open>x \<in> K\<close>] \<open>e > 0\<close> di i
+          by (auto simp: \<D> mem_box y_def field_simps elim!: ballE[of _ _ i])
+        ultimately show "y \<in> \<Union>(\<D> - {K})" by auto
+      qed
     qed
-  qed
-  then have "K \<subseteq> \<Union>(\<D> - {K})"
-    using closed closed_limpt by blast
-  then have "\<Union>(\<D> - {K}) = cbox a b"
-    unfolding \<D>(6)[symmetric] by auto
-  then have "\<D> - {K} division_of cbox a b"
-    by (metis Diff_subset less.prems division_of_subset \<D>(6))
-  then have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} division_of (cbox a b)"
-    using card less.hyps by blast
-  moreover have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} = {K \<in> \<D>. content K \<noteq> 0}"
-    using contk by auto
-  ultimately show ?case by auto
+    then have "K \<subseteq> \<Union>(\<D> - {K})"
+      using closed closed_limpt by blast
+    then have "\<Union>(\<D> - {K}) = cbox a b"
+      unfolding \<D>(6)[symmetric] by auto
+    then have "\<D> - {K} division_of cbox a b"
+      by (metis Diff_subset less.prems division_of_subset \<D>(6))
+    then have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} division_of (cbox a b)"
+      using card less.hyps by blast
+    moreover have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} = {K \<in> \<D>. content K \<noteq> 0}"
+      using contk by auto
+    ultimately show ?thesis by auto
+  qed (use less.prems in auto)
 qed
 
-
 subsection \<open>Integrability on subintervals\<close>
 
 lemma operative_integrableI:
@@ -3105,7 +3061,7 @@
   then have "f integrable_on cbox a b"
     using ac cb by (auto split: if_split_asm)
   with * show ?thesis
-    using ac cb by (auto simp add: integrable_on_def integral_unique split: if_split_asm)
+    using ac cb by (auto simp: integrable_on_def integral_unique split: if_split_asm)
 qed
 
 lemma integral_combine:
@@ -3115,12 +3071,9 @@
     and ab: "f integrable_on {a..b}"
   shows "integral {a..c} f + integral {c..b} f = integral {a..b} f"
 proof -
-  have "(f has_integral integral {a..c} f) {a..c}"
-    using ab \<open>c \<le> b\<close> integrable_subinterval_real by fastforce
-  moreover
-  have "(f has_integral integral {c..b} f) {c..b}"
-    using ab \<open>a \<le> c\<close> integrable_subinterval_real by fastforce
-  ultimately show ?thesis
+  have "(f has_integral integral {a..c} f) {a..c}" "(f has_integral integral {c..b} f) {c..b}"
+    using ab \<open>c \<le> b\<close> \<open>a \<le> c\<close> integrable_subinterval_real by fastforce+
+  then show ?thesis
     by (smt (verit, best) assms has_integral_combine integral_unique)
 qed
 
@@ -3171,7 +3124,7 @@
   then have sndp: "snd ` p division_of cbox a b"
     by (metis division_of_tagged_division)
   have "f integrable_on k" if "(x, k) \<in> p" for x k
-    using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
+    using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d by blast
   then show ?thesis
     unfolding division [symmetric, OF sndp] comm_monoid_set_F_and
     by auto
@@ -3214,7 +3167,7 @@
       have "?lhs \<le> e * content {x..y}"
         using yx False d x y \<open>e>0\<close> assms 
         by (intro has_integral_bound_real[where f="(\<lambda>u. f u - f x)"]) (auto simp: Idiff fux_int)
-      also have "... \<le> ?rhs"
+      also have "\<dots> \<le> ?rhs"
         using False by auto
       finally show ?thesis .
     next
@@ -3233,7 +3186,7 @@
       have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * content {y..x}"
         using yx True d x y \<open>e>0\<close> assms 
         by (intro has_integral_bound_real[where f="(\<lambda>u. f u - f x)"]) (auto simp: Idiff fux_int)
-      also have "... \<le> e * \<bar>y - x\<bar>"
+      also have "\<dots> \<le> e * \<bar>y - x\<bar>"
         using True by auto
       finally have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>" .
       then show ?thesis
@@ -3282,9 +3235,9 @@
   proof -
     have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
       by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
-          has_vector_derivative_within_subset subsetCE that(1,2))
+          has_vector_derivative_within_subset subsetCE that)
     then show ?thesis
-      by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
+      by (metis box_real(2) \<open>u \<le> v\<close> fundamental_theorem_of_calculus)
   qed
   then show ?thesis
     using that by blast
@@ -3304,10 +3257,6 @@
     and intfi: "(f has_integral i) (cbox a b)"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
 proof (cases "cbox a b = {}")
-  case True
-  then show ?thesis 
-    using intfi by auto
-next
   case False
   obtain w z where wz: "h ` cbox a b = cbox w z"
     using h by blast
@@ -3382,7 +3331,7 @@
       have "(\<Sum>(x,K)\<in>(\<lambda>(y,L). (g y, g ` L)) ` p. content K *\<^sub>R f x) 
           = (\<Sum>u\<in>p. case case u of (x,K) \<Rightarrow> (g x, g ` K) of (y,L) \<Rightarrow> content L *\<^sub>R f y)"
         by (metis (mono_tags, lifting) "*" sum.reindex_cong)
-      also have "... = (\<Sum>(x,K)\<in>p. r *\<^sub>R content K *\<^sub>R f (g x))"
+      also have "\<dots> = (\<Sum>(x,K)\<in>p. r *\<^sub>R content K *\<^sub>R f (g x))"
         using r by (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
       finally
       have "(\<Sum>(x, K)\<in>(\<lambda>(x,K). (g x, g ` K)) ` p. content K *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - i" 
@@ -3395,7 +3344,7 @@
   qed
   then show ?thesis
     by (auto simp: h_eq has_integral)
-qed
+qed (use intfi in auto)
 
 
 subsection \<open>Special case of a basic affine transformation\<close>
@@ -3409,7 +3358,7 @@
     have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} 
         = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
     using k
-    by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
+    by (auto simp: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
        (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
   also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
     by (intro measure_times) auto
@@ -3484,8 +3433,7 @@
     moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b-a) \<bullet> i"
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
-      by (simp add: image_affinity_cbox content_cbox'
-        prod.distrib[symmetric] inner_diff_left flip: prod_constant)
+      by (simp add: image_affinity_cbox content_cbox' inner_diff_left flip: prod_constant prod.distrib)
   qed
 qed
 
@@ -3625,8 +3573,7 @@
 
 lemma has_integral_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) (cbox a b)"
-    and "\<forall>k\<in>Basis. m k \<noteq> 0"
+  assumes "(f has_integral i) (cbox a b)" and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
          ((1/ \<bar>prod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
   apply (rule has_integral_twiddle[where f=f])
@@ -3643,8 +3590,7 @@
 
 lemma integrable_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "f integrable_on cbox a b"
-    and "\<forall>k\<in>Basis. m k \<noteq> 0"
+  assumes "f integrable_on cbox a b" and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "(\<lambda>x::'a. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) integrable_on
     ((\<lambda>x. \<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k) ` cbox a b)"
   using assms unfolding integrable_on_def
@@ -3655,9 +3601,9 @@
 proof -
   have "?lhs = (\<chi> k. f k (x \<bullet> axis k 1))"
     by (simp add: cart_eq_inner_axis)
-  also have "... = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)"
+  also have "\<dots> = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)"
     by (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
-  also have "... = ?rhs"
+  also have "\<dots> = ?rhs"
     by (simp add: Basis_vec_def UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
   finally show ?thesis .
 qed
@@ -3755,7 +3701,7 @@
 proof (cases "a = b")
   case True
   then have *: "cbox a b = {b}" "f b - f a = 0"
-    by (auto simp add:  order_antisym)
+    by (auto simp:  order_antisym)
   with True show ?thesis by auto
 next
   case False
@@ -3766,17 +3712,13 @@
     fix e :: real
     assume e: "e > 0"
     then have eba8: "(e * (b-a)) / 8 > 0"
-      using ab by (auto simp add: field_simps)
+      using ab by (auto simp: field_simps)
     note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format]
     have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
       by (simp add: bounded_linear_scaleR_left)
     have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
       (is "\<forall>x \<in> box a b. ?Q x") \<comment>\<open>The explicit quantifier is required by the following step\<close>
-    proof
-      fix x assume "x \<in> box a b"
-      with e show "?Q x"
-        using derf_exp [of x "e/2"] by auto
-    qed
+        using e derf_exp [of _ "e/2"] by auto
     then obtain d where d: "\<And>x. 0 < d x"
       "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk> \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
       unfolding bgauge_existence_lemma by metis
@@ -3803,7 +3745,7 @@
         proof
           show "norm ((e * (b - a) / 8 / norm (f' a)) *\<^sub>R f' a) \<le> e * (b - a) / 8"
                "0 < e * (b - a) / 8 / norm (f' a)"
-            using False ab e by (auto simp add: field_simps)
+            using False ab e by (auto simp: field_simps)
         qed 
       qed
       have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
@@ -3840,7 +3782,7 @@
     qed
     obtain db where "0 < db"
       and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
-                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b-a)) / 4"
+                   \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b-a)) / 4"
     proof -
       have "continuous (at b within {a..b}) f"
         using contf continuous_on_eq_continuous_within by force
@@ -3858,7 +3800,7 @@
         proof
           show "norm ((e * (b - a) / 8 / norm (f' b)) *\<^sub>R f' b) \<le> e * (b - a) / 8" 
                "0 < e * (b - a) / 8 / norm (f' b)"
-            using False ab e by (auto simp add: field_simps)
+            using False ab e by (auto simp: field_simps)
         qed
       qed
       have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4" 
@@ -3874,7 +3816,7 @@
         proof (rule add_mono)
           have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
             by (auto intro: mult_right_mono [OF lel])
-          also have "... \<le> e * (b-a) / 8"
+          also have "\<dots> \<le> e * (b-a) / 8"
             by (rule l)
           finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b-a) / 8" .
         next
@@ -3926,14 +3868,14 @@
           by metis
         have xd: "norm (u - x) < d x" "norm (v - x) < d x"
           using fineD[OF fine xk] \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> uv 
-          by (auto simp add: k subset_eq dist_commute dist_real_def)
+          by (auto simp: k subset_eq dist_commute dist_real_def)
         have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) =
               norm ((f u - f x - (u - x) *\<^sub>R f' x) - (f v - f x - (v - x) *\<^sub>R f' x))"
           by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff)
         also have "\<dots> \<le> e/2 * norm (u - x) + e/2 * norm (v - x)"
           by (metis norm_triangle_le_diff add_mono * xd)
         also have "\<dots> \<le> e/2 * norm (v - u)"
-          using p(2)[OF xk] by (auto simp add: field_simps k)
+          using p(2)[OF xk] by (auto simp: field_simps k)
         also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
           using result by (simp add: \<open>u \<le> v\<close>)
         finally have "e * (v - u)/2 < e * (v - u)/2"
@@ -3943,7 +3885,7 @@
       have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
           \<le> (\<Sum>(x, K)\<in>p - ?A. norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
         by (auto intro: sum_norm_le)
-      also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)/2)"
+      also have "\<dots> \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)/2)"
         using non by (fastforce intro: sum_mono)
       finally have I: "norm (\<Sum>(x, k)\<in>p - ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
                      \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
@@ -3959,7 +3901,7 @@
           with p that have "cbox u v \<noteq> {}"
             by blast
           then show "0 \<le> e * ((Sup k) - (Inf k))"
-            unfolding uv using e by (auto simp add: field_simps)
+            unfolding uv using e by (auto simp: field_simps)
         qed
         let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
         let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
@@ -3980,28 +3922,26 @@
           have 2: "norm(\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))  \<le> e * (b-a)/2"
           proof -
             have norm_le: "norm (sum f S) \<le> e"
-              if "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x = y" "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> e" "e > 0"
+              if \<section>: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x = y" "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> e" "e > 0"
               for S f and e :: real
             proof (cases "S = {}")
               case True
               with that show ?thesis by auto
             next
-              case False then obtain x where "x \<in> S"
-                by auto
-              then have "S = {x}"
-                using that(1) by auto
+              case False then obtain x where "S = {x}"
+                using \<section> by blast
               then show ?thesis
-                using \<open>x \<in> S\<close> that(2) by auto
+                by (simp add: that(2))
             qed
             have *: "p \<inter> ?C = ?B a \<union> ?B b"
               by blast
             then have "norm (\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) =
                        norm (\<Sum>(x,K) \<in> ?B a \<union> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
               by simp
-            also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + 
+            also have "\<dots> = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + 
                                    (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
               using p(1) ab e by (subst sum.union_disjoint) auto
-            also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
+            also have "\<dots> \<le> e * (b - a) / 4 + e * (b - a) / 4"
             proof (rule norm_triangle_le [OF add_mono])
               have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
                 using p that by fastforce
@@ -4013,12 +3953,12 @@
                   by blast
                 let ?v = "min v v'"
                 have "box a ?v \<subseteq> K \<inter> K'"
-                  unfolding v v' by (auto simp add: mem_box)
+                  unfolding v v' by (auto simp: mem_box)
                 then have "interior (box a (min v v')) \<subseteq> interior K \<inter> interior K'"
                   using interior_Int interior_mono by blast
                 moreover have "(a + ?v)/2 \<in> box a ?v"
                   using ne0  unfolding v v' content_eq_0 not_le
-                  by (auto simp add: mem_box)
+                  by (auto simp: mem_box)
                 ultimately have "(a + ?v)/2 \<in> interior K \<inter> interior K'"
                   unfolding interior_open[OF open_box] by auto
                 then show "K = K'"
@@ -4068,7 +4008,7 @@
                 proof -
                 obtain v where v: "c = cbox v b" and "v \<le> b"
                   using \<open>(b, c) \<in> p\<close> pb by blast
-                then have "v \<ge> a""b \<in> {v.. b}"  
+                then have "v \<ge> a""b \<in> {v.. b}"
                   using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
                 moreover have "{v..b} \<subseteq> ball b db"
                   using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
@@ -4077,7 +4017,7 @@
                 qed
               qed (use ab e in auto)
             qed
-            also have "... = e * (b-a)/2"
+            also have "\<dots> = e * (b-a)/2"
               by simp
             finally show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
                         content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2" .
@@ -4086,7 +4026,7 @@
             apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
             using 1 2 by (auto simp: split_paired_all)
         qed
-        also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
+        also have "\<dots> = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
           unfolding sum_distrib_left[symmetric]
           by (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag]) auto
         finally have norm_le: "norm (\<Sum>(x,K)\<in>p \<inter> {t. fst t \<in> {a, b}}. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
@@ -4216,12 +4156,11 @@
       then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
         using d2(2) ptag by auto
       have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
-        using t by (auto simp add: field_simps)
+        using t by (auto simp: field_simps)
       have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
-      proof (intro tagged_division_Un_interval_real)
-        show "{(c, {t..c})} tagged_division_of {a..c} \<inter> {x. t \<le> x \<bullet> 1}"
-          using \<open>t \<le> c\<close> by (auto simp: eqs tagged_division_of_self_real)
-      qed (auto simp: eqs ptag)
+        using \<open>t \<le> c\<close>
+        by (intro tagged_division_Un_interval_real [of _ _ _ 1 t])
+           (auto simp: eqs tagged_division_of_self_real eqs ptag)
       moreover
       have "d1 fine p \<union> {(c, {t..c})}"
         unfolding fine_def
@@ -4232,7 +4171,7 @@
       next
         fix x assume "x \<in> {t..c}"
         then have "dist c x < k"
-          using t(1) by (auto simp add: field_simps dist_real_def)
+          using t(1) by (auto simp: field_simps dist_real_def)
         with k show "x \<in> d1 c"
           unfolding d_def by auto
       qed  
@@ -4245,24 +4184,24 @@
           show "p \<inter> {(c, {t..c})} = {}"
             using \<open>t < c\<close> pt by force
         qed (use p'(1) in auto)
-        also have "... = (c - t) *\<^sub>R f c + ?SUM p"
+        also have "\<dots> = (c - t) *\<^sub>R f c + ?SUM p"
           using \<open>t \<le> c\<close> by auto
         finally show ?thesis .
       qed
       have "c - k < t"
-        using \<open>k>0\<close> t(1) by (auto simp add: field_simps)
+        using \<open>k>0\<close> t(1) by (auto simp: field_simps)
       moreover have "k \<le> w"
       proof (rule ccontr)
         assume "\<not> k \<le> w"
         then have "c + (k + w) / 2 \<notin> d c"
-          by (auto simp add: field_simps not_le not_less dist_real_def d_def)
+          by (auto simp: field_simps not_le not_less dist_real_def d_def)
         then have "c + (k + w) / 2 \<notin> ball c k"
           using k by blast
         then show False
           using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
       qed
       ultimately have cwt: "c - w < t"
-        by (auto simp add: field_simps)
+        by (auto simp: field_simps)
       have eq: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
                 integral {a..c} f) + (?SUM p - integral {a..t} f) + (c - t) *\<^sub>R f c"
         by auto
@@ -4310,7 +4249,7 @@
     have "(- c) - d < (- t)" "- t \<le> - c"
       using t by auto 
     from d[OF this] show "norm (integral {a..c} f - integral {a..t} f) < e"
-      by (auto simp add: algebra_simps norm_minus_commute *)
+      by (auto simp: algebra_simps norm_minus_commute *)
   qed
 qed
 
@@ -4350,7 +4289,7 @@
           using \<open>0 < d1\<close> \<open>0 < d2\<close> by simp
         show "dist (integral {a..y} f) (integral {a..x} f) < e"
           if "dist y x < min d1 d2" for y
-          by (smt (verit) d1 d2 dist_norm dist_real_def norm_minus_commute that)
+          by (smt (verit) d1 d2 dist_commute dist_norm dist_real_def that)
       qed
     qed
   qed
@@ -4444,12 +4383,12 @@
   have contf': "continuous_on {0 ..1} (f \<circ> ?\<phi>)"
   proof (rule continuous_intros continuous_on_subset[OF contf])+
     show "(\<lambda>u. (1 - u) *\<^sub>R c + u *\<^sub>R x) ` {0..1} \<subseteq> S"
-      using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> by (auto simp add: convex_alt algebra_simps)
+      using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> by (auto simp: convex_alt algebra_simps)
   qed
   have "t = u" if "?\<phi> t = ?\<phi> u" for t u
   proof -
     from that have "(t - u) *\<^sub>R x = (t - u) *\<^sub>R c"
-      by (auto simp add: algebra_simps)
+      by (auto simp: algebra_simps)
     then show ?thesis
       using \<open>x \<noteq> c\<close> by auto
   qed
@@ -4465,7 +4404,7 @@
   proof -
     have df: "(f has_derivative (\<lambda>h. 0)) (at (?\<phi> t) within ?\<phi> ` {0..1})"
       using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> that 
-      by (auto simp add: convex_alt algebra_simps intro: has_derivative_subset [OF derf])
+      by (auto simp: convex_alt algebra_simps intro: has_derivative_subset [OF derf])
     have "(f \<circ> ?\<phi> has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
       by (rule derivative_eq_intros df | simp)+
     then show ?thesis
@@ -4584,7 +4523,7 @@
       by (simp add: g_def)
   next
     case False
-    have iterate:"F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
+    have iterate: "F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
     proof (intro neutral ballI)
       fix x
       assume x: "x \<in> p - {cbox c d}"
@@ -4640,10 +4579,12 @@
     assume ?l
     then have "?g integrable_on cbox c d"
       using assms has_integral_integrable integrable_subinterval by blast
-    then have "f integrable_on cbox c d"
+    then have f: "f integrable_on cbox c d"
       by (rule integrable_eq) auto
-    moreover then have "i = integral (cbox c d) f"
-      by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
+    moreover have "i = integral (cbox c d) f"
+      using f \<open>(?g has_integral i) (cbox a b)\<close>
+      by (simp add: assms has_integral_restrict_closed_subinterval has_integral_unique
+          integrable_integral)
     ultimately show ?r by auto
   next
     assume ?r then show ?l
@@ -4689,7 +4630,7 @@
     define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
     have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" "i \<in> Basis" for x i
       using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
-      by (auto simp add: field_simps sum_negf c_def d_def)
+      by (auto simp: field_simps sum_negf c_def d_def)
     then have c_d: "cbox a b \<subseteq> cbox c d"
       by (meson B mem_box(2) subsetI)
     have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
@@ -4712,7 +4653,7 @@
       define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
       have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
         if "norm x \<le> B" and "i \<in> Basis" for x i
-          using that Basis_le_norm[of i x] by (auto simp add: field_simps sum_negf c_def d_def)
+          using that Basis_le_norm[of i x] by (auto simp: field_simps sum_negf c_def d_def)
         then have c_d: "cbox a b \<subseteq> cbox c d"
         by (simp add: B mem_box(2) subset_eq)
       have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm (0 - x) < C" and "i \<in> Basis" for x i
@@ -4721,8 +4662,8 @@
         by (auto simp: mem_box dist_norm)
       with C obtain z where z: "(f has_integral z) (cbox a b)" "norm (z-i) < norm (y-i)"
         using has_integral_restrict_closed_subintervals_eq[OF c_d] S by blast
-      moreover then have "z = y" 
-        by (blast intro: has_integral_unique[OF _ y])
+      moreover have "z = y" 
+        using z by (blast intro: has_integral_unique[OF _ y])
       ultimately show False
         by auto
     qed
@@ -4754,9 +4695,9 @@
 
 lemma integral_nonneg:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"
-  assumes f: "f integrable_on S" and 0: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
+  assumes "f integrable_on S" and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
   shows "0 \<le> integral S f"
-  by (rule has_integral_nonneg[OF f[unfolded has_integral_integral] 0])
+  using assms has_integral_nonneg by blast
 
 
 text \<open>Hence a general restriction property.\<close>
@@ -4865,7 +4806,7 @@
   proof (rule has_integral_spike [OF neg])
     have eq: "(\<lambda>x. (if x \<in> S then f x else 0) - (if x \<in> T then f x else 0)) =
             (\<lambda>x. if x \<in> T - S then - f x else if x \<in> S - T then f x else 0)"
-      by (force simp add: )
+      by force
     have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
       "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
       using S T has_integral_restrict_UNIV by auto
@@ -4914,7 +4855,7 @@
     then have *: "(indicator S has_integral 0) (cbox (a-c) (b-c))"
       by (meson Diff_iff assms has_integral_negligible indicator_simps(2))
     have eq: "indicator ((+) c ` S) = (\<lambda>x. indicator S (x - c))"
-      by (force simp add: indicator_def)
+      by (force simp: indicator_def)
     show "(indicator ((+) c ` S) has_integral 0) (cbox a b)"
       using has_integral_affinity [OF *, of 1 "-c"]
             cbox_translation [of "c" "-c+a" "-c+b"]
@@ -4971,13 +4912,14 @@
 lemma has_integral_interior:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
-  by (rule has_integral_spike_set_eq [OF empty_imp_negligible negligible_subset])
-     (use interior_subset in \<open>auto simp: frontier_def closure_def\<close>)
+proof (rule has_integral_spike_set_eq [OF empty_imp_negligible negligible_subset])
+qed (use interior_subset in \<open>auto simp: frontier_def closure_def\<close>)
 
 lemma has_integral_closure:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (closure S) \<longleftrightarrow> (f has_integral y) S"
-  by (rule has_integral_spike_set_eq [OF negligible_subset empty_imp_negligible]) (auto simp: closure_Un_frontier )
+proof (rule has_integral_spike_set_eq [OF negligible_subset empty_imp_negligible]) 
+qed (auto simp: closure_Un_frontier )
 
 lemma has_integral_open_interval:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
@@ -5082,7 +5024,7 @@
     show "?f integrable_on cbox a b"
     proof (rule integrable_subinterval[of _ ?a ?b])
       have "?a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> ?b \<bullet> i" if "norm (0 - x) < B" "i \<in> Basis" for x i
-        using Basis_le_norm[of i x] that by (auto simp add:field_simps)
+        using Basis_le_norm[of i x] that by (auto simp:field_simps)
       then have "ball 0 B \<subseteq> cbox ?a ?b"
         by (auto simp: mem_box dist_norm)
       then show "?f integrable_on cbox ?a ?b"
@@ -5154,12 +5096,12 @@
       have "sum ((*\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
             x \<bullet> i \<le> sum ((*\<^sub>R) (real n)) Basis \<bullet> i"
         if "norm x < B" "i \<in> Basis" for x i::'n
-          using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
+          using Basis_le_norm[of i x] n N that by (auto simp: field_simps sum_negf)
       then show ?thesis
         by (auto simp: mem_box dist_norm)
     qed
     then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (integral (?cube m) ?F) (integral (?cube n) ?F) < e"
-      by (fastforce simp add: dist_norm intro!: B)
+      by (fastforce simp: dist_norm intro!: B)
   qed
   then obtain i where i: "(\<lambda>n. integral (?cube n) ?F) \<longlonglongrightarrow> i"
     using convergent_eq_Cauchy by blast
@@ -5188,7 +5130,7 @@
         assume x: "x \<in> ball 0 B"
         have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
               \<Longrightarrow> sum ((*\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum ((*\<^sub>R) n) Basis \<bullet> i" for i
-          using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
+          using Basis_le_norm[of i x] n by (auto simp: field_simps sum_negf)
         then show "x \<in> ?cube n"
           using x by (auto simp: mem_box dist_norm)
       qed 
@@ -5267,7 +5209,7 @@
   have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on cbox a b"
     by (simp add: intf integrable_altD(1))
 then show ?thesis
-  by (metis (mono_tags) sub integrable_restrict_Int le_inf_iff order_refl subset_antisym)
+  by (simp add: inf.absorb2 integrable_restrict_Int sub)
 qed
 
 
@@ -5450,8 +5392,7 @@
       qed (use int_f int_g int_h fgh in \<open>simp_all add: integral_le\<close>)
     }
     then show ?thesis
-      apply (rule_tac x="max Bg Bh" in exI)
-        using \<open>Bg > 0\<close> by auto
+      by (meson \<open>0 < Bh\<close> linorder_not_less max.bounded_iff)
   qed
   then show ?thesis
     unfolding integrable_alt[of f] real_norm_def by (blast intro: int_f)
@@ -5492,7 +5433,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
   assumes "f integrable_on A" "f integrable_on B" "negligible (A \<inter> B)" "C = A \<union> B"
   shows   "f integrable_on C"
-  using integrable_Un[of A B f] assms by simp
+  by (simp add: assms integrable_Un set_zero)
 
 lemma has_integral_UN:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -5561,7 +5502,7 @@
       by (meson \<open>S \<in> \<D>\<close> \<open>s' \<in> \<D>\<close> \<D>(4))
     from \<D>(5)[OF that] show ?thesis
       unfolding obt interior_cbox
-      by (metis (no_types, lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval)
+      by (metis (lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval)
   qed
   show ?thesis
     unfolding \<D>(6)[symmetric]
@@ -5608,8 +5549,9 @@
     and "i \<subseteq> S"
   shows "f integrable_on i"
 proof -
-  have "f integrable_on i" if "i \<in> \<D>" for i
-    by (smt (verit, best) assms cbox_division_memE f integrable_on_subcbox order_trans that)
+  have "f integrable_on j" if "j \<in> \<D>" for j
+    using assms integrable_on_def that
+    by (metis cbox_division_memE elementary_interval has_integral_combine_division_topdown)
   then show ?thesis
     using \<D> integrable_combine_division by blast
 qed
@@ -5626,10 +5568,10 @@
   have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) S"
     by (smt (verit, del_insts) assms division_of_tagged_division has_integral_combine_division has_integral_iff imageE prod.collapse)
   also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)"
-    by (intro sum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null)
-       (simp add: content_eq_0_interior)
+    by (metis assms(1) eq_integralD has_integral_empty_eq has_integral_open_interval
+        sum.over_tagged_division_lemma)
   finally show ?thesis
-    using assms by (auto simp add: has_integral_iff intro!: sum.cong)
+    using assms by (auto simp: has_integral_iff intro!: sum.cong)
 qed
 
 lemma integral_combine_tagged_division_bottomup:
@@ -5655,7 +5597,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on cbox a b"
     and "p tagged_division_of (cbox a b)"
-  shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
+  shows "integral (cbox a b) f = (\<Sum>(x, k)\<in>p. integral k f)"
   using assms by (auto intro: integral_unique [OF has_integral_combine_tagged_division_topdown])
 
 
@@ -5792,17 +5734,17 @@
                   for ir ip i cr cp::'a
     using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"] that
     unfolding that(3)[symmetric] norm_minus_cancel
-    by (auto simp add: algebra_simps)
+    by (auto simp: algebra_simps)
 
   have "?lhs =  norm (?SUM p - (\<Sum>(x, k)\<in>p. integral k f))"
     unfolding split_def sum_subtractf ..
   also have "\<dots> \<le> e + k"
   proof (rule norm_le[OF less_e])
     have lessk: "k * real (card r) / (1 + real (card r)) < k"
-      using \<open>k>0\<close> by (auto simp add: field_simps)
+      using \<open>k>0\<close> by (auto simp: field_simps)
     have "norm (sum (?SUM \<circ> qq) r - (\<Sum>k\<in>r. integral k f)) \<le> (\<Sum>x\<in>r. k / (real (card r) + 1))"
       unfolding sum_subtractf[symmetric] by (force dest: qq intro!: sum_norm_le)
-    also have "... < k"
+    also have "\<dots> < k"
       by (simp add: lessk add.commute mult.commute)
     finally show "norm (sum (?SUM \<circ> qq) r - (\<Sum>k\<in>r. integral k f)) < k" .
   next
@@ -5814,15 +5756,14 @@
         using inp p'(4) by blast
       then show ?thesis
         using uv that p
-        by (metis content_eq_0_interior dual_order.refl inf.orderE integral_null ne tagged_partial_division_ofD(5))
+        by (metis content_eq_0_interior inf.orderE integral_null p'(5) subset_refl)
     qed
     then have "(\<Sum>(x, K)\<in>p. integral K f) = (\<Sum>K\<in>snd ` p. integral K f)"
       apply (subst sum.reindex_nontrivial [OF \<open>finite p\<close>])
       unfolding split_paired_all split_def by auto
     then show "(\<Sum>(x, k)\<in>p. integral k f) + (\<Sum>k\<in>r. integral k f) = integral (cbox a b) f"
       unfolding integral_combine_division_topdown[OF intf qdiv] r_def
-      using q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p", symmetric]
-        by simp
+      by (metis add.commute q q'(1) sum.subset_diff)
   qed
   finally show "?lhs \<le> e + k" .
 qed
@@ -5847,7 +5788,7 @@
       by (simp add: \<open>d fine p\<close> fine_subset)
     show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
       apply (rule Henstock_lemma_part1[OF fed less_e, unfolded split_def])
-      using Q tag tagged_partial_division_subset by (force simp add: fine)+
+      using Q tag tagged_partial_division_subset by (force simp: fine)+
   qed
 qed
 
@@ -5873,8 +5814,8 @@
     have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) 
           \<le> 2 * real DIM('n) * (e/(2 * (real DIM('n) + 1)))"
       using Henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
-    also have "... < e"
-      using \<open>e > 0\<close> by (auto simp add: field_simps)
+    also have "\<dots> < e"
+      using \<open>e > 0\<close> by (auto simp: field_simps)
     finally
     show "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) < e" .
   qed
@@ -5904,10 +5845,7 @@
   have fg1: "(f k x) \<le> (g x)" if x: "x \<in> cbox a b" for x k
   proof -
     have "\<forall>\<^sub>F j in sequentially. f k x \<le> f j x"
-    proof (rule eventually_sequentiallyI [of k])
-      show "\<And>j. k \<le> j \<Longrightarrow> f k x \<le> f j x"
-        using le x by (force intro: transitive_stepwise_le)
-    qed
+      by (metis eventually_sequentiallyI le lift_Suc_mono_le x)
     then show "f k x \<le> g x"
       using tendsto_lowerbound [OF fg] x trivial_limit_sequentially by blast
   qed
@@ -5952,9 +5890,8 @@
       with fg that LIMSEQ_D
       obtain N where "\<forall>n\<ge>N. norm (f n x - g x) < e/(4 * content (cbox a b))"
         by metis
-      then show "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> g x - f k x \<and> g x - f k x < e/(4 * content (cbox a b))"
-        apply (rule_tac x="N + r" in exI)
-        using fg1[OF that] by (auto simp add: field_simps)
+      with fg1[OF that] show "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> g x - f k x \<and> g x - f k x < e/(4 * content (cbox a b))"
+        by (rule_tac x="N + r" in exI) (auto simp: field_simps)
     qed
     then obtain m where r_le_m: "\<And>x. x \<in> cbox a b \<Longrightarrow> r \<le> m x"
        and m: "\<And>x k. \<lbrakk>x \<in> cbox a b; m x \<le> k\<rbrakk>
@@ -5976,13 +5913,13 @@
       have *: "\<bar>a - d\<bar> < e" if "\<bar>a - b\<bar> \<le> e/4" "\<bar>b - c\<bar> < e/2" "\<bar>c - d\<bar> < e/4" for a b c d
         using that norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
           norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
-        by (auto simp add: algebra_simps)
+        by (auto simp: algebra_simps)
       show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - i\<bar> < e"
       proof (rule *)
         have "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> 
               \<le> (\<Sum>i\<in>\<D>. \<bar>(case i of (x, K) \<Rightarrow> content K *\<^sub>R g x) - (case i of (x, K) \<Rightarrow> content K *\<^sub>R f (m x) x)\<bar>)"
           by (metis (mono_tags) sum_subtractf sum_abs) 
-        also have "... \<le> (\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b))))"
+        also have "\<dots> \<le> (\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b))))"
         proof (rule sum_mono, simp add: split_paired_all)
           fix x K
           assume xk: "(x,K) \<in> \<D>"
@@ -5993,17 +5930,16 @@
           then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e/(4 * content (cbox a b))"
             by (simp add: algebra_simps)
         qed
-        also have "... = (e/(4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
+        also have "\<dots> = (e/(4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
           by (simp add: sum_distrib_left sum_divide_distrib split_def mult.commute)
-        also have "... \<le> e/4"
+        also have "\<dots> \<le> e/4"
           by (metis False additive_content_tagged_division [OF ptag] nonzero_mult_divide_mult_cancel_right order_refl times_divide_eq_left)
         finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> \<le> e/4" .
 
       next
         have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
               \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
-          apply (subst sum.group)
-          using s by (auto simp: sum_subtractf split_def p'(1))
+          using s by (subst sum.group) (auto simp: sum_subtractf split_def p')
         also have "\<dots> < e/2"
         proof -
           have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> \<D>. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
@@ -6014,7 +5950,7 @@
             have "norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
                   norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
               by (force intro!: sum.cong arg_cong[where f=norm])
-            also have "... \<le> e/2 ^ (t + 2)"
+            also have "\<dots> \<le> e/2 ^ (t + 2)"
             proof (rule Henstock_lemma_part1 [OF intf])
               show "{xk \<in> \<D>. m (fst xk) = t} tagged_partial_division_of cbox a b"
               proof (rule tagged_partial_division_subset[of \<D>])
@@ -6027,7 +5963,7 @@
             finally show "norm (\<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
                                 integral K (f (m x))) \<le> e/2 ^ (t + 2)" .
           qed
-          also have "... = (e/2/2) * (\<Sum>i = 0..s. (1/2) ^ i)"
+          also have "\<dots> = (e/2/2) * (\<Sum>i = 0..s. (1/2) ^ i)"
             by (simp add: sum_distrib_left field_simps)
           also have "\<dots> < e/2"
             by (simp add: sum_gp mult_strict_left_mono[OF _ e])
@@ -6145,14 +6081,13 @@
         using that by auto
       with LIMSEQ_D [OF i] obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (integral S (f n) - i) < e/4"
         by metis
-      with int_f[of N, unfolded has_integral_integral has_integral_alt'[of "f N"]] 
       obtain B where "0 < B" and B: 
         "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> norm (integral (cbox a b) (?f N) - integral S (f N)) < e/4"
-        by (meson \<open>0 < e/4\<close>)
+        by (metis (lifting) ext \<open>0 < e/4\<close> has_integral_alt' int_f integrable_integral)
       have "norm (integral (cbox a b) ?g - i) < e" if  ab: "ball 0 B \<subseteq> cbox a b" for a b
       proof -
         obtain M where M: "\<And>n. n \<ge> M \<Longrightarrow> abs (integral (cbox a b) (?f n) - integral (cbox a b) ?g) < e/2"
-          using \<open>e > 0\<close> g by (fastforce simp add: dest!: LIMSEQ_D [where r = "e/2"])
+          using \<open>e > 0\<close> g by (fastforce simp: dest!: LIMSEQ_D [where r = "e/2"])
         have *: "\<And>\<alpha> \<beta> g. \<lbrakk>\<bar>\<alpha> - i\<bar> < e/2; \<bar>\<beta> - g\<bar> < e/2; \<alpha> \<le> \<beta>; \<beta> \<le> i\<rbrakk> \<Longrightarrow> \<bar>g - i\<bar> < e"
           unfolding real_inner_1_right by arith
         show "norm (integral (cbox a b) ?g - i) < e"
@@ -6182,7 +6117,7 @@
             by (metis Int_lower1 f0 inf_commute int' int_f integral_subset_le)
           then have "integral (cbox a b) (?f (M + N)) \<le> integral S (f (M + N))"
             by (metis (no_types) inf_commute integral_restrict_Int)
-          also have "... \<le> i"
+          also have "\<dots> \<le> i"
             using i'[of "M + N"] by auto
           finally show "integral (cbox a b) (?f (M + N)) \<le> i" .
         qed
@@ -6206,12 +6141,8 @@
     show "\<And>k. (\<lambda>x. f (Suc k) x - f 0 x) integrable_on S"
       by (simp add: integrable_diff int_f)
     show "(\<lambda>k. f (Suc k) x - f 0 x) \<longlonglongrightarrow> g x - f 0 x" if "x \<in> S" for x
-    proof -
-      have "(\<lambda>n. f (Suc n) x) \<longlonglongrightarrow> g x"
-        using LIMSEQ_ignore_initial_segment[OF fg[OF \<open>x \<in> S\<close>], of 1] by simp
-      then show ?thesis
-        by (simp add: tendsto_diff)
-    qed
+      using LIMSEQ_ignore_initial_segment[OF fg[OF \<open>x \<in> S\<close>], of 1]
+      by (simp add: tendsto_diff)
     show "bounded (range (\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)))"
     proof -
       obtain B where B: "\<And>k. norm (integral S (f k)) \<le> B"
@@ -6225,7 +6156,7 @@
   qed (use * in auto)
   then have "(\<lambda>x. integral S (\<lambda>xa. f (Suc x) xa - f 0 xa) + integral S (f 0))
              \<longlonglongrightarrow> integral S (\<lambda>x. g x - f 0 x) + integral S (f 0)"
-    by (auto simp add: tendsto_add)
+    by (auto simp: tendsto_add)
   moreover have "(\<lambda>x. g x - f 0 x + f 0 x) integrable_on S"
     using gf integrable_add int_f [of 0] by metis
   ultimately show ?thesis
@@ -6546,8 +6477,8 @@
         norm (integral (cbox a b) (\<lambda>t. f y t - f x t))"
         using elim \<open>x \<in> U\<close>
         unfolding dist_norm
-        by (subst integral_diff)
-           (auto intro!: integrable_continuous continuous_intros)
+        proof (subst integral_diff)
+        qed (auto intro!: integrable_continuous continuous_intros)
       also have "\<dots> \<le> e * content (cbox a b)"
         using elim \<open>x \<in> U\<close>
         by (intro integrable_bound)
@@ -6597,9 +6528,7 @@
     moreover
     have "\<forall>\<^sub>F x in at x0 within U. x \<in> X0"
       using \<open>open X0\<close> \<open>x0 \<in> X0\<close> eventually_at_topological by blast
-    moreover have "\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0"
-      by (auto simp: eventually_at_filter)
-    moreover have "\<forall>\<^sub>F x in at x0 within U. x \<in> U"
+    moreover have "\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0" "\<forall>\<^sub>F x in at x0 within U. x \<in> U"
       by (auto simp: eventually_at_filter)
     ultimately
     show "\<forall>\<^sub>F x in at x0 within U. norm ((?F x - ?F x0 - ?dF (x - x0)) /\<^sub>R norm (x - x0)) < e'"
@@ -6617,27 +6546,23 @@
             auto intro!: integrable_diff integrable_f2 continuous_intros
               intro: integrable_continuous)+
       also
-      {
+      have "norm ?id \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))"
+      proof (intro integral_norm_bound_integral)
         fix t assume t: "t \<in> (cbox a b)"
         then have deriv:
           "((\<lambda>x. f x t) has_derivative (fx y t)) (at y within X0 \<inter> U)"
           if "y \<in> X0 \<inter> U" for y
           using fx has_derivative_subset that by fastforce
         have seg: "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R (x - x0) \<in> X0 \<inter> U"
-          using \<open>closed_segment x0 x \<subseteq> U\<close>
-            \<open>closed_segment x0 x \<subseteq> X0\<close>
+          using \<open>closed_segment x0 x \<subseteq> U\<close> \<open>closed_segment x0 x \<subseteq> X0\<close>
           by (force simp: closed_segment_def algebra_simps)
         have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
           using fx_bound t
-          by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
+          by (auto simp: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
         from differentiable_bound_linearization[OF seg deriv this] X0
-        have "norm (f x t - f x0 t - fx x0 t (x - x0)) \<le> e * norm (x - x0)"
-          by (auto simp add: ac_simps)
-      }
-      then have "norm ?id \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))"
-        by (intro integral_norm_bound_integral)
-          (auto intro!: continuous_intros integrable_diff integrable_f2
-            intro: integrable_continuous)
+        show "norm (f x t - f x0 t - fx x0 t (x - x0)) \<le> e * norm (x - x0)"
+          by (auto simp: ac_simps)
+      qed (force intro: continuous_intros integrable_diff integrable_f2 integrable_continuous)+
       also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
         by simp
       also have "\<dots> < e' * norm (x - x0)"
@@ -6769,8 +6694,7 @@
       then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
       proof eventually_elim
         case (elim n)
-        have "I n = integral (cbox a b) (f n)"
-            "J = integral (cbox a b) g"
+        have "I n = integral (cbox a b) (f n)" "J = integral (cbox a b) g"
           using I[of n] J by (simp_all add: integral_unique)
         then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))"
           by (simp add: integral_diff dist_norm)
@@ -6951,8 +6875,8 @@
       and "continuous_on {c..d} f"
       and "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
     shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
-  by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
-     (auto intro: DERIV_continuous_on assms)
+proof (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
+qed (auto intro: DERIV_continuous_on assms)
 
 lemma integral_shift:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -7053,7 +6977,7 @@
   show "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
           \<le> e * content (cbox (u,w) (v,z))"
     using content_cbox_pair_eq0_D [OF c0']
-    by (force simp add: c0')
+    by (force simp: c0')
 next
   fix a::'a and c::'b and b::'a and d::'b
   and M::real and i::'a and j::'b
@@ -7171,7 +7095,7 @@
           \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
               integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
               \<le> e' * content (cbox (u, w) (v, z))"
-        using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp add: comm_monoid_set_F_and)
+        using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp: comm_monoid_set_F_and)
       with False have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
           \<le> e"
         if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
@@ -7181,13 +7105,14 @@
         using that by (simp add: e'_def)
     } note op_acbd = this
     { fix k::real and \<D> and u::'a and v w and z::'b and t1 t2 l
+      let ?CBUZ = "cbox (u,w) (v,z)"
       assume k: "0 < k"
          and nf: "\<And>x y u v.
                   \<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk>
                   \<Longrightarrow> norm (f(u,v) - f(x,y)) < e/(2 * (content ?CBOX))"
          and p_acbd: "\<D> tagged_division_of cbox (a,c) (b,d)"
          and fine: "(\<lambda>x. ball x k) fine \<D>"  "((t1,t2), l) \<in> \<D>"
-         and uwvz_sub: "cbox (u,w) (v,z) \<subseteq> l" "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"
+         and uwvz_sub: "?CBUZ \<subseteq> l" "?CBUZ \<subseteq> cbox (a,c) (b,d)"
       have t: "t1 \<in> cbox a b" "t2 \<in> cbox c d"
         by (meson fine p_acbd cbox_Pair_iff tag_in_interval)+
       have ls: "l \<subseteq> ball (t1,t2) k"
@@ -7200,17 +7125,17 @@
           by (simp add: norm_Pair norm_minus_commute)
         also have "norm (t1 - x1, t2 - x2) < k"
           using xuvwz ls uwvz_sub unfolding ball_def
-          by (force simp add: cbox_Pair_eq dist_norm )
+          by (force simp: cbox_Pair_eq dist_norm )
         finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX/2"
           using nf [OF t x]  by simp
       } note nf' = this
-      have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
+      have f_int_uwvz: "f integrable_on ?CBUZ"
         using f_int_acbd uwvz_sub integrable_on_subcbox by blast
       have f_int_uv: "\<And>x. x \<in> cbox u v \<Longrightarrow> (\<lambda>y. f (x,y)) integrable_on cbox w z"
         using assms continuous_on_subset uwvz_sub
         by (blast intro: continuous_on_imp_integrable_on_Pair1)
-      have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
-             \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
+      have 1: "norm (integral ?CBUZ f - integral ?CBUZ (\<lambda>x. f (t1,t2)))
+             \<le> e * content ?CBUZ / content ?CBOX/2"
         using cbp \<open>0 < e/content ?CBOX\<close> nf'
         apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
         apply (auto simp: integrable_diff f_int_uwvz integrable_const intro: order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
@@ -7232,17 +7157,17 @@
         apply (intro integrable_bound [OF _ _ normint_wz])
         apply (auto simp: field_split_simps integrable_diff int_integrable integrable_const)
         done
-      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
+      also have "\<dots> \<le> e * content ?CBUZ / content ?CBOX/2"
         by (simp add: content_Pair field_split_simps)
       finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
                       integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
-                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
+                \<le> e * content ?CBUZ / content ?CBOX/2"
         by (simp only: integral_diff [symmetric] int_integrable integrable_const)
       have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
         using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] field_sum_of_halves
         by (simp add: norm_minus_commute)
-      have "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
-            \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
+      have "norm (integral ?CBUZ f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
+            \<le> e * content ?CBUZ / content ?CBOX"
         by (rule norm_xx [OF integral_Pair_const 1 2])
     } note * = this
     have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e" 
@@ -7289,9 +7214,9 @@
 proof -
   have "integral (cbox a b) (\<lambda>x. integral (cbox c d) (f x)) = integral (cbox (a, c) (b, d)) (\<lambda>(x, y). f x y)"
     using integral_prod_continuous [OF assms] by auto
-  also have "... = integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)"
+  also have "\<dots> = integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)"
     by (rule integral_swap_2dim [OF assms])
-  also have "... = integral (cbox c d) (\<lambda>y. integral (cbox a b) (\<lambda>x. f x y))"
+  also have "\<dots> = integral (cbox c d) (\<lambda>y. integral (cbox a b) (\<lambda>x. f x y))"
     using integral_prod_continuous [OF swap_continuous] assms
     by auto
   finally show ?thesis .
@@ -7392,17 +7317,18 @@
   proof (cases "inverse (of_nat (Suc k)) \<le> c")
     case True
     have x: "x > 0" if "x \<ge> inverse (1 + real k)" for x
-      by (smt (verit) that inverse_Suc of_nat_Suc)
+      by (metis inverse_Suc of_nat_Suc order_less_le_trans that)
     hence "((\<lambda>x. x powr a) has_integral c powr (a + 1) / (a + 1) -
                inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}"
-      using True a by (intro fundamental_theorem_of_calculus)
-        (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
-          simp: has_real_derivative_iff_has_vector_derivative [symmetric])
+      using True a 
+    proof (intro fundamental_theorem_of_calculus)
+    qed (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
+          simp flip: has_real_derivative_iff_has_vector_derivative)
     with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
   next
     case False
-    thus ?thesis unfolding f_def F_def 
-      by (subst has_integral_restrict) auto
+    thus ?thesis unfolding f_def F_def
+      by force 
   qed
   then have integral_f: "integral {0..c} (f k) = F k" for k
     by blast
@@ -7436,7 +7362,7 @@
     {
       fix k
       from a have "F k \<le> c powr (a + 1) / (a + 1)"
-        by (auto simp add: F_def divide_simps)
+        by (auto simp: F_def divide_simps)
       also from a have "F k \<ge> 0"
         by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2)
       hence "F k = abs (F k)" by simp
@@ -7482,8 +7408,8 @@
     by (meson eventually_at_top_linorderI integral_unique)
   moreover have "((\<lambda>y::real. F y - F a) \<longlongrightarrow> - F a) at_top"
     using assms unfolding F_def by real_asymp
-  ultimately show "((\<lambda>y. integral {a..y} (\<lambda>x. x powr e)) 
-              \<longlongrightarrow> - (a powr (e+1)) / (e+1)) at_top"
+  ultimately 
+  show "((\<lambda>y. integral {a..y} (\<lambda>x. x powr e))  \<longlongrightarrow> - (a powr (e+1)) / (e+1)) at_top"
     by (simp add: F_def filterlim_cong)
 qed (use assms in auto)
 
@@ -7500,8 +7426,8 @@
   also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
     by (intro powr_realpow)
   finally show ?thesis
-    by (rule has_integral_eq [rotated])
-       (insert assms, simp_all add: powr_minus powr_realpow field_split_simps)
+  proof (rule has_integral_eq [rotated])
+  qed (insert assms, simp_all add: powr_minus powr_realpow field_split_simps)
 qed
 
 subsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>