author paulson Sat, 31 Oct 2020 21:24:40 +0000 changeset 72532 088e2141f5e6 parent 72526 a3d096a98b69 (current diff) parent 72531 ee2ba879afb5 (diff) child 72533 63ec86626ec3
merged
```--- a/src/HOL/Analysis/Arcwise_Connected.thy	Sat Oct 31 21:06:29 2020 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Sat Oct 31 21:24:40 2020 +0000
@@ -16,9 +16,8 @@
lemma segment_to_closest_point:
fixes S :: "'a :: euclidean_space set"
shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
-  apply (subst disjoint_iff_not_equal)
-  apply (clarify dest!: dist_in_open_segment)
-  by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+  unfolding disjoint_iff
+  by (metis closest_point_le dist_commute dist_in_open_segment not_le)

lemma segment_to_point_exists:
fixes S :: "'a :: euclidean_space set"
@@ -110,10 +109,7 @@
show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
proof (intro conjI)
show "\<Inter>(F ` UNIV) \<noteq> {}"
-      apply (rule compact_nest)
-      apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
-      by (meson Fsub lift_Suc_antimono_le)
+      by (metis F Fsub \<open>compact S\<close> cloF closed_Int_compact compact_nest inf.orderE lift_Suc_antimono_le)
show " \<Inter>(F ` UNIV) \<subseteq> S"
using F by blast
show "\<phi> (\<Inter>(F ` UNIV))"
@@ -160,12 +156,9 @@
also have "... = e"
by simp
finally have "dist (\<Sum>i\<in>Basis. (\<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x < e" .
-    then
+    with Ints_of_int
show "\<exists>k. \<exists>f \<in> Basis \<rightarrow> \<int>. dist (\<Sum>b\<in>Basis. (f b / 2^k) *\<^sub>R b) x < e"
-      apply (rule_tac x=k in exI)
-      apply (rule_tac x="\<lambda>i. of_int (floor (2^k*(x \<bullet> i)))" in bexI)
-       apply auto
-      done
+      by fastforce
qed
then show ?thesis by auto
qed
@@ -223,8 +216,7 @@
definition\<^marker>\<open>tag unimportant\<close> dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"

-  by (metis divide_numeral_1 numeral_One power_0)

lemma nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
proof
@@ -264,8 +256,8 @@
then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)"
by linarith
then obtain "4*m + k = 4*m' + k" "n=n'"
-      apply (rule prime_power_cancel2 [OF two_is_prime_nat])
-      using assms by auto
+      using prime_power_cancel2 [OF two_is_prime_nat] assms
+      by (metis even_mult_iff even_numeral odd_add)
then have "m=m'" "n=n'"
by auto
}
@@ -353,13 +345,14 @@
done
next
-    apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc)
-    apply (intro conjI subsetI)
-    apply (auto simp del: power_Suc)
-      apply (metis divide_numeral_1 numeral_One power_0)
-     apply (metis of_nat_Suc of_nat_mult of_nat_numeral)
+  have "range of_nat \<subseteq> (\<Union>k m. {(of_nat m::'a) / 2 ^ k})"
+    by clarsimp (metis divide_numeral_1 numeral_One power_0)
+  moreover have "\<And>k m. \<exists>k' m'. ((1::'a) + 4 * of_nat m) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
+    by (metis (no_types) of_nat_Suc of_nat_mult of_nat_numeral)
+  moreover have "\<And>k m. \<exists>k' m'. (4 * of_nat m + (3::'a)) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
+  ultimately show "?rhs \<subseteq> dyadics"
+    by (auto simp: dyadics_def Nats_def)
qed

@@ -369,9 +362,8 @@
| "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
| "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined"
using iff_4k [of _ 1] iff_4k [of _ 3]
-         apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43, atomize_elim)
-  done
+  by (fastforce simp:  field_simps)+

lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
@@ -452,13 +444,16 @@

lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
-
+  show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)"
+qed

lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
+  show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)"
+qed

assumes "n > 0"
@@ -509,17 +504,15 @@

lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
-  done

lemma leftrec_43: "n > 0 \<Longrightarrow>
leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
-  done

lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v"
@@ -528,14 +521,12 @@
rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
-  done

lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
-  done

"{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
@@ -565,8 +556,8 @@
with that have "m \<in> cbox c0 d0"
by auto
obtain c d where cd: "{a..b} \<inter> f -` {f m} = {c..d}"
-      apply (rule_tac c="max a c0" and d="min b d0" in that)
-      using ab01 cd0 by auto
+      using ab01 cd0
+      by (rule_tac c="max a c0" and d="min b d0" in that) auto
then have cdab: "{c..d} \<subseteq> {a..b}"
by blast
show ?thesis
@@ -614,7 +605,7 @@
apply (rule that, blast)
done
then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b"
-    and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
+       and  left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
by auto
have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
@@ -709,24 +700,17 @@
case True
then obtain r where r: "m = 2*r" by (metis evenE)
show ?thesis
-            using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"]
-              Suc.IH [of "m+1"]
-            apply (simp add: r m add.commute [of 1] \<open>n > 0\<close> a41 b41 del: power_Suc)
-            apply (auto simp: left_right [THEN conjunct1])
-            using  order_trans [OF left_le c_le_v]
+            using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"]
+            using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] left_right \<open>n > 0\<close>
+            by (simp_all add: r m add.commute [of 1]  a41 b41 del: power_Suc)
next
case False
then obtain r where r: "m = 2*r + 1" by (metis oddE)
show ?thesis
-            using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"]
-              Suc.IH [of "m+1"]
-            apply (simp add: r m add.commute [of 3] \<open>n > 0\<close> a43 b43 del: power_Suc)
-            apply (auto simp: add.commute left_right [THEN conjunct2])
-            using  order_trans [OF c_ge_u right_ge]
-             apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral)
-            apply (metis Suc.IH mult_2 of_nat_1 of_nat_add)
-            done
+            using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"]
+            using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right \<open>n > 0\<close>
+            apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc)
qed
qed
qed
@@ -738,8 +722,7 @@
have alec [simp]: "a(m / 2^n) \<le> c(m / 2^n)" and cleb [simp]: "c(m / 2^n) \<le> b(m / 2^n)" for m::nat and n
by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv)
have c_ge_0 [simp]: "0 \<le> c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n) \<le> 1" for m::nat and n
-    using a_ge_0 alec order_trans apply blast
-    by (meson b_le_1 cleb order_trans)
+    using a_ge_0 alec b_le_1 cleb order_trans by blast+
have "\<lbrakk>d = m-n; odd j; \<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n\<rbrakk>
\<Longrightarrow> (a(j / 2^n)) \<le> (c(i / 2^m)) \<and> (c(i / 2^m)) \<le> (b(j / 2^n))" for d i j m n
proof (induction d arbitrary: j n rule: less_induct)
@@ -786,25 +769,27 @@
by (auto simp: ac)
next
case True show ?thesis
-        proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases)
+        proof (cases "i / 2^m" "j / 2^n" rule: linorder_cases)
case less
moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n"
using k by (force simp: field_split_simps)
-          moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
+          moreover have "\<bar>real i / 2 ^ m - j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
-          have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+          have "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
-            apply (rule less.IH [OF _ refl])
-            using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps  \<open>n < m\<close> diff_less_mono2)
-            done
-          show ?thesis
+          proof (rule less.IH [OF _ refl])
+            show "m - Suc n < d"
+              using \<open>n < m\<close> diff_less_mono2 less.prems(1) lessI by presburger
+            show "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+              using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
+          qed auto
+          then show ?thesis
using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
-            using k a41 b41 * \<open>0 < n\<close>
-            done
+            using k a41 b41 \<open>0 < n\<close>
next
case equal then show ?thesis by simp
next
@@ -815,17 +800,19 @@
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
-          have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+          have "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
-            apply (rule less.IH [OF _ refl])
-            using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps  \<open>n < m\<close> diff_less_mono2)
-            done
-          show ?thesis
+          proof (rule less.IH [OF _ refl])
+            show "m - Suc n < d"
+              using \<open>n < m\<close> diff_less_mono2 less.prems(1) by blast
+            show "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+              using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps  \<open>n < m\<close> diff_less_mono2)
+          qed auto
+          then show ?thesis
using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
-            using k a43 b43 * \<open>0 < n\<close>
-            done
+            using k a43 b43 \<open>0 < n\<close>
qed
qed
qed
@@ -912,9 +899,7 @@
with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
-          apply (simp add: m1_to_3 a41 b43 del: power_Suc)
-          apply (subst of_nat_diff, auto)
-          done
+          by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -924,8 +909,7 @@
= f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))"
using alec [of "2*k+1" n] cleb [of "2*k+1" n] a_ge_0 [of "2*k+1" n]  b_le_1 [of "2*k+1" n] k
using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
-           apply (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
-          done
+          by (auto simp: add.commute  feqm [OF order_refl]  feqm [OF _ order_refl, symmetric])
then
show ?thesis
@@ -951,9 +935,7 @@
by auto
then show ?thesis
using Suc.IH [of k] k \<open>0 < k\<close>
-        apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
-        apply (auto simp: of_nat_diff)
-        done
+        by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -1057,8 +1039,7 @@
show thesis
proof
show "(1::nat) < 2 ^ n"
-                apply (subst one_less_power)
-                using \<open>n > 0\<close> by auto
+                by (metis Suc_1 \<open>0 < n\<close> lessI one_less_power)
show "\<bar>real i / 2 ^ m - real 1/2 ^ n\<bar> < 1/2 ^ n"
using i less_j1 by (simp add: dist_norm field_simps True)
show "\<bar>real k / 2 ^ p - real 1/2 ^ n\<bar> < 1/2 ^ n"
@@ -1109,35 +1090,34 @@
qed
show ?thesis
proof
-              have "real j < 2 ^ n"
-                using j_le i k
-                apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff
-                    elim!: le_less_trans)
-                 apply (auto simp: field_simps)
-                done
+              have "2 ^ n * real i / 2 ^ m < 2 ^ n" "2 ^ n * real k / 2 ^ p < 2 ^ n"
+                using i k by (auto simp: field_simps)
+              then have "max (2^n * i / 2^m) (2^n * k / 2^p) < 2^n"
+                by simp
+              with j_le have "real j < 2 ^ n" by linarith
then show "j < 2 ^ n"
by auto
-              show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+              have "\<bar>real i * 2 ^ n - real j * 2 ^ m\<bar> < 2 ^ m"
using clo less_j1 j_le
-                apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
-                 apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
-                done
-              show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
-                using  clo less_j1 j_le
-                apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
-                 apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
-                done
+                 by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 1 2)
+              then show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+                by (auto simp: field_split_simps)
+              have "\<bar>real k * 2 ^ n - real j * 2 ^ p\<bar> < 2 ^ p"
+                using clo less_j1 j_le
+                by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 3 2)
+              then show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
+                by (auto simp: le_max_iff_disj field_split_simps dist_norm)
qed (use False in simp)
qed
qed
show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e"
proof (rule dist_triangle_half_l)
show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2"
-            apply (rule dist_fc_close)
-            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto
+            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj
+            by (intro dist_fc_close) auto
show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
-            apply (rule dist_fc_close)
-            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto
+            using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij
+            by (intro dist_fc_close) auto
qed
qed
qed
@@ -1191,8 +1171,7 @@
proof cases
case 1
then show ?thesis
-              apply (rule_tac x=u in exI)
-              using uabv [of 1 1] f0u [of u] f0u [of x] by auto
+              using uabv [of 1 1] f0u [of u] f0u [of x] by force
next
case 2
then show ?thesis
@@ -1200,8 +1179,7 @@
next
case 3
then show ?thesis
-              apply (rule_tac x=v in exI)
-              using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto
+              using uabv [of 1 1] fv1 [of v] fv1 [of x] by force
qed
with \<open>n=0\<close> show ?thesis
by (rule_tac x=1 in exI) auto
@@ -1212,6 +1190,9 @@
and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
by metis
then obtain j where j: "m = 2*j + 1" by (metis oddE)
+          have j4: "4 * j + 1 < 2 ^ Suc n"
+            using mless j by (simp add: algebra_simps)
+
consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
| "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
| "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
@@ -1219,33 +1200,35 @@
then show ?thesis
proof cases
case 1
-            then show ?thesis
-              apply (rule_tac x="4*j + 1" in exI)
-              apply (rule_tac x=y in exI)
-              using mless j \<open>n \<noteq> 0\<close>
-              apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc)
-              done
+            show ?thesis
+            proof (intro exI conjI)
+              show "y \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+                using mless j \<open>n \<noteq> 0\<close> 1 by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
+            qed (use feq j4 in auto)
next
case 2
show ?thesis
-              apply (rule_tac x="4*j + 1" in exI)
-              apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI)
-              using mless \<open>n \<noteq> 0\<close> 2 j
-              using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n]  b_le_1 [of "2*j+1" n]
-              using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
-              apply (auto simp: feq [symmetric] intro: f_eqI)
-              done
+            proof (intro exI conjI)
+              show "b (real (4 * j + 1) / 2 ^ Suc n) \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+                using \<open>n \<noteq> 0\<close> alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n]
+                using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
+              show "f (b (real (4 * j + 1) / 2 ^ Suc n)) = f x"
+                using \<open>n \<noteq> 0\<close> 2
+                using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n]  b_le_1 [of "2*j+1" n]
+                by (force simp add: b41 a43 add.commute [of 1] feq [symmetric] simp del: power_Suc intro: f_eqI)
+            qed (use j4 in auto)
next
case 3
-            then show ?thesis
-              apply (rule_tac x="4*j + 3" in exI)
-              apply (rule_tac x=y in exI)
-              using mless j \<open>n \<noteq> 0\<close>
-              apply (simp add: feq a43 b43 del: power_Suc)
-              done
+            show ?thesis
+            proof (intro exI conjI)
+              show "4 * j + 3 < 2 ^ Suc n"
+                using mless j by simp
+              show "f y = f x"
+                by fact
+              show "y \<in> {a (real (4 * j + 3) / 2 ^ Suc n) .. b (real (4 * j + 3) / 2 ^ Suc n)}"
+                using 3 False b43 [of n j] by (simp add: add.commute)
+            qed (use 3 in auto)
qed
qed
qed
@@ -1255,24 +1238,26 @@
by fastforce
with * obtain m::nat and y
where "odd m" "0 < m" and mless: "m < 2 ^ n"
-          and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
-        by metis
+          and y: "a(m / 2^n) \<le> y \<and> y \<le> b(m / 2^n)" and feq: "f x = f y"
+        by (metis atLeastAtMost_iff)
then have "0 \<le> y" "y \<le> 1"
-        by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
+        by (meson a_ge_0 b_le_1 order.trans)+
moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
-        using y apply simp_all
-        using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
+        using y alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
by linarith+
moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
-      ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
-        apply (rule_tac x=n in exI)
-        apply (rule_tac x=m in bexI)
-         apply (auto simp: dist_norm h_eq feq \<delta>)
-        done
+      ultimately have "dist (h (real m / 2 ^ n)) (f x) < e"
+        by (auto simp: dist_norm h_eq feq \<delta>)
+      then show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
+        using \<open>0 < m\<close> greaterThanLessThan_iff mless by blast
qed
also have "... \<subseteq> h ` {0..1}"
-      apply (rule closure_minimal)
-      using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
+    proof (rule closure_minimal)
+      show "h ` D01 \<subseteq> h ` {0..1}"
+        using cloD01 closure_subset by blast
+      show "closed (h ` {0..1})"
+        using compact_continuous_image [OF cont_h] compact_imp_closed by auto
+    qed
finally show "f ` {0..1} \<subseteq> h ` {0..1}" .
qed
moreover have "inj_on h {0..1}"
@@ -1394,8 +1379,7 @@
qed
have c_gt_0 [simp]: "0 < c(m / 2^n)" and c_less_1 [simp]: "c(m / 2^n) < 1" for m::nat and n
using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
-      using a_ge_0 [of m n] b_le_1 [of m n] apply linarith+
-      done
+      using a_ge_0 [of m n] b_le_1 [of m n] by linarith+
have approx: "\<exists>j n. odd j \<and> n \<noteq> 0 \<and>
real i / 2^m \<le> real j / 2^n \<and>
real j / 2^n \<le> real k / 2^p \<and>
@@ -1423,7 +1407,7 @@
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
-            have False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
+            have \<section>: False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
proof -
have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
using that by simp
@@ -1431,11 +1415,13 @@
using that by linarith
with that show ?thesis by simp
qed
-            then show ?thesis
+            moreover have *: "real i / 2 ^ m' < real k / 2^p'"  "k < 2 ^ p'"
+              using less.prems \<open>m = Suc m'\<close> 2 Suc by (force simp: field_split_simps)+
+            moreover have "i < 2 ^ m' "
+              using \<section> * by (clarsimp simp: divide_simps linorder_not_le) (meson linorder_not_le)
+            ultimately show ?thesis
using less.IH [of "m'+p'" i m' k p'] less.prems \<open>m = Suc m'\<close> 2 Suc
-              apply atomize
-              apply (force simp: field_split_simps)
-              done
+              by (force simp: field_split_simps)
qed
qed
next
@@ -1449,10 +1435,18 @@
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
-            then show ?thesis
+            have "real (i - 2 ^ m') / 2 ^ m' < real (k - 2 ^ p') / 2 ^ p'"
+              using less.prems \<open>m = Suc m'\<close> Suc 3  by (auto simp: field_simps of_nat_diff)
+            moreover have "k - 2 ^ p' < 2 ^ p'" "i - 2 ^ m' < 2 ^ m'"
+              using less.prems Suc \<open>m = Suc m'\<close> by auto
+            moreover
+            have "2 ^ p' \<le> k" "2 ^ p' \<noteq> k"
+              using less.prems \<open>m = Suc m'\<close> Suc 3 by auto
+            then have "2 ^ p' < k"
+              by linarith
+            ultimately show ?thesis
using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems \<open>m = Suc m'\<close> Suc 3
-              apply atomize
-              apply (auto simp: field_simps of_nat_diff)
+              apply (clarsimp simp: field_simps of_nat_diff)
apply (rule_tac x="2 ^ n + j" in exI, simp)
apply (rule_tac x="Suc n" in exI)
apply (auto simp: field_simps)
@@ -1476,15 +1470,10 @@
case True then show ?thesis by simp
next
case False
-        with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'"
-          by auto
-        have *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
-          by auto
-        have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
-          apply (rule ci_le_bj, force)
-          apply (rule * [OF less])
-          using i_le_j clo_ij q apply (auto simp: field_split_simps)
-          done
+        with i_le_j clo_ij q have "\<bar>real i / 2 ^ m - real (4 * q + 1) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+          by (auto simp: field_split_simps)
+        then have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
+          by (meson ci_le_bj even_mult_iff even_numeral even_plus_one_iff)
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1500,11 +1489,10 @@
by auto
have *: "\<lbrakk>q < i; abs(i - q) < s*2; r = q + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
by auto
-        have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
-          apply (rule aj_le_ci, force)
-          apply (rule * [OF less])
-          using j_le_j clo_jj q apply (auto simp: field_split_simps)
-          done
+        have "\<bar>real j / 2 ^ n - real (4 * q + 3) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+          by (rule * [OF less]) (use j_le_j clo_jj q  in \<open>auto simp: field_split_simps\<close>)
+        then have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] a43 [of n' q] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1611,15 +1599,13 @@
using m  by (auto simp: field_split_simps)
have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
-      have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
-        using \<open>0 < real m / 2 ^ n\<close> by linarith
+      have "2^n > m"
+        by (simp add: m(2) not_le)
+      then have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
+        using closure_dyadic_rationals_in_convex_set_pos_1 m_div(1) by fastforce
have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h"
if "0 \<le> u" "v \<le> 1" for u v
-        apply (rule continuous_on_subset [OF cont_h])
-        apply (rule closure_minimal [OF subsetI])
-        using that apply auto
-        done
+        using that by (intro continuous_on_subset [OF cont_h] closure_minimal [OF subsetI]) auto
have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v
by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
compact_imp_closed continuous_on_subset that)
@@ -1629,20 +1615,18 @@
proof clarsimp
fix p q
assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
-        then have [simp]: "0 < p" "p < 2 ^ q"
-          apply (blast intro: p less_2I m_div less_trans)
-          done
+        then have [simp]: "0 < p"
+        have [simp]: "p < 2 ^ q"
+          by (blast intro: p less_2I m_div less_trans)
have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}"
by (auto simp: clec p m)
then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}"
qed
-      then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
+      with m_div have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
apply (subst closure0m)
-        apply (rule image_closure_subset [OF cont_h' closed_f'])
-        using m_div apply auto
-        done
+        by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}"
using x12 less.prems(1) by auto
then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)"
@@ -1658,11 +1642,9 @@
then show "h (real p / 2 ^ q) \<in> f ` {c (real m / 2 ^ n)..1}"
qed
-      then have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
+      with m have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
apply (subst closurem1)
-        apply (rule image_closure_subset [OF cont_h' closed_f'])
-        using m apply auto
-        done
+        by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx2: "h x2 \<in> f ` {c(m / 2^n)..1}"
using x12 less.prems by auto
then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n) \<le> t2" "t2 \<le> 1"
@@ -1718,15 +1700,15 @@
by (metis uniformly_continuous_onE [OF ucont_p])
have minxy: "min e (y - x)  < (y - x) * (3 / 2)"
by (subst min_less_iff_disj) (simp add: less)
-        obtain w z where "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
+        define w where "w \<equiv> x + (min e (y - x) / 3)"
+        define z where "z \<equiv>y - (min e (y - x) / 3)"
+        have "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e"
-          apply (rule_tac w = "x + (min e (y - x) / 3)" and z = "y - (min e (y - x) / 3)" in that)
-          using minxy \<open>0 < e\<close> less by simp_all
+          using minxy \<open>0 < e\<close> less unfolding w_def z_def by auto
have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
-          using less w z apply (auto simp: open_segment_eq_real_ivl)
-          by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
+          using less w z by (simp add: open_segment_eq_real_ivl disjoint_iff)
then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
then have "K \<noteq> {}"
@@ -1752,8 +1734,7 @@
by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(1) less_eq_real_def w)
qed (auto simp: open_segment_eq_real_ivl intro!: that)
with False show thesis
-            apply (auto simp: disjoint_iff_not_equal intro!: that)
-            by (metis greaterThanLessThan_iff less_eq_real_def)
+            by (auto simp add: disjoint_iff less_eq_real_def intro!: that)
qed
obtain v where v: "v \<in> F n" "v \<in> {z..y}" "({z..v} - {v}) \<inter> F n = {}"
proof (cases "z \<in> F n")
@@ -1771,9 +1752,10 @@
show "F n \<inter> {z..y} \<noteq> {}"
by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> thesis"
-              apply (rule that)
-                apply (auto simp: open_segment_eq_real_ivl)
-              by (metis DiffI Int_iff atLeastAtMost_diff_ends atLeastAtMost_iff atLeastatMost_empty_iff empty_iff insert_iff False)
+            proof
+              show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> ({z..b} - {b}) \<inter> F n = {}"
+                using False by (auto simp: open_segment_eq_real_ivl less_eq_real_def)
+            qed auto
qed
qed
obtain u v where "u \<in> {0..1}" "v \<in> {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
@@ -1807,8 +1789,7 @@
qed
then show ?case
using e [of x u] e [of y v] xy
-          apply (simp add: open_segment_eq_real_ivl dist_norm del: divide_const_simps)
-          by (metis dist_norm dist_triangle_half_r less_irrefl)
+          by (metis dist_norm dist_triangle_half_r order_less_irrefl)
qed (auto simp: open_segment_commute)
show ?thesis
unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
@@ -1830,8 +1811,7 @@
have "insert x (open_segment x y \<union> open_segment x z) \<inter> T = {}"
by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
moreover have "open_segment y z \<inter> T \<subseteq> insert x (open_segment x y \<union> open_segment x z) \<inter> T"
-      apply auto
-      by (metis greaterThanLessThan_iff less_eq_real_def less_le_trans linorder_neqE_linordered_idom open_segment_eq_real_ivl)
+      by (auto simp: open_segment_eq_real_ivl)
ultimately have "open_segment y z \<inter> T = {}"
by blast
with that peq show ?thesis by metis
@@ -1877,13 +1857,21 @@
have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}"
using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int)
obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}"
-          apply (rule segment_to_point_exists [OF uvT, of u])
-          by (metis IntD1 Int_commute Int_left_commute ends_in_segment(1) inf.orderE subset_oc_segment)
+        proof (rule segment_to_point_exists [OF uvT])
+          fix b
+          assume "b \<in> closed_segment u v \<inter> T" "open_segment u b \<inter> (closed_segment u v \<inter> T) = {}"
+          then show thesis
+            by (metis IntD1 IntD2 ends_in_segment(1) inf.orderE inf_assoc subset_oc_segment that)
+        qed
then have puw: "dist (p u) (p w) < \<epsilon> / 2"
by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}"
-          apply (rule segment_to_point_exists [OF uvT, of v])
-          by (metis IntD2 Int_commute Int_left_commute ends_in_segment(2) inf.orderE subset_oc_segment)
+        proof (rule segment_to_point_exists [OF uvT])
+          fix b
+          assume "b \<in> closed_segment u v \<inter> T" "open_segment v b \<inter> (closed_segment u v \<inter> T) = {}"
+          then show thesis
+            by (metis IntD1 IntD2 ends_in_segment(2) inf.orderE inf_assoc subset_oc_segment that)
+        qed
then have "dist (p u) (p z) < \<epsilon> / 2"
by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
then show ?thesis
@@ -2048,11 +2036,10 @@
with y \<open>r > 0\<close>  obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r"
and g: "pathstart g = y" "pathfinish g = z"
using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
-  have "compact (g -` frontier S \<inter> {0..1})"
-    apply (simp add: compact_eq_bounded_closed bounded_Int)
-     apply (rule closed_vimage_Int)
-    using \<open>arc g\<close> apply (auto simp: arc_def path_def)
-    done
+  have "continuous_on {0..1} g"
+    using \<open>arc g\<close> arc_imp_path path_def by blast
+  then have "compact (g -` frontier S \<inter> {0..1})"
+    by (simp add: bounded_Int closed_Diff closed_vimage_Int compact_eq_bounded_closed)
moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}"
proof -
have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}"
@@ -2082,11 +2069,7 @@
then show "pathfinish (subpath 0 t g) \<in> V"
by auto
then have "inj_on (subpath 0 t g) {0..1}"
-      using t01
-      apply (clarsimp simp: inj_on_def subpath_def)
-      apply (drule inj_onD [OF arc_imp_inj_on [OF \<open>arc g\<close>]])
-      using mult_le_one apply auto
-      done
+      using t01 \<open>arc (subpath 0 t g)\<close> arc_imp_inj_on by blast
then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
by (force simp: dest: inj_onD)
moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}"
@@ -2096,11 +2079,10 @@
have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}"
proof (rule connected_Int_frontier [OF _ _ that])
show "connected (subpath 0 t g ` {0..<1})"
-          apply (rule connected_continuous_image)
-           apply (intro continuous_intros continuous_on_compose2 [OF contg])
-           apply (auto simp: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one)
-          done
+        proof (rule connected_continuous_image)
+          show "continuous_on {0..<1} (subpath 0 t g)"
+            by (meson \<open>arc (subpath 0 t g)\<close> arc_def atLeastLessThan_subseteq_atLeastAtMost_iff continuous_on_subset order_refl path_def)
+        qed auto
show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}"
using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def)
qed
@@ -2139,17 +2121,18 @@
by (simp add: \<open>arc g\<close> arc_imp_path)
then obtain h where "arc h"
and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
-    apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"])
-    using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto
-  have "h ` {0..1} - {h 1} \<subseteq> S"
-    using f g h apply (clarsimp simp: path_image_join)
+    using path_contains_arc [of "f +++ g" x "pathfinish g"] \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> f
+    by (metis pathfinish_join pathstart_join)
+  have "path_image h \<subseteq> path_image f \<union> path_image g"
+    using h(1) path_image_join_subset by auto
+  then have "h ` {0..1} - {h 1} \<subseteq> S"
+    using f g h
apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
by (metis le_less)
then have "h ` {0..<1} \<subseteq> S"
using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD)
then show thesis
-    apply (rule that [OF \<open>arc h\<close>])
-    using h \<open>pathfinish g \<in> V\<close> by auto
+    using \<open>arc h\<close> g(3) h that by presburger
qed

lemma dense_access_fp_aux:
@@ -2188,9 +2171,10 @@
proof
show "arc \<gamma>" "pathstart \<gamma> \<in> U" "pathfinish \<gamma> \<in> V"
using \<gamma> \<open>arc \<gamma>\<close> \<open>pathfinish h \<in> U - {pathfinish g}\<close>  \<open>pathfinish g \<in> V\<close> by auto
-    have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
-      using \<gamma> g h
+    have "path_image \<gamma> \<subseteq> path_image h \<union> path_image g"
+      by (metis \<gamma>(1) g(2) h(2) path_image_join path_image_reversepath pathfinish_reversepath)
+    then have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
+      using \<gamma> g h
apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
by (metis linorder_neqE_linordered_idom not_less)
then show "\<gamma> ` {0<..<1} \<subseteq> S"```
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Oct 31 21:06:29 2020 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Oct 31 21:24:40 2020 +0000
@@ -14,6 +14,10 @@
Cartesian_Euclidean_Space
begin

+lemma LIMSEQ_if_less: "(\<lambda>k. if i < k then a else b) \<longlonglongrightarrow> a"
+  by (rule_tac k="Suc i" in LIMSEQ_offset) auto
+
+text \<open>Note that the rhs is an implication. This lemma plays a specific role in one proof.\<close>
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
by (auto intro: order_trans)

@@ -227,8 +231,8 @@
also have "\<dots> = ?\<mu> E - ?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})"
using \<open>E \<in> sets ?L\<close> fin[of X] sets[of X] by (auto intro!: emeasure_Diff)
finally have "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}}) \<le> e"
-          using \<open>0 < e\<close> e_less_M apply (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})")
-          by (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
+          using \<open>0 < e\<close> e_less_M
+          by (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})") (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
note this }
note upper_bound = this

@@ -345,12 +349,8 @@
proof cases
assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
then show ?thesis
-        apply simp
-        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
-        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
using has_integral_const[of "1::real" l u]
-        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
-        done
+        by (simp flip: has_integral_restrict[OF box_subset_cbox] add: has_integral_spike_interior)
next
assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
then have "box l u = {}"
@@ -405,11 +405,8 @@
by (intro sum_mono2) auto
from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
-        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)"
-          apply (auto simp: * sum.If_cases Iio_Int_singleton)
-          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
-          apply simp
-          done
+        show "(\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)" for x
+          by (auto simp: * sum.If_cases Iio_Int_singleton if_distrib LIMSEQ_if_less cong: if_cong)
have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
by (intro emeasure_mono) auto

@@ -486,14 +483,8 @@
case (seq U)
note seq(1)[measurable] and f[measurable]

-  { fix i x
-    have "U i x \<le> f x"
-      using seq(5)
-      apply (rule LIMSEQ_le_const)
-      using seq(4)
-      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
-      done }
-  note U_le_f = this
+  have U_le_f: "U i x \<le> f x" for i x
+    by (metis (no_types) LIMSEQ_le_const UNIV_I incseq_def le_fun_def seq.hyps(4) seq.hyps(5) space_borel)

{ fix i
have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
@@ -910,9 +901,7 @@
using assms has_integral_integral_lborel
unfolding set_integrable_def set_lebesgue_integral_def by blast
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
-    apply (subst has_integral_restrict_UNIV [symmetric])
-    apply (rule has_integral_eq)
-    by auto
thus "f integrable_on S"
with 1 have "(f has_integral (integral S f)) S"
@@ -1088,8 +1077,8 @@
lemma absolutely_integrable_reflect[simp]:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "(\<lambda>x. f(-x)) absolutely_integrable_on cbox (-b) (-a) \<longleftrightarrow> f absolutely_integrable_on cbox a b"
-  apply (auto simp: absolutely_integrable_on_def dest: integrable_reflect [THEN iffD1])
-  unfolding integrable_on_def by auto
+  unfolding absolutely_integrable_on_def
+  by (metis (mono_tags, lifting) integrable_eq integrable_reflect)

lemma absolutely_integrable_reflect_real[simp]:
fixes f :: "real \<Rightarrow> 'b::euclidean_space"
@@ -1168,15 +1157,16 @@
proof -
have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
by (meson indicator_def)
-  moreover
-  have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
+  moreover have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
using assms by (simp add: lmeasurable_iff_has_integral)
ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
by (metis (no_types) integral_unique)
-  then show ?thesis
-    using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
-    apply (simp add: integral_restrict_Int [symmetric])
+  moreover have "integral T (\<lambda>a. if a \<in> S then 1::real else 0) = integral (S \<inter> T \<inter> UNIV) (\<lambda>a. 1)"
+  moreover have "integral T (indicat_real S) = integral T (\<lambda>a. if a \<in> S then 1 else 0)"
by (meson indicator_def)
+  ultimately show ?thesis
+    by (simp add: assms lmeasure_integral)
qed

lemma measurable_integrable:
@@ -1234,9 +1224,8 @@
by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
next
assume RHS [rule_format]: ?rhs
-  show ?lhs
+  then show ?lhs
apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
-    using RHS
by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
qed

@@ -1305,14 +1294,13 @@
assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
proof -
obtain x where x: "a \<bullet> x \<noteq> b"
-    using assms
-    apply auto
-     apply (metis inner_eq_zero_iff inner_zero_right)
-    using inner_zero_right by fastforce
+    using assms by (metis euclidean_all_zero_iff inner_zero_right)
+  moreover have "c = 1" if "a \<bullet> (x + c *\<^sub>R w) = b" "a \<bullet> (x + w) = b" for c w
+    using that
+    by (metis (no_types, hide_lams) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
+  ultimately
show ?thesis
-    apply (rule starlike_negligible [OF closed_hyperplane, of x])
-    using x apply (auto simp: algebra_simps)
-    done
+    using starlike_negligible [OF closed_hyperplane, of x] by simp
qed

lemma negligible_lowdim:
@@ -1348,12 +1336,15 @@
next
case 2
-      obtain a where a: "a \<in> interior S"
-        apply (rule interior_simplex_nonempty [OF indB])
-          apply (simp add: indB independent_finite)
-         apply (simp add: cardB 2)
-        apply (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
-        done
+      obtain a where "a \<in> interior (convex hull insert 0 B)"
+      proof (rule interior_simplex_nonempty [OF indB])
+        show "finite B"
+          by (simp add: indB independent_finite)
+        show "card B = DIM('N)"
+          by (simp add: cardB 2)
+      qed
+      then have a: "a \<in> interior S"
+        by (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
show ?thesis
proof (rule starlike_negligible_strong [where a=a])
fix c::real and x
@@ -1361,10 +1352,9 @@
assume "0 \<le> c" "c < 1" "a + x \<in> frontier S"
then show "a + c *\<^sub>R x \<notin> frontier S"
-          apply (clarsimp simp: frontier_def)
-          apply (subst eq)
-          apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"], auto)
-          done
+          using eq mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"]
+          unfolding frontier_def
qed auto
qed
qed
@@ -1426,10 +1416,7 @@

lemma negligible_convex_interior:
"convex S \<Longrightarrow> (negligible S \<longleftrightarrow> interior S = {})"
-  apply safe
-  apply (metis interior_subset negligible_subset open_interior open_not_negligible)
-   apply (metis Diff_empty closure_subset frontier_def negligible_convex_frontier negligible_subset)
-  done
+  by (metis Diff_empty closure_subset frontier_def interior_subset negligible_convex_frontier negligible_subset open_interior open_not_negligible)

lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
by (auto simp: measure_def null_sets_def)
@@ -1441,8 +1428,7 @@
by (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)

lemma negligible_iff_measure0: "S \<in> lmeasurable \<Longrightarrow> (negligible S \<longleftrightarrow> measure lebesgue S = 0)"
-  apply (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
-  by (metis completion.null_sets_outer subsetI)
+  by (metis (full_types) completion.null_sets_outer negligible_iff_null_sets negligible_imp_measure0 order_refl)

lemma negligible_imp_sets: "negligible S \<Longrightarrow> S \<in> sets lebesgue"
@@ -1474,12 +1460,7 @@
qed

lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
-proof
-  assume ?rhs
-  then show "negligible S"
-    apply (auto simp: negligible_def has_integral_iff integrable_on_indicator)
-    by (metis negligible integral_unique lmeasure_integral_UNIV negligible_iff_measure0)
+  by (metis lmeasurable_iff_indicator_has_integral negligible_iff_measure)

lemma sets_negligible_symdiff:
"\<lbrakk>S \<in> sets lebesgue; negligible((S - T) \<union> (T - S))\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
@@ -1688,11 +1669,7 @@
then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
then show ?thesis
-      apply (rule_tac x="min (1/2) \<epsilon>" in exI)
-      apply (simp del: divide_const_simps)
-      apply (intro allI impI conjI)
-       apply (metis dist_commute dist_norm mem_ball subsetCE)
-      by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
+      by (rule_tac x="min (1/2) \<epsilon>" in exI) (simp add: U dist_norm norm_minus_commute subset_iff)
next
case False
then show ?thesis
@@ -1709,10 +1686,13 @@
obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
using \<open>bounded S\<close> bounded_iff by blast
show ?thesis
-      apply (rule_tac c = "abs B + 1" in that)
-      using norm_bound_Basis_le Basis_le_norm
-       apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
-      done
+    proof (rule_tac c = "abs B + 1" in that)
+      show "S \<subseteq> cbox (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One)"
+        using norm_bound_Basis_le Basis_le_norm
+        by (fastforce simp: mem_box dest!: B intro: order_trans)
+      show "box (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One) \<noteq> {}"
+    qed
qed
obtain \<D> where "countable \<D>"
and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
@@ -1728,10 +1708,7 @@
obtain u v where "K = cbox u v"
using \<open>K \<in> \<D>\<close> cbox by blast
with that show ?thesis
-      apply (rule_tac x=u in exI)
-      apply (rule_tac x=v in exI)
-      apply (metis Int_iff interior_cbox cbox Ksub)
-      done
+      by (metis Int_iff interior_cbox cbox Ksub)
qed
then obtain uf vf zf
where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
@@ -1771,8 +1748,7 @@
have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
by (rule prod_constant [symmetric])
also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
-        apply (rule prod.cong [OF refl])
-        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
+        by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem cong: prod.cong)
finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
@@ -1788,11 +1764,9 @@
have 0: "0 \<le> prj1 (vf X - uf X)"
using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
-        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close>)
-        apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
+        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> \<open>0 < B\<close> flip: prj1_eq)
using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
-        apply (fastforce simp add: box_ne_empty power_decreasing)
-        done
+        by (fastforce simp add: box_ne_empty power_decreasing)
also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
by (subst (3) ufvf[symmetric]) simp
finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
@@ -1801,11 +1775,11 @@
also have "\<dots> \<le> e/2"
proof -
-      have div: "\<D>' division_of \<Union>\<D>'"
-        apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
-        using cbox that apply blast
-        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
-        done
+      have "\<And>K. K \<in> \<D>' \<Longrightarrow> \<exists>a b. K = cbox a b"
+        using cbox that by blast
+      then have div: "\<D>' division_of \<Union>\<D>'"
+        using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def
+        by (force simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
proof (rule measure_mono_fmeasurable)
show "(\<Union>\<D>') \<in> sets lebesgue"
@@ -1830,10 +1804,8 @@
(2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
using content_division [OF div] by auto
also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
-        apply (rule mult_left_mono [OF le_meaT])
-        using \<open>0 < B\<close>
-        done
+        using \<open>0 < B\<close>
+        by (intro mult_left_mono [OF le_meaT]) (force simp add: algebra_simps)
also have "\<dots> \<le> e/2"
using T \<open>0 < B\<close> by (simp add: field_simps)
finally show ?thesis .
@@ -1924,12 +1896,10 @@
then show ?thesis
using B order_trans that by blast
qed
-    have "x \<in> ?S (nat (ceiling (max B (norm x))))"
-      apply (simp add: \<open>x \<in> S \<close>, rule)
-      using real_nat_ceiling_ge max.bounded_iff apply blast
-      using T no
-      apply (force simp: algebra_simps)
-      done
+    have "norm x \<le> real (nat \<lceil>max B (norm x)\<rceil>)"
+      by linarith
+    then have "x \<in> ?S (nat (ceiling (max B (norm x))))"
+      using T no by (force simp: \<open>x \<in> S\<close> algebra_simps)
then show "x \<in> (\<Union>n. ?S n)" by force
qed auto
then show ?thesis
@@ -1946,9 +1916,9 @@
if "x \<in> S" for x
proof -
obtain f' where "linear f'"
-      and f': "\<And>e. e>0 \<Longrightarrow>
-                  \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
-                              norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
+       and f': "\<And>e. e>0 \<Longrightarrow>
+                        \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
+                                    norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
using diff_f \<open>x \<in> S\<close>
by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
@@ -1957,24 +1927,21 @@
and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
using f' [of 1] by (force simp:)
-    have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
-              if "y \<in> S" "norm (y - x) < d" for y
-    proof -
-      have "norm (f y - f x) -B *  norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
-      also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
-        by (rule norm_triangle_ineq2)
-      also have "... \<le> norm (y - x)"
-        by (rule d [OF that])
-      finally show ?thesis
-    qed
show ?thesis
-      apply (rule_tac x="ball x d" in exI)
-      apply (rule_tac x="B+1" in exI)
-      using \<open>d>0\<close>
-      apply (auto simp: dist_norm norm_minus_commute intro!: *)
-      done
+    proof (intro exI conjI ballI)
+      show "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
+        if "y \<in> S \<inter> ball x d" for y
+      proof -
+        have "norm (f y - f x) - B * norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
+        also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
+          by (rule norm_triangle_ineq2)
+        also have "... \<le> norm (y - x)"
+          by (metis IntE d dist_norm mem_ball norm_minus_commute that)
+        finally show ?thesis
+      qed
+    qed (use \<open>d>0\<close> in auto)
qed
with negligible_locally_Lipschitz_image assms show ?thesis by metis
qed
@@ -1990,25 +1957,28 @@
where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
using lowerdim_embeddings [OF MlessN] by metis
-  have "negligible {x. x\<bullet>j = 0}"
-    by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
-  then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
-    apply (rule negligible_subset)
-    by (simp add: image_subsetI j)
-  have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
+  have "negligible ((\<lambda>x. lift (x, 0)) ` S)"
+  proof -
+    have "negligible {x. x\<bullet>j = 0}"
+      by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
+    moreover have "(\<lambda>m. lift (m, 0)) ` S \<subseteq> {n. n \<bullet> j = 0}"
+      using j by force
+    ultimately show ?thesis
+      using negligible_subset by auto
+  qed
+  moreover
+  have "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
using diff_f
apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
linear_imp_differentiable [OF linear_fst])
apply (force simp: image_comp o_def)
done
-  have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
+  moreover
+  have "f = f \<circ> fst \<circ> drop \<circ> (\<lambda>x. lift (x, 0))"
-  then show ?thesis
-    apply (rule ssubst)
-    apply (subst image_comp [symmetric])
-    apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
-    done
+  ultimately show ?thesis
+    by (metis (no_types) image_comp negligible_differentiable_image_negligible order_refl)
qed

subsection\<open>Measurability of countable unions and intersections of various kinds.\<close>
@@ -2020,21 +1990,24 @@
shows measurable_nested_Union: "(\<Union>n. S n) \<in> lmeasurable"
and measure_nested_Union:  "(\<lambda>n. measure lebesgue (S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. S n)" (is ?Lim)
proof -
-  have 1: "\<And>n. (indicat_real (S n)) integrable_on UNIV"
-    using S measurable_integrable by blast
-  have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
-    by (simp add: indicator_leI nest rev_subsetD)
-  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
-    apply (rule tendsto_eventually)
-    by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
-  have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
-    using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
-  have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
-    apply (simp add: lmeasure_integral_UNIV S cong: conj_cong)
-    apply (rule monotone_convergence_increasing [OF 1 2 3 4])
-    done
+  have "indicat_real (\<Union> (range S)) integrable_on UNIV \<and>
+    (\<lambda>n. integral UNIV (indicat_real (S n)))
+    \<longlonglongrightarrow> integral UNIV (indicat_real (\<Union> (range S)))"
+  proof (rule monotone_convergence_increasing)
+    show "\<And>n. (indicat_real (S n)) integrable_on UNIV"
+      using S measurable_integrable by blast
+    show "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
+      by (simp add: indicator_leI nest rev_subsetD)
+    have "\<And>x. (\<exists>n. x \<in> S n) \<longrightarrow> (\<forall>\<^sub>F n in sequentially. x \<in> S n)"
+      by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
+    then
+    show "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
+      by (simp add: indicator_def tendsto_eventually)
+    show "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
+      using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
+  qed
+  then have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
then show "(\<Union>n. S n) \<in> lmeasurable" "?Lim"
by auto
qed
@@ -2094,8 +2067,9 @@
using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
by (metis S finite_atMost subset_UNIV)
also have "\<dots> \<le> measure lebesgue (cbox a b)"
-      apply (rule measure_mono_fmeasurable)
-      using ab S by force+
+    proof (rule measure_mono_fmeasurable)
+      show "\<Union> (S ` {..n}) \<in> sets lebesgue" using S by blast
+    qed (use ab in auto)
finally show ?thesis .
qed
show "(\<Union>n. S n) \<in> lmeasurable"
@@ -2167,12 +2141,9 @@
using negligible_subset by blast
qed

-lemma locally_negligible:
-     "locally negligible S \<longleftrightarrow> negligible S"
+lemma locally_negligible: "locally negligible S \<longleftrightarrow> negligible S"
unfolding locally_def
-  apply safe
-   apply (meson negligible_subset openin_subtopology_self locally_negligible_alt)
-  by (meson negligible_subset openin_imp_subset order_refl)
+  by (metis locally_negligible_alt negligible_subset openin_imp_subset openin_subtopology_self)

subsection\<open>Integral bounds\<close>
@@ -2237,15 +2208,17 @@
qed

lemma absdiff_norm_less:
-  assumes "sum (\<lambda>x. norm (f x - g x)) s < e"
-    and "finite s"
-  shows "\<bar>sum (\<lambda>x. norm(f x)) s - sum (\<lambda>x. norm(g x)) s\<bar> < e"
-  unfolding sum_subtractf[symmetric]
-  apply (rule le_less_trans[OF sum_abs])
-  apply (rule le_less_trans[OF _ assms(1)])
-  apply (rule sum_mono)
-  apply (rule norm_triangle_ineq3)
-  done
+  assumes "sum (\<lambda>x. norm (f x - g x)) S < e"
+  shows "\<bar>sum (\<lambda>x. norm(f x)) S - sum (\<lambda>x. norm(g x)) S\<bar> < e" (is "?lhs < e")
+proof -
+  have "?lhs \<le> (\<Sum>i\<in>S. \<bar>norm (f i) - norm (g i)\<bar>)"
+    by (metis (no_types) sum_abs sum_subtractf)
+  also have "... \<le> (\<Sum>x\<in>S. norm (f x - g x))"
+    by (simp add: norm_triangle_ineq3 sum_mono)
+  also have "... < e"
+    using assms(1) by blast
+  finally show ?thesis .
+qed

proposition bounded_variation_absolutely_integrable_interval:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
@@ -2344,17 +2317,6 @@
next
have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
unfolding p'_def using d' by blast
-        have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
-        proof -
-          obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
-            using y unfolding p'(6)[symmetric] by auto
-          obtain i where i: "i \<in> d" "y \<in> i"
-            using y unfolding d'(6)[symmetric] by auto
-          have "x \<in> i"
-            using fineD[OF p(3) xl(1)] using k(2) i xl by auto
-          then show ?thesis
-            unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
-        qed
show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
proof
show "\<Union>{k. \<exists>x. (x, k) \<in> p'} \<subseteq> cbox a b"
@@ -2370,17 +2332,24 @@
using y unfolding d'(6)[symmetric] by auto
have "x \<in> I"
using fineD[OF p(3) xl(1)] using k(2) i xl by auto
-            then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
-              apply (rule_tac X="I \<inter> L" in UnionI)
-              using i xl by (auto simp: p'_def)
+            then show "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}"
+            proof -
+              obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
+                using y unfolding p'(6)[symmetric] by auto
+              obtain i where i: "i \<in> d" "y \<in> i"
+                using y unfolding d'(6)[symmetric] by auto
+              have "x \<in> i"
+                using fineD[OF p(3) xl(1)] using k(2) i xl by auto
+              then show ?thesis
+                unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+            qed
qed
qed
qed
-
then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
using g(2) gp' tagged_division_of_def by blast

-      have "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
+      have in_p': "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
for x I L y
proof -
have "x \<in> I"
@@ -2391,7 +2360,8 @@
with y show ?thesis by auto
qed
-      moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+      moreover
+      have Ex_p_p': "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
if xK: "(x,K) \<in> p'" for x K
proof -
obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
@@ -2402,9 +2372,10 @@
ultimately have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
by auto
have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
-        apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
-         apply (auto intro: integral_null simp: content_eq_0_interior)
-        done
+      proof (rule sum.over_tagged_division_lemma[OF p''])
+        show "\<And>u v. box u v = {} \<Longrightarrow> norm (integral (cbox u v) f) = 0"
+          by (auto intro: integral_null simp: content_eq_0_interior)
+      qed
have snd_p_div: "snd ` p division_of cbox a b"
by (rule division_of_tagged_division[OF p(1)])
note snd_p = division_ofD[OF snd_p_div]
@@ -2432,28 +2403,30 @@
define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
have uvab: "cbox u v \<subseteq> cbox a b"
using d(1) k uv by blast
-            have "d' division_of cbox u v"
+            have d'_div: "d' division_of cbox u v"
unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
-            moreover then have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+            moreover have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+            moreover have "f integrable_on K"
+              using f integrable_on_subcbox uv uvab by blast
+            moreover have "d' division_of K"
+              using d'_div uv by blast
ultimately have "norm (integral K f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
-              apply (subst integral_combine_division_topdown[of _ _ d'])
-                apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab])
-              done
also have "\<dots> = (\<Sum>I\<in>{K \<inter> L |L. L \<in> snd ` p}. norm (integral I f))"
-            proof -
-              have *: "norm (integral I f) = 0"
-                if "I \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-                  "I \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for I
-                using that by auto
-              show ?thesis
-                apply (rule sum.mono_neutral_left)
-                unfolding d'_def uv using * by auto
+            proof (rule sum.mono_neutral_left)
+              show "finite {K \<inter> L |L. L \<in> snd ` p}"
+              show "\<forall>i\<in>{K \<inter> L |L. L \<in> snd ` p} - d'. norm (integral i f) = 0"
+                "d' \<subseteq> {K \<inter> L |L. L \<in> snd ` p}"
+                using d'_def image_eqI uv by auto
qed
also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
-            proof -
-              have *: "norm (integral (K \<inter> l) f) = 0"
+              unfolding Setcompr_eq_image
+            proof (rule sum.reindex_nontrivial [unfolded o_def])
+              show "finite (snd ` p)"
+                using snd_p(1) by blast
+              show "norm (integral (K \<inter> l) f) = 0"
if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "K \<inter> l = K \<inter> y" for l y
proof -
have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
@@ -2468,12 +2441,6 @@
unfolding uv Int_interval content_eq_0_interior
by (metis (mono_tags, lifting) norm_eq_zero)
qed
-              show ?thesis
-                unfolding Setcompr_eq_image
-                apply (rule sum.reindex_nontrivial [unfolded o_def])
-                 apply (rule finite_imageI)
-                 apply (rule p')
-                using * by auto
qed
finally show "norm (integral K f) \<le> (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))" .
qed
@@ -2485,7 +2452,7 @@
proof -
have eq0: " (integral (l1 \<inter> k1) f) = 0"
if "l1 \<inter> k1 = l2 \<inter> k2" "(l1, k1) \<noteq> (l2, k2)"
-                "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
+                 "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
for l1 l2 k1 k2 j1 j2
proof -
obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
@@ -2508,26 +2475,14 @@
by (metis eq0 fst_conv snd_conv)
qed
also have "\<dots> = (\<Sum>(x,k) \<in> p'. norm (integral k f))"
-          proof -
-            have 0: "integral (ia \<inter> snd (a, b)) f = 0"
-              if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for ia a b
-            proof -
-              have "ia \<inter> b = {}"
-                using that unfolding p'alt image_iff Bex_def not_ex
-                apply (erule_tac x="(a, ia \<inter> b)" in allE)
-                apply auto
-                done
-              then show ?thesis by auto
-            qed
-            have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
-              using that
-              apply (clarsimp simp: p'_def image_iff)
-              by (metis (no_types, hide_lams) snd_conv)
-            show ?thesis
-              unfolding sum_p'
-              apply (rule sum.mono_neutral_right)
-                apply (metis * finite_imageI[OF fin_d_sndp])
-              using 0 1 by auto
+            unfolding sum_p'
+          proof (rule sum.mono_neutral_right)
+            show "finite {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+              by (metis * finite_imageI[OF fin_d_sndp])
+            show "snd ` p' \<subseteq> {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+              by (clarsimp simp: p'_def) (metis image_eqI snd_conv)
+            show "\<forall>i\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p} - snd ` p'. norm (integral i f) = 0"
+              by clarsimp (metis Henstock_Kurzweil_Integration.integral_empty disjoint_iff image_eqI in_p' snd_conv)
qed
finally show ?thesis .
qed
@@ -2540,11 +2495,10 @@
using finite_cartesian_product[OF p'(1) d'(1)] by metis
have "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> ?S. \<bar>content k\<bar> * norm (f x))"
unfolding norm_scaleR
-            apply (rule sum.mono_neutral_left)
-              apply (subst *)
-              apply (rule finite_imageI [OF fin_pd])
-            unfolding p'alt apply auto
-            by fastforce
+          proof (rule sum.mono_neutral_left)
+            show "finite {(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+              by (simp add: "*" fin_pd)
+          qed (use p'alt in \<open>force+\<close>)
also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
proof -
have "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
@@ -2557,8 +2511,7 @@
have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
using that by auto
then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-                apply (rule disjE)
-                using that p'(5) d'(5) by auto
+                using that p'(5) d'(5) by (metis snd_conv)
moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
unfolding that ..
ultimately have "interior (l1 \<inter> k1) = {}"
@@ -2570,8 +2523,7 @@
unfolding *
apply (subst sum.reindex_nontrivial [OF fin_pd])
unfolding split_paired_all o_def split_def prod.inject
-               apply force+
-              done
+              by force+
qed
also have "\<dots> = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
proof -
@@ -2601,20 +2553,17 @@
qed
then show ?thesis
unfolding Setcompr_eq_image
-                  apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
-                  by auto
+                  by (fastforce intro: sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
qed
also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
-                apply (rule sum.mono_neutral_right)
-                unfolding Setcompr_eq_image
-                  apply (rule finite_imageI [OF \<open>finite d\<close>])
-                 apply (fastforce simp: inf.commute)+
-                done
-              finally show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
-                unfolding sum_distrib_right[symmetric] real_scaleR_def
-                apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
-                using xl(2)[unfolded uv] unfolding uv apply auto
-                done
+              proof (rule sum.mono_neutral_right)
+                show "finite {k \<inter> cbox u v |k. k \<in> d}"
+              qed (fastforce simp: inf.commute)+
+              finally have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = content (cbox u v)"
+                using additive_content_division[OF division_inter_1[OF d(1)]] uv xl(2) by auto
+              then show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+                unfolding sum_distrib_right[symmetric] using uv by auto
qed
show ?thesis
by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
@@ -2636,66 +2585,55 @@
and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> sum (\<lambda>k. norm (integral k f)) d \<le> B"
shows "f absolutely_integrable_on UNIV"
proof (rule absolutely_integrable_onI, fact)
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
+  let ?f = "\<lambda>D. \<Sum>k\<in>D. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
+  define SDF where "SDF \<equiv> SUP d\<in>?D. ?f d"
have D_1: "?D \<noteq> {}"
by (rule elementary_interval) auto
have D_2: "bdd_above (?f`?D)"
-    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
-  note D = D_1 D_2
-  let ?S = "SUP d\<in>?D. ?f d"
-  have "\<And>a b. f integrable_on cbox a b"
-    using assms(1) integrable_on_subcbox by blast
-  then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
-    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
-    using assms(2) apply blast
-    done
-  have "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
-    apply (subst has_integral_alt')
-    apply safe
-  proof goal_cases
-    case (1 a b)
-    show ?case
-      using f_int[of a b] unfolding absolutely_integrable_on_def by auto
-  next
-    case prems: (2 e)
-    have "\<exists>y\<in>sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
+    using assms(2) by auto
+  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
+    using assms integrable_on_subcbox
+    by (blast intro!: bounded_variation_absolutely_integrable_interval)
+  have "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
+                    \<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
+    if "0 < e" for e
+  proof -
+    have "\<exists>y \<in> ?f ` ?D. \<not> y \<le> SDF - e"
proof (rule ccontr)
assume "\<not> ?thesis"
-      then have "?S \<le> ?S - e"
-        by (intro cSUP_least[OF D(1)]) auto
+      then have "SDF \<le> SDF - e"
+        unfolding SDF_def
+        by (metis (mono_tags) D_1 cSUP_least image_eqI)
then show False
-        using prems by auto
+        using that by auto
qed
-    then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
-      "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
+    then obtain d K where ddiv: "d division_of \<Union>d" and "K = ?f d" "SDF - e < K"
by (auto simp add: image_iff not_le)
-    then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
-                  < (\<Sum>k\<in>d. norm (integral k f))"
+    then have d: "SDF - e < ?f d"
by auto
note d'=division_ofD[OF ddiv]
have "bounded (\<Union>d)"
-      by (rule elementary_bounded,fact)
-    from this[unfolded bounded_pos] obtain K where
-       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
-    show ?case
+      using ddiv by blast
+    then obtain K where K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K"
+      using bounded_pos by blast
+    show ?thesis
proof (intro conjI impI allI exI)
fix a b :: 'n
assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
-      have *: "\<And>s s1. \<lbrakk>?S - e < s1; s1 \<le> s; s < ?S + e\<rbrakk> \<Longrightarrow> \<bar>s - ?S\<bar> < e"
+      have *: "\<And>s s1. \<lbrakk>SDF - e < s1; s1 \<le> s; s < SDF + e\<rbrakk> \<Longrightarrow> \<bar>s - SDF\<bar> < e"
by arith
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
+      show "\<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
unfolding real_norm_def
proof (rule * [OF d])
-        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
+        have "?f d \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
proof (intro sum_mono)
fix k assume "k \<in> d"
with d'(4) f_int show "norm (integral k f) \<le> integral k (\<lambda>x. norm (f x))"
by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
qed
also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
-          apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
-          using absolutely_integrable_on_def d'(4) f_int by blast
-        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
+          by (metis (full_types) absolutely_integrable_on_def d'(4) ddiv f_int integral_combine_division_bottomup)
+        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. norm (f x))"
proof -
have "\<Union>d \<subseteq> cbox a b"
using K(2) ab by fastforce
@@ -2703,8 +2641,7 @@
using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
by (auto intro!: integral_subset_le)
qed
-        finally show "(\<Sum>k\<in>d. norm (integral k f))
-                      \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" .
+        finally show "?f d \<le> integral (cbox a b) (\<lambda>x. norm (f x))" .
next
have "e/2>0"
using \<open>e > 0\<close> by auto
@@ -2723,31 +2660,39 @@
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
-        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;
-                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> SDF; \<bar>sf - si\<bar> < e/2;
+                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < SDF + e"
by arith
-        have "integral (cbox a b) (\<lambda>x. norm (f x)) < ?S + e"
+        have "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
proof (rule *)
show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
unfolding split_def
-            apply (rule absdiff_norm_less)
-            using d2[of p] p(1,3) apply (auto simp: tagged_division_of_def split_def)
-            done
+          proof (rule absdiff_norm_less)
+            show "(\<Sum>p\<in>p. norm (content (snd p) *\<^sub>R f (fst p) - integral (snd p) f)) < e/2"
+              using d2[of p] p(1,3) by (auto simp: tagged_division_of_def split_def)
+          qed
show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
using d1[OF p(1,2)] by (simp only: real_norm_def)
show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
by (auto simp: split_paired_all sum.cong [OF refl])
-          show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
+          have "(\<Sum>(x,k) \<in> p. norm (integral k f)) = (\<Sum>k\<in>snd ` p. norm (integral k f))"
+            apply (rule sum.over_tagged_division_lemma[OF p(1)])
+            by (metis Henstock_Kurzweil_Integration.integral_empty integral_open_interval norm_zero)
+          also have "... \<le> SDF"
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
-            apply (subst sum.over_tagged_division_lemma[OF p(1)])
-            apply (auto simp: content_eq_0_interior tagged_partial_division_of_def intro!: cSUP_upper2 D)
-            done
+            by (auto simp: SDF_def tagged_partial_division_of_def intro!: cSUP_upper2 D_1 D_2)
+          finally show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> SDF" .
qed
-        then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+        then show "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
by simp
qed
-    qed (insert K, auto)
+    qed (use K in auto)
qed
+  moreover have "\<And>a b. (\<lambda>x. norm (f x)) integrable_on cbox a b"
+    using absolutely_integrable_on_def f_int by auto
+  ultimately
+  have "((\<lambda>x. norm (f x)) has_integral SDF) UNIV"
+    by (auto simp: has_integral_alt')
then show "(\<lambda>x. norm (f x)) integrable_on UNIV"
by blast
qed
@@ -2844,10 +2789,13 @@
have "?\<mu> (\<Union>\<F>) \<le> ?\<mu> S + e"
proof (rule *)
have "(\<Sum>K\<in>\<F>. ?\<mu> (K \<inter> S)) = ?\<mu> (\<Union>C\<in>\<F>. C \<inter> S)"
-          apply (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
-          using \<F>div \<open>S \<in> lmeasurable\<close> apply blast
-          unfolding pairwise_def
-          by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+        proof (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
+          show "\<And>K. K \<in> \<F> \<Longrightarrow> K \<inter> S \<in> lmeasurable"
+            using \<F>div \<open>S \<in> lmeasurable\<close> by blast
+          show "pairwise (\<lambda>K y. negligible (K \<inter> S \<inter> (y \<inter> S))) \<F>"
+            unfolding pairwise_def
+            by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+        qed
also have "\<dots> = ?\<mu> (\<Union>\<F> \<inter> S)"
by simp
also have "\<dots> \<le> ?\<mu> S"
@@ -3007,8 +2955,7 @@
by (metis True empty_imp_negligible image_Int image_empty interior_Int interior_injective_linear_image that(1))
qed
moreover have "g ` K \<inter> g ` L \<subseteq> frontier (g ` K \<inter> g ` L) \<union> interior (g ` K \<inter> g ` L)"
-            apply (auto simp: frontier_def)
-            using closure_subset contra_subsetD by fastforce+
+            by (metis Diff_partition Int_commute calculation closure_Un_frontier frontier_def inf.absorb_iff2 inf_bot_right inf_sup_absorb negligible_Un_eq open_interior open_not_negligible sup_commute)
ultimately show ?thesis
by (rule negligible_subset)
next
@@ -3090,8 +3037,6 @@
and DD: "cbox a b - S \<subseteq> \<Union>\<D>" "\<Union>\<D> \<in> lmeasurable"
and le: "?\<mu> (\<Union>\<D>) \<le> ?\<mu> (cbox a b - S) + e/(1 + \<bar>m\<bar>)"
by (rule measurable_outer_intervals_bounded [of "cbox a b - S" a b "e/(1 + \<bar>m\<bar>)"]; use 1 2 pairwise_def in force)
-        have meq: "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
-          by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
show "\<exists>T \<in> lmeasurable. T \<subseteq> f ` S \<and> m * ?\<mu> S - e \<le> ?\<mu> T"
proof (intro bexI conjI)
show "f ` (cbox a b) - f ` (\<Union>\<D>) \<subseteq> f ` S"
@@ -3099,16 +3044,24 @@
have "m * ?\<mu> S - e \<le> m * (?\<mu> S - e / (1 + \<bar>m\<bar>))"
using \<open>m \<ge> 0\<close> \<open>e > 0\<close> by (simp add: field_simps)
also have "\<dots> \<le> ?\<mu> (f ` cbox a b) - ?\<mu> (f ` (\<Union>\<D>))"
-            using le \<open>m \<ge> 0\<close> \<open>e > 0\<close>
-            apply (simp add: im fUD [OF \<open>countable \<D>\<close> cbox intdisj] right_diff_distrib [symmetric])
-            apply (rule mult_left_mono; simp add: algebra_simps meq)
-            done
+          proof -
+            have "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
+              by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
+            then have "(?\<mu> S - e / (1 + m)) \<le> (content (cbox a b) - ?\<mu> (\<Union> \<D>))"
+              using \<open>m \<ge> 0\<close> le by auto
+            then show ?thesis
+              using \<open>m \<ge> 0\<close> \<open>e > 0\<close>
+              by (simp add: mult_left_mono im fUD [OF \<open>countable \<D>\<close> cbox intdisj] flip: right_diff_distrib)
+          qed
also have "\<dots> = ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)"
-            apply (rule measurable_measure_Diff [symmetric])
-            apply (simp add: assms(1) measurable_linear_image_interval)
-            apply (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
-             apply (simp add: Sup_le_iff cbox image_mono)
-            done
+          proof (rule measurable_measure_Diff [symmetric])
+            show "f ` cbox a b \<in> lmeasurable"
+              by (simp add: assms(1) measurable_linear_image_interval)
+            show "f ` \<Union> \<D> \<in> sets lebesgue"
+              by (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
+            show "f ` \<Union> \<D> \<subseteq> f ` cbox a b"
+              by (simp add: Sup_le_iff cbox image_mono)
+          qed
finally show "m * ?\<mu> S - e \<le> ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)" .
show "f ` cbox a b - f ` \<Union>\<D> \<in> lmeasurable"
by (simp add: fUD \<open>countable \<D>\<close> \<open>linear f\<close> cbox fmeasurable.Diff intdisj measurable_linear_image_interval)
@@ -3166,7 +3119,7 @@
moreover have fim: "f ` (S \<inter> h ` (cbox a b)) = (f ` S) \<inter> cbox a b"
by (auto simp: hf rev_image_eqI fh)
ultimately have 1: "(f ` S) \<inter> cbox a b \<in> lmeasurable"
-              and 2: "m * ?\<mu> (S \<inter> h ` cbox a b) = ?\<mu> ((f ` S) \<inter> cbox a b)"
+              and 2: "?\<mu> ((f ` S) \<inter> cbox a b) = m * ?\<mu> (S \<inter> h ` cbox a b)"
using fBS [of "S \<inter> (h ` (cbox a b))"] by auto
have *: "\<lbrakk>\<bar>z - m\<bar> < e; z \<le> w; w \<le> m\<rbrakk> \<Longrightarrow> \<bar>w - m\<bar> \<le> e"
for w z m and e::real by auto
@@ -3192,20 +3145,12 @@
show "?\<mu> (S \<inter> h ` cbox a b) \<le> ?\<mu> S"
by (simp add: S Shab fmeasurableD measure_mono_fmeasurable)
qed
-        have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> m * e / (1 + \<bar>m\<bar>)"
-        proof -
-          have mm: "\<bar>m\<bar> = m"
-            by (simp add: \<open>0 \<le> m\<close>)
-          then have "\<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m \<le> e / (1 + m) * m"
-            by (metis (no_types) \<open>0 \<le> m\<close> meas_adiff abs_minus_commute mult_right_mono)
-          moreover have "\<forall>r. \<bar>r * m\<bar> = m * \<bar>r\<bar>"
-            by (metis \<open>0 \<le> m\<close> abs_mult_pos mult.commute)
-          ultimately show ?thesis
-            apply (simp add: 2 [symmetric])
-            by (metis (no_types) abs_minus_commute mult.commute right_diff_distrib' mm)
-        qed
+        have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> \<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m"
+          by (metis "2" \<open>m \<ge> 0\<close> abs_minus_commute abs_mult_pos mult.commute order_refl right_diff_distrib')
+        also have "\<dots> \<le> e / (1 + m) * m"
+          by (metis \<open>m \<ge> 0\<close> abs_minus_commute abs_of_nonneg meas_adiff mult.commute mult_left_mono)
also have "\<dots> < e"
-          using \<open>e > 0\<close> by (cases "m \<ge> 0") (simp_all add: field_simps)
+          using \<open>e > 0\<close> \<open>m \<ge> 0\<close> by (simp add: field_simps)
finally have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> < e" .
with 1 show ?thesis by auto
qed
@@ -3293,23 +3238,21 @@
proposition absolutely_integrable_componentwise_iff:
shows "f absolutely_integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A)"
proof -
-  have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)"
-          if "f integrable_on A"
-  proof -
-    have 1: "\<And>i. \<lbrakk>(\<lambda>x. norm (f x)) integrable_on A; i \<in> Basis\<rbrakk>
-                 \<Longrightarrow> (\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
-      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. norm(f x)"])
-      using Basis_le_norm integrable_component that apply fastforce+
-      done
-    have 2: "\<forall>i\<in>Basis. (\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on A \<Longrightarrow> f absolutely_integrable_on A"
-      apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)"])
-      using norm_le_l1 that apply (force intro: integrable_sum)+
-      done
-    show ?thesis
-      apply auto
-       apply (metis (full_types) absolutely_integrable_on_def set_integrable_abs 1)
-      apply (metis (full_types) absolutely_integrable_on_def 2)
-      done
+  have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)" (is "?lhs = ?rhs")
+    if "f integrable_on A"
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (metis absolutely_integrable_on_def Topology_Euclidean_Space.norm_nth_le absolutely_integrable_integrable_bound integrable_component that)
+  next
+    assume R: ?rhs
+    have "f absolutely_integrable_on A"
+    proof (rule absolutely_integrable_integrable_bound)
+      show "(\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)) integrable_on A"
+        using R by (force intro: integrable_sum)
+    qed (use that norm_le_l1 in auto)
+    then show ?lhs
+      using absolutely_integrable_on_def by auto
qed
show ?thesis
unfolding absolutely_integrable_on_def
@@ -3331,8 +3274,7 @@
shows "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S"
proof -
have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
-    apply (rule absolutely_integrable_linear [OF assms])
+    by (simp add: absolutely_integrable_linear assms bounded_linear_scaleR_right)
then show ?thesis
using assms by blast
qed
@@ -3354,10 +3296,6 @@
shows "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) absolutely_integrable_on S"
(is "?g absolutely_integrable_on S")
proof -
-  have eq: "?g =
-        (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
-               (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
-    by (simp)
have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
absolutely_integrable_on S"
@@ -3367,19 +3305,20 @@
by (simp add: linear_linear algebra_simps linearI)
moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
absolutely_integrable_on S"
+      using assms \<open>i \<in> Basis\<close>
unfolding o_def
-      apply (rule absolutely_integrable_norm [unfolded o_def])
-      using assms \<open>i \<in> Basis\<close>
-      apply (auto simp: algebra_simps dest: absolutely_integrable_component[where b=i])
-      done
+      by (intro absolutely_integrable_norm [unfolded o_def])
+         (auto simp: algebra_simps dest: absolutely_integrable_component)
ultimately show ?thesis
by (subst comp_assoc) (blast intro: absolutely_integrable_linear)
qed
+  have eq: "?g =
+        (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
+               (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
+    by (simp)
show ?thesis
-    apply (rule ssubst [OF eq])
-    apply (rule absolutely_integrable_sum)
-     apply (force simp: intro!: *)+
-    done
+    unfolding eq
+    by (rule absolutely_integrable_sum) (force simp: intro!: *)+
qed

lemma abs_absolutely_integrableI_1:
@@ -3447,10 +3386,8 @@
qed
moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
-    apply (intro set_integral_add absolutely_integrable_scaleR_left assms)
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
-    done
ultimately show ?thesis by metis
qed

@@ -3482,10 +3419,9 @@
qed
moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
-    apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
-    done
+    by (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
ultimately show ?thesis by metis
qed

@@ -3522,9 +3458,10 @@
shows "f absolutely_integrable_on A"
proof -
have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
-    apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
-    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
-    by (simp add: comp inner_diff_left)
+  proof (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
+    show "(\<lambda>x. g x - f x) integrable_on A"
+      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+  qed (simp add: comp inner_diff_left)
then show ?thesis
by simp
qed
@@ -3536,9 +3473,10 @@
shows "g absolutely_integrable_on A"
proof -
have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
-    apply (rule set_integral_add [OF f nonnegative_absolutely_integrable])
-    using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
-    by (simp add: comp inner_diff_left)
+  proof (rule set_integral_add [OF f nonnegative_absolutely_integrable])
+    show "(\<lambda>x. g x - f x) integrable_on A"
+      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+  qed (simp add: comp inner_diff_left)
then show ?thesis
by simp
qed
@@ -3613,9 +3551,10 @@
apply (subst has_integral_alt)
apply (subst (asm) has_integral_alt)
apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
-    apply (metis vector_one_nth)
-    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
-    apply (blast intro!: *)
+    subgoal by (metis vector_one_nth)
+    subgoal
+      apply (erule all_forward imp_forward ex_forward asm_rl)+
+      by (blast intro!: *)+
done
qed

@@ -3653,10 +3592,12 @@
and B: "ball 0 B \<subseteq> cbox a b" for e B and a b::"real^1"
proof -
have B': "ball 0 B \<subseteq> {a\$1..b\$1}"
-      using B
-      apply (simp add: subset_iff Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
-      apply (metis (full_types) norm_real vec_component)
-      done
+    proof (clarsimp)
+      fix t
+      assume "\<bar>t\<bar> < B" then show "a \$ 1 \<le> t \<and> t \<le> b \$ 1"
+        using subsetD [OF B]
+        by (metis (mono_tags, hide_lams) mem_ball_0 mem_box_cart(2) norm_real vec_component)
+    qed
have eq: "(\<lambda>x. if vec x \<in> S then f (vec x) else 0) = (\<lambda>x. if x \<in> S then f x else 0) \<circ> vec"
by force
have [simp]: "(\<exists>y\<in>S. x = y \$ 1) \<longleftrightarrow> vec x \<in> S" for x
@@ -3670,11 +3611,10 @@
apply (subst (asm) has_integral_alt)
apply (simp add: has_integral_vec1_D_cbox eq_cbox split: if_split_asm, blast)
apply (intro conjI impI)
-     apply (metis vector_one_nth)
+    subgoal by (metis vector_one_nth)
apply (erule thin_rl)
-    apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
-    using * apply blast
-    done
+    apply (erule all_forward ex_forward conj_forward)+
+      by (blast intro!: *)+
qed

@@ -3988,11 +3928,8 @@
by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
-      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
-      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
-      apply (rule filterlim_real_sequentially)
-      done
+     have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
+       by (auto intro: filterlim_compose[OF lim filterlim_tendsto_add_at_top] filterlim_real_sequentially)
then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
by (simp add: F_mono F_le_T tendsto_diff)
qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
@@ -4028,17 +3965,22 @@
shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
=  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
proof-
-  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
-    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
-      (auto intro!: DERIV_isCont)
-
-  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
-    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
-    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
-    by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
-
-  thus ?thesis using 0 by auto
+  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel)
+      = LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x"
+    by (meson vector_space_over_itself.scale_left_distrib)
+  also have "... = (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+  proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+      using DERIV_isCont by blast+
+  qed
+  finally have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+                (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" .
+  moreover have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
+  proof (intro integral_FTC_Icc_real derivative_eq_intros cont_f cont_g continuous_intros)
+    show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+      using DERIV_isCont by blast+
+  qed auto
+  ultimately show ?thesis by auto
qed

lemma integral_by_parts':
@@ -4737,10 +4679,8 @@
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "S \<in> sets lebesgue"
shows "f absolutely_integrable_on S \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S) \<and> (\<lambda>x. \<bar>f x\<bar>) integrable_on S"
-  using assms
-  apply (auto simp: absolutely_integrable_measurable integrable_on_lebesgue_on)
-  apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
-  using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
+  by (metis abs_absolutely_integrableI_1 absolutely_integrable_measurable_real assms
+            measurable_bounded_by_integrable_imp_integrable order_refl real_norm_def set_integrable_abs set_lebesgue_integral_eq_integral(1))

lemma absolutely_integrable_imp_borel_measurable:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -4782,8 +4722,8 @@
have "\<exists>T' B. open T' \<and> f x \<in> T' \<and>
(\<forall>y\<in>f ` V \<inter> T \<inter> T'. norm (g y - g (f x)) \<le> B * norm (y - f x))"
if "f x \<in> T" "x \<in> V" for x
-        apply (rule_tac x = "ball (f x) 1" in exI)
-        using that noxy by (force simp: g)
+        using that noxy
+        by (rule_tac x = "ball (f x) 1" in exI) (force simp: g)
then have "negligible (g ` (f ` V \<inter> T))"
by (force simp: \<open>negligible T\<close> negligible_Int intro!: negligible_locally_Lipschitz_image)
moreover have "V \<subseteq> g ` (f ` V \<inter> T)"
@@ -4826,12 +4766,12 @@
using less by linarith
with \<delta> \<open>y \<in> S\<close> have le: "norm (f y - f x - f' x (y - x)) \<le> B * norm (y - x) - norm (y - x)/i"
by (auto simp: algebra_simps)
-    have *: "\<lbrakk>norm(f - f' - y) \<le> b - c; b \<le> norm y; d \<le> c\<rbrakk> \<Longrightarrow> d \<le> norm(f - f')"
-      for b c d and y f f'::'a
-      using norm_triangle_ineq3 [of "f - f'" y] by simp
-    show ?thesis
-      apply (rule * [OF le B])
+    have "norm (y - x) / real (max i j) \<le> norm (y - x) / real i"
using \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> by (simp add: field_split_simps max_mult_distrib_left of_nat_max less_max_iff_disj)
+    also have "... \<le> norm (f y - f x)"
+      using B [of "y-x"] le norm_triangle_ineq3 [of "f y - f x" "f' x (y - x)"]
+      by linarith
+    finally show ?thesis .
qed
with \<open>x \<in> S\<close> \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> show "\<exists>n\<in>{0<..}. x \<in> U n"
by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj)
@@ -5069,11 +5009,11 @@
qed
finally show ?thesis .
qed
-    then show "\<exists>d>0. \<forall>y\<in>f ` S.
+    with \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close>
+    show "\<exists>d>0. \<forall>y\<in>f ` S.
norm (y - f a) < d \<longrightarrow>
norm (g y - g (f a) - g' (y - f a)) \<le> e * norm (y - f a)"
-      apply (rule_tac x="min k (d / B)" in exI)
-      using \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close> by (auto simp: gf)
+      by (rule_tac x="min k (d / B)" in exI) (auto simp: gf)
qed
qed
```