author paulson Sun, 11 Oct 2020 18:46:44 +0100 changeset 72447 c6c352c5807f parent 72444 2d9a70b85009 (current diff) parent 72446 d189ad779a23 (diff) child 72448 faad63aca1e7
merged
```--- a/src/HOL/Analysis/Change_Of_Vars.thy	Sun Oct 11 17:42:32 2020 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Sun Oct 11 18:46:44 2020 +0100
@@ -744,7 +744,7 @@
fix x :: "(real,'n) vec"
assume "x \<in> T n"
show "(f has_derivative f' x) (at x within T n)"
-        by (metis (no_types, lifting) \<open>x \<in> T n\<close> deriv has_derivative_within_subset mem_Collect_eq subsetI T_def)
+        by (metis (no_types, lifting) \<open>x \<in> T n\<close> deriv has_derivative_subset mem_Collect_eq subsetI T_def)
show "\<bar>det (matrix (f' x))\<bar> \<le> (Suc n) * e"
using \<open>x \<in> T n\<close> T_def by auto
next
@@ -797,7 +797,7 @@
have "(\<Sum>k\<le>n. ?\<mu> (f ` T k)) \<le> (\<Sum>k\<le>n. ((k+1) * e) * ?\<mu>(T k))"
proof (rule sum_mono [OF measure_bounded_differentiable_image])
show "(f has_derivative f' x) (at x within T k)" if "x \<in> T k" for k x
-          using that unfolding T_def by (blast intro: deriv has_derivative_within_subset)
+          using that unfolding T_def by (blast intro: deriv has_derivative_subset)
show "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on T k" for k
using absolutely_integrable_on_def aint_T by blast
show "\<bar>det (matrix (f' x))\<bar> \<le> real (k + 1) * e" if "x \<in> T k" for k x
@@ -916,7 +916,7 @@
have In: "?I n \<in> lmeasurable"
by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int)
moreover have "\<And>x. x \<in> ?I n \<Longrightarrow> (f has_derivative f' x) (at x within ?I n)"
-      by (meson Int_iff deriv has_derivative_within_subset subsetI)
+      by (meson Int_iff deriv has_derivative_subset subsetI)
moreover have int_In: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on ?I n"
proof -
have "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S"
@@ -2356,7 +2356,7 @@
proof (rule measurable_bounded_by_integrable_imp_integrable)
have "(\<lambda>x. ?D x) \<in> borel_measurable (lebesgue_on ({t. h n (g t) = y} \<inter> S))"
apply (intro borel_measurable_abs borel_measurable_det_Jacobian [OF h_lmeas, where f=g])
-          by (meson der_g IntD2 has_derivative_within_subset inf_le2)
+          by (meson der_g IntD2 has_derivative_subset inf_le2)
then have "(\<lambda>x. if x \<in> {t. h n (g t) = y} \<inter> S then ?D x else 0) \<in> borel_measurable lebesgue"
by (rule borel_measurable_if_I [OF _ h_lmeas])
then show "(\<lambda>x. if x \<in> {t. h n (g t) = y} then ?D x else 0) \<in> borel_measurable (lebesgue_on S)"
@@ -2372,7 +2372,7 @@
using integrable_restrict_Int by force
have "(g ` ({t. h n (g t) = y} \<inter> S)) \<in> lmeasurable"
apply (rule measurable_differentiable_image [OF h_lmeas])
-         apply (blast intro: has_derivative_within_subset [OF der_g])
+         apply (blast intro: has_derivative_subset [OF der_g])
apply (rule int_det)
done
moreover have "g ` ({t. h n (g t) = y} \<inter> S) = {x. h n x = y} \<inter> g ` S"
@@ -2380,7 +2380,7 @@
moreover have "measure lebesgue (g ` ({t. h n (g t) = y} \<inter> S))
\<le> integral ({t. h n (g t) = y} \<inter> S) (\<lambda>t. \<bar>det (matrix (g' t))\<bar>)"
apply (rule measure_differentiable_image [OF h_lmeas _ int_det])
-        apply (blast intro: has_derivative_within_subset [OF der_g])
+        apply (blast intro: has_derivative_subset [OF der_g])
done
ultimately show ?thesis
using \<open>y > 0\<close> integral_restrict_Int [of S "{t. h n (g t) = y}" "\<lambda>t. \<bar>det (matrix (g' t))\<bar> * y"]
@@ -2484,7 +2484,7 @@
let ?D = "\<lambda>x. det (matrix (g' x))"
define S' where "S' \<equiv> {x \<in> S. ?D x * f(g x) \<noteq> 0}"
then have der_gS': "\<And>x. x \<in> S' \<Longrightarrow> (g has_derivative g' x) (at x within S')"
-    by (metis (mono_tags, lifting) der_g has_derivative_within_subset mem_Collect_eq subset_iff)
+    by (metis (mono_tags, lifting) der_g has_derivative_subset mem_Collect_eq subset_iff)
have "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) integrable_on UNIV"
then have Df_borel: "(\<lambda>x. if x \<in> S then \<bar>?D x\<bar> * f (g x) else 0) \<in> borel_measurable lebesgue"
@@ -2505,7 +2505,7 @@
proof (rule differentiable_image_in_sets_lebesgue)
show "g differentiable_on S'"
using der_g unfolding S'_def differentiable_def differentiable_on_def
-      by (blast intro: has_derivative_within_subset)
+      by (blast intro: has_derivative_subset)
qed auto
have f: "f \<in> borel_measurable (lebesgue_on (g ` S'))"
@@ -2532,7 +2532,7 @@
by (simp add: \<open>S' \<in> sets lebesgue\<close> \<open>open T\<close> borel_measurable_vimage_open sets_restrict_space_iff)
show "g differentiable_on {x \<in> S'. f (g x) \<in> T}"
using der_g unfolding S'_def differentiable_def differentiable_on_def
-        by (blast intro: has_derivative_within_subset)
+        by (blast intro: has_derivative_subset)
qed auto
ultimately have "{x \<in> g ` S'. f x \<in> T} \<in> sets lebesgue"
by metis
@@ -2566,7 +2566,7 @@
fix x
assume x: "x \<in> S \<and> det (matrix (g' x)) = 0"
then show "(g has_derivative g' x) (at x within {x \<in> S. det (matrix (g' x)) = 0})"
-      by (metis (no_types, lifting) der_g has_derivative_within_subset mem_Collect_eq subsetI)
+      by (metis (no_types, lifting) der_g has_derivative_subset mem_Collect_eq subsetI)
then show "rank (matrix (g' x)) < CARD('n)"
using det_nz_iff_inj matrix_vector_mul_linear x
@@ -2630,7 +2630,7 @@
have dfgbm: "?D \<in> borel_measurable (lebesgue_on S)"
using intS absolutely_integrable_on_def integrable_imp_measurable by blast
have der_gN: "(g has_derivative g' x) (at x within ?N)" if "x \<in> ?N" for x
-      using der_g has_derivative_within_subset that by force
+      using der_g has_derivative_subset that by force
have "(\<lambda>x. - f x) integrable_on g ` ?N \<and>
integral (g ` ?N) (\<lambda>x. - f x) \<le> integral ?N (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * - f (g x))"
proof (rule integral_on_image_ubound_nonneg [OF _ der_gN])
@@ -2652,7 +2652,7 @@
by (rule absolutely_integrable_absolutely_integrable_ubound) auto

have der_gP: "(g has_derivative g' x) (at x within ?P)" if "x \<in> ?P" for x
-      using der_g has_derivative_within_subset that by force
+      using der_g has_derivative_subset that by force
have "f integrable_on g ` ?P \<and> integral (g ` ?P) f \<le> integral ?P ?D"
proof (rule integral_on_image_ubound_nonneg [OF _ der_gP])
have "?D integrable_on {x \<in> S. 0 < ?D x}"
@@ -2805,9 +2805,9 @@
= ((\<lambda>x. f (g x)) -` Y \<inter> S) \<inter> {x \<in> S. f (g x) > 0}" for Y
by auto
show "(g has_derivative g' x) (at x within {x \<in> S. f (g x) > 0})" if "x \<in> {x \<in> S. f (g x) > 0}" for x
-      using that der_g has_derivative_within_subset by fastforce
+      using that der_g has_derivative_subset by fastforce
show "(h has_derivative h' y) (at y within {y \<in> T. f y > 0})" if "y \<in> {y \<in> T. f y > 0}" for y
-      using that der_h has_derivative_within_subset by fastforce
+      using that der_h has_derivative_subset by fastforce
qed (use gh hg id in auto)
have "-": "(?DN has_integral b) {x \<in> S. f (g x) < 0} \<longleftrightarrow> ((\<lambda>x. - f x) has_integral b) {y \<in> T. f y < 0}" for b
proof (rule cov_invertible_nonneg_eq)
@@ -2815,9 +2815,9 @@
= ((\<lambda>x. f (g x)) -` uminus ` y \<inter> S) \<inter> {x \<in> S. f (g x) < 0}" for y
using image_iff by fastforce
show "(g has_derivative g' x) (at x within {x \<in> S. f (g x) < 0})" if "x \<in> {x \<in> S. f (g x) < 0}" for x
-      using that der_g has_derivative_within_subset by fastforce
+      using that der_g has_derivative_subset by fastforce
show "(h has_derivative h' y) (at y within {y \<in> T. f y < 0})" if "y \<in> {y \<in> T. f y < 0}" for y
-      using that der_h has_derivative_within_subset by fastforce
+      using that der_h has_derivative_subset by fastforce
qed (use gh hg id in auto)
show ?thesis
proof
@@ -3016,13 +3016,13 @@
proof (rule cv_inv_version4)
show "(g has_derivative g' x) (at x within ?S) \<and> invertible (matrix (g' x))"
if "x \<in> ?S" for x
-      using der_g that has_derivative_within_subset that by fastforce
+      using der_g that has_derivative_subset that by fastforce
show "continuous_on (g ` ?S) h \<and> h (g x) = x"
if "x \<in> ?S" for x
using that continuous_on_subset [OF conth]  by (simp add: hg image_mono)
qed
have "(g has_derivative g' x) (at x within {x \<in> S. rank (matrix (g' x)) < CARD('m)})" if "x \<in> S" for x
-    by (metis (no_types, lifting) der_g has_derivative_within_subset mem_Collect_eq subsetI that)
+    by (metis (no_types, lifting) der_g has_derivative_subset mem_Collect_eq subsetI that)
then have "negligible (g ` {x \<in> S. \<not> invertible (matrix (g' x))})"
by (auto simp: invertible_det_nz det_eq_0_rank intro: baby_Sard)
then have neg: "negligible {x \<in> g ` S. x \<notin> g ` ?S \<and> f x \<noteq> 0}"
@@ -3085,7 +3085,7 @@
show "(g has_derivative g' x) (at x within (?U n))"
if "x \<in> ?U n" for x
-      using that by (blast intro!: has_derivative_within_subset [OF der_g])
+      using that by (blast intro!: has_derivative_subset [OF der_g])
show "inj_on g (?U n)"
using inj by (auto simp: inj_on_def)
qed
@@ -3173,7 +3173,7 @@
proof (rule differentiable_image_in_sets_lebesgue [OF F_leb])
show "g differentiable_on F m"
using der_g unfolding differentiable_def differentiable_on_def
-        by (meson Sup_upper UNIV_I UnionI has_derivative_within_subset image_eqI)
+        by (meson Sup_upper UNIV_I UnionI has_derivative_subset image_eqI)
qed auto
have fgU: "\<And>n. f absolutely_integrable_on (\<Union>m\<le>n. g ` F m)"
"(\<lambda>n. integral (\<Union>m\<le>n. g ` F m) f) \<longlonglongrightarrow> integral (\<Union>m. g ` F m) f"
@@ -3266,7 +3266,7 @@
fix n x
assume "x \<in> \<Union>(F ` UNIV)"
then show "(g has_derivative g' x) (at x within \<Union>(F ` UNIV))"
-      using Ceq \<open>C \<union> N = S\<close> der_g has_derivative_within_subset by blast
+      using Ceq \<open>C \<union> N = S\<close> der_g has_derivative_subset by blast
next
have "\<Union>(F ` UNIV) \<subseteq> S"
using Ceq \<open>C \<union> N = S\<close> by blast```
```--- a/src/HOL/Analysis/Derivative.thy	Sun Oct 11 17:42:32 2020 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Sun Oct 11 18:46:44 2020 +0100
@@ -893,7 +893,7 @@
qed
have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
(f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
-    by (auto intro: * has_derivative_within_subset [OF derf])
+    by (auto intro: * has_derivative_subset [OF derf])
then have "continuous_on (?p ` {0..1}) f"
unfolding continuous_on_eq_continuous_within
by (meson has_derivative_continuous)
@@ -905,7 +905,7 @@
interpret linear "(f' ?u)"
using u by (auto intro!: has_derivative_linear derf *)
have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
-      by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
+      by (intro derivative_intros has_derivative_subset [OF derf]) (use u * in auto)
hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
by (simp add: at_within_open[OF u open_greaterThanLessThan] scaleR has_vector_derivative_def o_def)
} note 2 = this
@@ -1907,7 +1907,7 @@

lemma has_vector_derivative_within_subset:
"(f has_vector_derivative f') (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f has_vector_derivative f') (at x within T)"
-  by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
+  by (auto simp: has_vector_derivative_def intro: has_derivative_subset)

lemma has_vector_derivative_at_within:
"(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within S)"
@@ -2549,7 +2549,7 @@

have "\<And>x. x \<in> ball y d \<inter> Y \<Longrightarrow> onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
-    with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
+    with seg has_derivative_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
by (rule differentiable_bound_linearization[where S="?S"])
(auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)```
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 11 17:42:32 2020 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Oct 11 18:46:44 2020 +0100
@@ -510,10 +510,12 @@
have *: "?S(h \<circ> f) = h \<circ> ?S f"
using zero by auto
show "\<exists>z. (?S(h \<circ> f) has_integral z) (cbox a b) \<and> norm (z - h y) < e"
-        apply (rule_tac x="h z" in exI)
-        apply (simp add: * has_integral_linear_cbox[OF z(1) h])
-        apply (metis B diff le_less_trans pos_less_divide_eq z(2))
-        done
+      proof (intro exI conjI)
+        show "(?S(h \<circ> f) has_integral h z) (cbox a b)"
+          by (simp add: * has_integral_linear_cbox[OF z(1) h])
+        show "norm (h z - h y) < e"
+          by (metis B diff le_less_trans pos_less_divide_eq z(2))
+      qed
qed
qed
qed
@@ -635,11 +637,12 @@
have *: "\<And>x. (if x \<in> S then f x + g x else 0) = (?S f x) + (?S g x)"
by auto
show "\<exists>z. (?S(\<lambda>x. f x + g x) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
-        apply (rule_tac x="w + z" in exI)
-        using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
-        apply (auto simp add: field_simps)
-        done
+      proof (intro exI conjI)
+        show "(?S(\<lambda>x. f x + g x) has_integral (w + z)) (cbox a b)"
+        show "norm (w + z - (k + l)) < e"
+          by (metis dist_norm dist_triangle_add_half w(2) z(2))
+      qed
qed
qed
qed
@@ -731,9 +734,7 @@

lemma integral_linear:
"f integrable_on S \<Longrightarrow> bounded_linear h \<Longrightarrow> integral S (h \<circ> f) = h (integral S f)"
-  apply (rule has_integral_unique [where i=S and f = "h \<circ> f"])
-  apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
-  done
+  by (meson has_integral_iff has_integral_linear)

lemma integrable_on_cnj_iff:
"(\<lambda>x. cnj (f x)) integrable_on A \<longleftrightarrow> f integrable_on A"
@@ -1005,9 +1006,8 @@
\<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> \<D>2. content K *\<^sub>R f x))
< 1 / (m + 1)"
by metis
-  have "\<And>n. gauge (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}})"
-    apply (rule gauge_Inter)
-    using \<gamma> by auto
+  have "gauge (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}})" for n
+    using \<gamma> by (intro gauge_Inter) auto
then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}}) fine p"
by (meson fine_division_exists)
then obtain p where p: "\<And>z. p z tagged_division_of cbox a b"
@@ -1485,10 +1485,7 @@
proof (cases "f integrable_on cbox a b")
case True
with k show ?thesis
-        apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
-        apply (auto intro: integrable_integral)
-        done
+        by (auto simp: integrable_split intro: integral_unique [OF has_integral_split[OF _ _ k]])
next
case False
have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
@@ -1497,8 +1494,7 @@
then have "f integrable_on cbox a b"
unfolding integrable_on_def
apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
-          apply (rule has_integral_split[OF _ _ k])
-          apply (auto intro: integrable_integral)
+          apply (auto intro: has_integral_split[OF _ _ k])
done
then show False
using False by auto
@@ -1518,16 +1514,12 @@
subsection \<open>Bounds on the norm of Riemann sums and the integral itself\<close>

lemma dsum_bound:
-  assumes "p division_of (cbox a b)"
+  assumes p: "p division_of (cbox a b)"
and "norm c \<le> e"
shows "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content(cbox a b)"
proof -
have sumeq: "(\<Sum>i\<in>p. \<bar>content i\<bar>) = sum content p"
-    apply (rule sum.cong)
-    using assms
-    apply simp
-    apply (metis abs_of_nonneg content_pos_le)
-    done
+    by simp
have e: "0 \<le> e"
using assms(2) norm_ge_zero order_trans by blast
have "norm (sum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
@@ -1535,10 +1527,7 @@
also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
by (simp add: sum_distrib_left[symmetric] mult.commute assms(2) mult_right_mono sum_nonneg)
also have "... \<le> e * content (cbox a b)"
-    apply (rule mult_left_mono [OF _ e])
-    using additive_content_division assms(1) eq_iff apply blast
-    done
+    by (metis additive_content_division p eq_iff sumeq)
finally show ?thesis .
qed

@@ -1559,20 +1548,19 @@
have con: "\<And>xk. xk \<in> p \<Longrightarrow> 0 \<le> content (snd xk)"
using tagged_division_ofD(4) [OF p] content_pos_le
by force
-  have norm: "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e"
-    unfolding fst_conv using tagged_division_ofD(2,3)[OF p] assms
-    by (metis prod.collapse subset_eq)
have "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p) \<le> (\<Sum>i\<in>p. norm (case i of (x, k) \<Rightarrow> content k *\<^sub>R f x))"
by (rule norm_sum)
also have "...  \<le> e * content (cbox a b)"
-    unfolding split_def norm_scaleR
-    apply (rule order_trans[OF sum_mono])
-    apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e])
-    apply (metis norm)
-    unfolding sum_distrib_right[symmetric]
-    using con sum_le
-    apply (auto simp: mult.commute intro: mult_left_mono [OF _ e])
-    done
+  proof -
+    have "\<And>xk. xk \<in> p \<Longrightarrow> norm (f (fst xk)) \<le> e"
+      using assms(2) p tag_in_interval by force
+    moreover have "(\<Sum>i\<in>p. \<bar>content (snd i)\<bar> * e) \<le> e * content (cbox a b)"
+      unfolding sum_distrib_right[symmetric]
+      using con sum_le by (auto simp: mult.commute intro: mult_left_mono [OF _ e])
+    ultimately show ?thesis
+      unfolding split_def norm_scaleR
+      by (metis (no_types, lifting) mult_left_mono[OF _ abs_ge_zero]   order_trans[OF sum_mono])
+  qed
finally show ?thesis .
qed

@@ -1581,9 +1569,8 @@
and "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e"
shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - sum (\<lambda>(x,k). content k *\<^sub>R g x) p) \<le>
e * content (cbox a b)"
-  apply (rule order_trans[OF _ rsum_bound[OF assms]])
-  apply (simp add: split_def scaleR_diff_right sum_subtractf eq_refl)
-  done
+  using order_trans[OF _ rsum_bound[OF assms]]
+  by (simp add: split_def scaleR_diff_right sum_subtractf eq_refl)

lemma has_integral_bound:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -1722,10 +1709,7 @@
and "f integrable_on S" "g integrable_on S"
and "\<And>x. x \<in> S \<Longrightarrow> (f x)\<bullet>k \<le> (g x)\<bullet>k"
shows "(integral S f)\<bullet>k \<le> (integral S g)\<bullet>k"
-  apply (rule has_integral_component_le)
-  using integrable_integral assms
-  apply auto
-  done
+  using has_integral_component_le assms by blast

lemma has_integral_component_nonneg:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1744,10 +1728,7 @@
shows "0 \<le> (integral S f)\<bullet>k"
proof (cases "f integrable_on S")
case True show ?thesis
-    apply (rule has_integral_component_nonneg)
-    using assms True
-    apply auto
-    done
+    using True assms has_integral_component_nonneg by blast
next
case False then show ?thesis by (simp add: not_integrable_integral)
qed
@@ -1785,11 +1766,7 @@
and "\<forall>x\<in>cbox a b. B \<le> f(x)\<bullet>k"
and "k \<in> Basis"
shows "B * content (cbox a b) \<le> (integral(cbox a b) f)\<bullet>k"
-  apply (rule has_integral_component_lbound)
-  using assms
-  unfolding has_integral_integral
-  apply auto
-  done
+  using assms has_integral_component_lbound by blast

lemma integral_component_lbound_real:
assumes "f integrable_on {a ::real..b}"
@@ -1805,11 +1782,7 @@
and "\<forall>x\<in>cbox a b. f x\<bullet>k \<le> B"
and "k \<in> Basis"
shows "(integral (cbox a b) f)\<bullet>k \<le> B * content (cbox a b)"
-  apply (rule has_integral_component_ubound)
-  using assms
-  unfolding has_integral_integral
-  apply auto
-  done
+  using assms has_integral_component_ubound by blast

lemma integral_component_ubound_real:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -1885,8 +1858,7 @@
have "norm (f x - g n x) + norm (f x - g m x) \<le> 1 / (real n + 1) + 1 / (real m + 1)"
using g_near_f[OF x, of n] g_near_f[OF x, of m] by simp
also have "\<dots> \<le> 1 / (real M) + 1 / (real M)"
-          using \<open>M \<noteq> 0\<close> m n by (auto simp: field_split_simps)
+          using \<open>M \<noteq> 0\<close> m n by (intro add_mono; force simp: field_split_simps)
also have "\<dots> = 2 / real M"
by auto
finally show "norm (g n x - g m x) \<le> 2 / real M"
@@ -2130,10 +2102,7 @@
finally show "(\<Sum>(x, K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
qed
then show "\<bar>\<Sum>(x, K)\<in>\<D>. content K * ?i x\<bar> < e"
-      unfolding *
-      apply (subst abs_of_nonneg)
-      using measure_nonneg
-      by (force simp add: indicator_def intro: sum_nonneg)+
+      unfolding *  by (simp add: sum_nonneg split: prod.split)
qed
qed

@@ -2158,9 +2127,9 @@
then have nn_gt0: "e/2 / ((real n+1) * (2 ^ n)) > 0" for n
by simp
then have "\<exists>\<gamma>. gauge \<gamma> \<and>
-                   (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
-                        \<bar>\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R indicator S x\<bar>
-                        < e/2 / ((real n + 1) * 2 ^ n))" for n
+                 (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
+                      \<bar>\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R indicator S x\<bar>
+                      < e/2 / ((real n + 1) * 2 ^ n))" for n
using negs [unfolded negligible_def has_integral] by auto
then obtain \<gamma> where
gd: "\<And>n. gauge (\<gamma> n)"
@@ -2238,9 +2207,7 @@
by force
qed auto
also have "... = (\<Sum>i\<le>N + 1. \<Sum>j\<in>q i. (real i + 1) * (case j of (x, K) \<Rightarrow> content K *\<^sub>R indicator S x))"
-        apply (rule sum_Sigma_product [symmetric])
-        using q(1) apply auto
-        done
+        using q(1) by (intro sum_Sigma_product [symmetric]) auto
also have "... \<le> (\<Sum>i\<le>N + 1. (real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar>)"
by (rule sum_mono) (simp add: sum_distrib_left [symmetric])
also have "... \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
@@ -2309,16 +2276,17 @@
then show ?thesis
by auto
qed
+  have \<section>: "\<And>a b z. \<lbrakk>\<And>x. x \<in> T \<and> x \<notin> S \<Longrightarrow> g x = f x;
+                     ((\<lambda>x. if x \<in> T then f x else 0) has_integral z) (cbox a b)\<rbrakk>
+                    \<Longrightarrow> ((\<lambda>x. if x \<in> T then g x else 0) has_integral z) (cbox a b)"
+      by (auto dest!: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])
show ?thesis
using fint gf
apply (subst has_integral_alt)
apply (subst (asm) has_integral_alt)
-    apply (simp split: if_split_asm)
+    apply (auto split: if_split_asm)
apply (blast dest: *)
-      apply (erule_tac V = "\<forall>a b. T \<noteq> cbox a b" in thin_rl)
-    apply (elim all_forward imp_forward ex_forward all_forward conj_forward asm_rl)
-     apply (auto dest!: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])
-    done
+    using \<section> by meson
qed

lemma has_integral_spike_eq:
@@ -2383,10 +2351,7 @@
using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast

lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
-  apply (subst insert_is_Un)
-  unfolding negligible_Un_eq
-  apply auto
-  done
+  by (metis insert_is_Un negligible_Un_eq negligible_sing)

lemma negligible_empty[iff]: "negligible {}"
using negligible_insert by blast
@@ -2478,9 +2443,8 @@
lemma has_integral_spike_interior:
assumes f: "(f has_integral y) (cbox a b)" and gf: "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
shows "(g has_integral y) (cbox a b)"
-  apply (rule has_integral_spike[OF negligible_frontier_interval _ f])
-  using gf by auto
-
+  by (meson Diff_iff gf has_integral_spike[OF negligible_frontier_interval _ f])
+
lemma has_integral_spike_interior_eq:
assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
shows "(f has_integral y) (cbox a b) \<longleftrightarrow> (g has_integral y) (cbox a b)"
@@ -2507,16 +2471,15 @@
fix a b :: 'b
show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
if "box a b = {}" for a b
-      apply (rule_tac x=f in exI)
-      using assms that by (auto simp: content_eq_0_interior)
+      using assms that
+      by (metis content_eq_0_interior integrable_on_null interior_cbox norm_zero right_minus_eq)
{
fix c g and k :: 'b
assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
assume k: "k \<in> Basis"
show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
"\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-         apply (rule_tac[!] x=g in exI)
-        using fg integrable_split[OF g k] by auto
+        using fg g k by auto
}
show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e"
@@ -2583,8 +2546,7 @@
then have x: "x \<in> cbox a b"
using as ptag by auto
show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l"
-      apply (rule_tac x="\<lambda>y. f x" in exI)
-    proof safe
+    proof (intro exI conjI strip)
show "(\<lambda>y. f x) integrable_on l"
unfolding integrable_on_def l by blast
next
@@ -2650,22 +2612,15 @@
let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and>
(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> opp (norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i)) e)"
show ?thesis
-    apply (subst has_integral)
-  proof safe
+  proof (subst has_integral, safe)
fix e :: real
assume e: "e > 0"
-    { assume "\<forall>e>0. ?P e (<)"
-      then show "?P (e * content (cbox a b)) (\<le>)"
-        apply (rule allE [where x="e * content (cbox a b)"])
-        apply (elim impE ex_forward conj_forward)
-        using F e apply (auto simp add: algebra_simps)
-        done }
-    { assume "\<forall>e>0. ?P (e * content (cbox a b)) (\<le>)"
-      then show "?P e (<)"
-        apply (rule allE [where x="e/2 / content (cbox a b)"])
-        apply (elim impE ex_forward conj_forward)
-        using F e apply (auto simp add: algebra_simps)
-        done }
+    show "?P (e * content (cbox a b)) (\<le>)" if \<section>[rule_format]: "\<forall>\<epsilon>>0. ?P \<epsilon> (<)"
+      using \<section> [of "e * content (cbox a b)"]
+      by (meson F e less_imp_le mult_pos_pos)
+    show "?P e (<)" if \<section>[rule_format]:  "\<forall>\<epsilon>>0. ?P (\<epsilon> * content (cbox a b)) (\<le>)"
+      using \<section> [of "e/2 / content (cbox a b)"]
+        using F e by (force simp add: algebra_simps)
qed
qed

@@ -2737,11 +2692,15 @@
also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
-          apply (rule d(2)[of x u])
-          using \<open>x \<in> K\<close> kab \<open>u \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+        proof (rule d)
+          show "norm (u - x) < d x"
+            using \<open>u \<in> K\<close> ball by (auto simp add: dist_real_def)
+        qed (use \<open>x \<in> K\<close> \<open>u \<in> K\<close> kab in auto)
show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
-          apply (rule d(2)[of x v])
-          using \<open>x \<in> K\<close> kab \<open>v \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+        proof (rule d)
+          show "norm (v - x) < d x"
+            using \<open>v \<in> K\<close> ball by (auto simp add: dist_real_def)
+        qed (use \<open>x \<in> K\<close> \<open>v \<in> K\<close> kab in auto)
qed
also have "\<dots> \<le> e * (Sup K - Inf K)"
using \<open>x \<in> K\<close> by (auto simp: k interval_bounds_real[OF \<open>u \<le> v\<close>] field_simps)
@@ -2759,9 +2718,8 @@
shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
proof -
have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
-    apply (rule fundamental_theorem_of_calculus [OF assms])
unfolding power2_eq_square
-    by (rule derivative_eq_intros | simp)+
+    by (rule fundamental_theorem_of_calculus [OF assms] derivative_eq_intros | simp)+
then show ?thesis
qed
@@ -2813,9 +2771,8 @@
show "((\<lambda>x. - cos (n * x) / n) has_vector_derivative sin (n * a)) (at a within {-pi..pi})"
if "a \<in> {-pi..pi}" for a :: real
using that False
-      apply (simp only: has_vector_derivative_def)
-      apply (rule derivative_eq_intros | force)+
-      done
+      unfolding has_vector_derivative_def
+      by (intro derivative_eq_intros | force)+
qed auto
then show ?thesis
by simp
@@ -2839,9 +2796,8 @@
if "x \<in> {-pi..pi}"
for x :: real
using that False
-      apply (simp only: has_vector_derivative_def)
-      apply (rule derivative_eq_intros | force)+
-      done
+      unfolding has_vector_derivative_def
+      by (intro derivative_eq_intros | force)+
qed auto
with False show ?thesis
@@ -3087,18 +3043,17 @@
shows "operative conj True (\<lambda>i. f integrable_on i)"
proof -
interpret comm_monoid conj True
-    by standard auto
-  have 1: "\<And>a b. box a b = {} \<Longrightarrow> f integrable_on cbox a b"
-    by (simp add: content_eq_0_interior integrable_on_null)
-  have 2: "\<And>a b c k.
-       \<lbrakk>k \<in> Basis;
-        f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c};
-        f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}\<rbrakk>
-       \<Longrightarrow> f integrable_on cbox a b"
-    unfolding integrable_on_def by (auto intro!: has_integral_split)
+  proof qed
show ?thesis
-    apply standard
-    using 1 2 by blast+
+  proof
+    show "\<And>a b. box a b = {} \<Longrightarrow> (f integrable_on cbox a b) = True"
+      by (simp add: content_eq_0_interior integrable_on_null)
+    show "\<And>a b c k.
+             k \<in> Basis \<Longrightarrow>
+             (f integrable_on cbox a b) \<longleftrightarrow>
+             (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} \<and> f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+      unfolding integrable_on_def by (auto intro!: has_integral_split)
+  qed
qed

lemma integrable_subinterval:
@@ -3246,7 +3201,7 @@
assume "e > 0"
obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b} - S; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
-    have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+    have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>" (is "?lhs \<le> ?rhs")
if y: "y \<in> {a..b} - S" and yx: "\<bar>y - x\<bar> < d" for y
proof (cases "y < x")
case False
@@ -3255,18 +3210,18 @@
then have Idiff: "?I a y - ?I a x = ?I x y"
using False x by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y-x) *\<^sub>R f x) {x..y}"
-        apply (rule has_integral_diff)
-        using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
-        using has_integral_const_real [of "f x" x y] False
-        apply simp
-        done
-      have "\<And>xa. y - x < d \<Longrightarrow> (\<And>x'. a \<le> x' \<and> x' \<le> b \<and> x' \<notin> S \<Longrightarrow> \<bar>x' - x\<bar> < d \<Longrightarrow> norm (f x' - f x) \<le> e) \<Longrightarrow> 0 < e \<Longrightarrow> xa \<notin> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<notin> S \<Longrightarrow> y \<le> b \<Longrightarrow> y \<notin> S \<Longrightarrow> x \<le> xa \<Longrightarrow> xa \<le> y \<Longrightarrow> norm (f xa - f x) \<le> e"
-        using assms by auto
-      show ?thesis
-        using False
-        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
-        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx False d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
+      proof (rule has_integral_diff)
+        show "(f has_integral integral {x..y} f) {x..y}"
+          using x y by (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+        show "((\<lambda>u. f x) has_integral (y - x) *\<^sub>R f x) {x..y}"
+          using has_integral_const_real [of "f x" x y] False by simp
+      qed
+      have "?lhs \<le> e * content {x..y}"
+        using yx False d x y \<open>e>0\<close> assms
+        by (intro has_integral_bound_real[where f="(\<lambda>u. f u - f x)"]) (auto simp: Idiff fux_int)
+      also have "... \<le> ?rhs"
+        using False by auto
+      finally show ?thesis .
next
case True
have "f integrable_on {a..x}"
@@ -3274,16 +3229,18 @@
then have Idiff: "?I a x - ?I a y = ?I y x"
using True x y by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
-        apply (rule has_integral_diff)
-        using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
-        using has_integral_const_real [of "f x" y x] True
-        apply simp
-        done
-      have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
-        using True
-        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
-        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx True d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
+      proof (rule has_integral_diff)
+        show "(f has_integral integral {y..x} f) {y..x}"
+          using x y by (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
+        show "((\<lambda>u. f x) has_integral (x - y) *\<^sub>R f x) {y..x}"
+          using has_integral_const_real [of "f x" y x] True by simp
+      qed
+      have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * content {y..x}"
+        using yx True d x y \<open>e>0\<close> assms
+        by (intro has_integral_bound_real[where f="(\<lambda>u. f u - f x)"]) (auto simp: Idiff fux_int)
+      also have "... \<le> e * \<bar>y - x\<bar>"
+        using True by auto
+      finally have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>" .
then show ?thesis
qed
@@ -3423,22 +3380,22 @@
using p(6) by auto
then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
-          apply clarsimp
-          by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
+          by clarsimp (metis (no_types, lifting) gh image_eqI pair_imageI)
qed (use gab in auto)
have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
using inj(1) unfolding inj_on_def by fastforce
-      have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
-        using r
-        apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
-        apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
-         apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
-        done
-      also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
+      have "(\<Sum>(x,K)\<in>(\<lambda>(y,L). (g y, g ` L)) ` p. content K *\<^sub>R f x)
+          = (\<Sum>u\<in>p. case case u of (x,K) \<Rightarrow> (g x, g ` K) of (y,L) \<Rightarrow> content L *\<^sub>R f y)"
+        by (metis (mono_tags, lifting) "*" sum.reindex_cong)
+      also have "... = (\<Sum>(x,K)\<in>p. r *\<^sub>R content K *\<^sub>R f (g x))"
+        using r by (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
+      finally
+      have "(\<Sum>(x, K)\<in>(\<lambda>(x,K). (g x, g ` K)) ` p. content K *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - i"
+        by (simp add: scaleR_right.sum split_def)
+      also have "\<dots> = r *\<^sub>R ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)"
using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
-      finally have eq: "?l = ?r" .
-      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
-        using d[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
+      finally show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
+        using d[OF gimp] \<open>0 < r\<close> by auto
qed
qed
then show ?thesis
@@ -3454,8 +3411,8 @@
proof -
interpret finite_product_sigma_finite "\<lambda>_. lborel" Basis
proof qed simp
-
-  have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
+    have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c}
+        = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
using k
by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
(auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
@@ -3520,11 +3477,7 @@
proof (cases "m \<ge> 0")
case True
with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
-      unfolding box_ne_empty
-      apply (intro ballI)
-      apply (erule_tac x=i in ballE)
-      apply (auto simp: inner_simps mult_left_mono)
-      done
+      by (simp add: box_ne_empty inner_left_distrib mult_left_mono)
moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b-a) \<bullet> i"
ultimately show ?thesis
@@ -3533,11 +3486,7 @@
next
case False
with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
-      unfolding box_ne_empty
-      apply (intro ballI)
-      apply (erule_tac x=i in ballE)
-      apply (auto simp: inner_simps mult_left_mono)
-      done
+      by (simp add: box_ne_empty inner_left_distrib mult_left_mono)
moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b-a) \<bullet> i"
ultimately show ?thesis using False
@@ -3550,25 +3499,21 @@
fixes a :: "'a::euclidean_space"
assumes "(f has_integral i) (cbox a b)"
and "m \<noteq> 0"
-  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (\<bar>m\<bar> ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
-  apply (rule has_integral_twiddle)
-  using assms
-  apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox)
-  apply (rule zero_less_power)
-  unfolding scaleR_right_distrib
-  apply auto
-  done
+  shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral (1 / (\<bar>m\<bar> ^ DIM('a))) *\<^sub>R i) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)"
+proof (rule has_integral_twiddle)
+  show "\<exists>w z. (\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox u v = cbox w z"
+       "\<exists>w z. (\<lambda>x. m *\<^sub>R x + c) ` cbox u v = cbox w z" for u v
+    using interval_image_affinity_interval by blast+
+  show "content ((\<lambda>x. m *\<^sub>R x + c) ` cbox u v) = \<bar>m\<bar> ^ DIM('a) * content (cbox u v)" for u v
+    using content_image_affinity_cbox by blast
+qed (use assms zero_less_power in \<open>auto simp: field_simps\<close>)

lemma integrable_affinity:
assumes "f integrable_on cbox a b"
and "m \<noteq> 0"
shows "(\<lambda>x. f(m *\<^sub>R x + c)) integrable_on ((\<lambda>x. (1 / m) *\<^sub>R x + -((1/m) *\<^sub>R c)) ` cbox a b)"
-  using assms
-  unfolding integrable_on_def
-  apply safe
-  apply (drule has_integral_affinity)
-  apply auto
-  done
+  using has_integral_affinity assms
+  unfolding integrable_on_def by blast

lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]

@@ -3660,10 +3605,16 @@
by (force dest: has_integral_stretch)

lemma vec_lambda_eq_sum:
-  shows "(\<chi> k. f k (x \$ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)"
-    apply (simp add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
-    apply (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
-    done
+     "(\<chi> k. f k (x \$ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<chi> k. f k (x \<bullet> axis k 1))"
+  also have "... = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)"
+    by (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
+  also have "... = ?rhs"
+    by (simp add: Basis_vec_def UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
+  finally show ?thesis .
+qed

lemma has_integral_stretch_cart:
fixes m :: "'n::finite \<Rightarrow> real"
@@ -3703,11 +3654,17 @@
lemma uminus_interval_vector[simp]:
fixes a b :: "'a::euclidean_space"
shows "uminus ` cbox a b = cbox (-b) (-a)"
-  apply safe
-  apply (rule_tac x="-x" in image_eqI)
-   apply (auto simp add: mem_box)
-  done
+proof -
+  have "x \<in> uminus ` cbox a b" if "x \<in> cbox (- b) (- a)" for x
+  proof -
+    have "-x \<in> cbox a b"
+      using that by (auto simp: mem_box)
+    then show ?thesis
+      by force
+  qed
+  then show ?thesis
+    by (auto simp: mem_box)
+qed

lemma has_integral_reflect_lemma[intro]:
assumes "(f has_integral i) (cbox a b)"
@@ -3771,22 +3728,20 @@
assume e: "e > 0"
then have eba8: "(e * (b-a)) / 8 > 0"
using ab by (auto simp add: field_simps)
-    note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
+    note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format]
+    thm derf_exp
have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
-      using derf_exp by simp
have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
-      (is "\<forall>x \<in> box a b. ?Q x")
+      (is "\<forall>x \<in> box a b. ?Q x") \<comment>\<open>The explicit quantifier is required by the following step\<close>
proof
-      fix x assume x: "x \<in> box a b"
-      show "?Q x"
-        apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
-        using x e by auto
+      fix x assume "x \<in> box a b"
+      with e show "?Q x"
+        using derf_exp [of x "e/2"] by auto
qed
-    from this [unfolded bgauge_existence_lemma]
-    obtain d where d: "\<And>x. 0 < d x"
-      "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
-               \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
-      by metis
+    then obtain d where d: "\<And>x. 0 < d x"
+      "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk> \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
+      unfolding bgauge_existence_lemma by metis
have "bounded (f ` cbox a b)"
using compact_cbox assms by (auto simp: compact_imp_bounded compact_continuous_image)
then obtain B
@@ -3806,10 +3761,12 @@
case True with ab e that show ?thesis by auto
next
case False
-        then show ?thesis
-          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' a)" in that)
-          using ab e apply (auto simp add: field_simps)
-          done
+        show ?thesis
+        proof
+          show "norm ((e * (b - a) / 8 / norm (f' a)) *\<^sub>R f' a) \<le> e * (b - a) / 8"
+               "0 < e * (b - a) / 8 / norm (f' a)"
+            using False ab e by (auto simp add: field_simps)
+        qed
qed
have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
@@ -3860,9 +3817,12 @@
case True thus ?thesis
using ab e that by auto
next
-        case False then show ?thesis
-          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' b)" in that)
-          using ab e by (auto simp add: field_simps)
+        case False show ?thesis
+        proof
+          show "norm ((e * (b - a) / 8 / norm (f' b)) *\<^sub>R f' b) \<le> e * (b - a) / 8"
+               "0 < e * (b - a) / 8 / norm (f' b)"
+            using False ab e by (auto simp add: field_simps)
+        qed
qed
have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4"
if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
@@ -4006,8 +3966,7 @@
by simp
also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) +
(\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
-              apply (subst sum.union_disjoint)
-              using p(1) ab e by auto
+              using p(1) ab e by (subst sum.union_disjoint) auto
also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
@@ -4095,8 +4054,7 @@
qed
also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
unfolding sum_distrib_left[symmetric]
-          apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
-          by auto
+          by (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag]) auto
finally have norm_le: "norm (\<Sum>(x,K)\<in>p \<inter> {t. fst t \<in> {a, b}}. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
\<le> (\<Sum>n\<in>p. e * (case n of (x, K) \<Rightarrow> Sup K - Inf K))/2" .
have le2: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2)/2 \<Longrightarrow> x - s1 \<le> s2/2"
@@ -4104,8 +4062,7 @@
show ?thesis
apply (rule le2 [OF sum_nonneg])
using ge0 apply force
-          unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
-          by (metis norm_le)
+          by (metis (no_types, lifting) Diff_Diff_Int Diff_subset norm_le p(1) sum.subset_diff)
qed
note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
@@ -4190,8 +4147,7 @@
have e3: "e/3 > 0"
using \<open>e > 0\<close> by auto
have "f integrable_on {a..c}"
-    apply (rule integrable_subinterval_real[OF intf])
-    using \<open>a < c\<close> \<open>c \<le> b\<close> by auto
+    using \<open>a < c\<close> \<open>c \<le> b\<close> by (auto intro: integrable_subinterval_real[OF intf])
then obtain d1 where "gauge d1" and d1:
"\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow> norm (?SUM p - integral {a..c} f) < e/3"
using integrable_integral has_integral_real e3 by metis
@@ -4216,8 +4172,7 @@
next
case True
have "f integrable_on {a..t}"
-        apply (rule integrable_subinterval_real[OF intf])
-        using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
+        using \<open>t < c\<close> \<open>c \<le> b\<close> by (auto intro: integrable_subinterval_real[OF intf])
then obtain d2 where d2: "gauge d2"
"\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
using integrable_integral has_integral_real e3 by metis
@@ -4236,8 +4191,10 @@
have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
using t by (auto simp add: field_simps)
have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
-        apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
-        using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
+      proof (intro tagged_division_Un_interval_real)
+        show "{(c, {t..c})} tagged_division_of {a..c} \<inter> {x. t \<le> x \<bullet> 1}"
+          using \<open>t \<le> c\<close> by (auto simp: eqs tagged_division_of_self_real)
+      qed (auto simp: eqs ptag)
moreover
have "d1 fine p \<union> {(c, {t..c})}"
unfolding fine_def
@@ -4322,8 +4279,7 @@
assume t: "c \<le> t \<and> t < c + ?d"
have *: "integral {a..c} f = integral {a..b} f - integral {c..b} f"
"integral {a..t} f = integral {a..b} f - integral {t..b} f"
-      apply (simp_all only: algebra_simps)
-      using assms t by (auto simp: integral_combine)
+      using assms t by (auto simp: algebra_simps integral_combine)
have "(- c) - d < (- t)" "- t \<le> - c"
using t by auto
from d[OF this] show "norm (integral {a..c} f - integral {a..t} f) < e"
@@ -4348,15 +4304,11 @@
by force
then show ?thesis
proof cases
-      case 1 show ?thesis
-        apply (rule indefinite_integral_continuous_right [OF assms _ \<open>a < b\<close> \<open>e > 0\<close>], force)
-        using \<open>x = a\<close> apply (force simp: dist_norm algebra_simps)
-        done
+      case 1 then show ?thesis
+        by (force simp: dist_norm algebra_simps intro: indefinite_integral_continuous_right [OF assms _ \<open>a < b\<close> \<open>e > 0\<close>])
next
-      case 2 show ?thesis
-        apply (rule indefinite_integral_continuous_left [OF assms \<open>a < b\<close> _ \<open>e > 0\<close>], force)
-        using \<open>x = b\<close> apply (force simp: dist_norm norm_minus_commute algebra_simps)
-        done
+      case 2 then show ?thesis
+        by (force simp: dist_norm norm_minus_commute algebra_simps intro: indefinite_integral_continuous_left [OF assms \<open>a < b\<close> _ \<open>e > 0\<close>])
next
case 3
obtain d1 where "0 < d1"
@@ -4444,7 +4396,7 @@
unfolding has_vector_derivative_def
proof (simp add: at_within_open[OF z, symmetric])
show "(f has_derivative (\<lambda>x. 0)) (at z within {a<..<x})"
-        by (rule has_derivative_within_subset [OF fder]) (use x z notin in auto)
+        by (rule has_derivative_subset [OF fder]) (use x z notin in auto)
qed
qed
from has_integral_unique[OF has_integral_0 this]
@@ -4492,8 +4444,8 @@
if "t \<in> {0..1} - {t. ?\<phi> t \<in> K}" for t
proof -
have df: "(f has_derivative (\<lambda>h. 0)) (at (?\<phi> t) within ?\<phi> ` {0..1})"
-      apply (rule has_derivative_within_subset [OF derf])
-      using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> that by (auto simp add: convex_alt algebra_simps)
+      using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> that
+      by (auto simp add: convex_alt algebra_simps intro: has_derivative_subset [OF derf])
have "(f \<circ> ?\<phi> has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
by (rule derivative_eq_intros df | simp)+
then show ?thesis
@@ -4538,7 +4490,7 @@
using contf continuous_on_subset e by blast
show "(f has_derivative (\<lambda>h. 0)) (at u within ball x e)"
if "u \<in> ball x e - K" for u
-          by (metis Diff_iff contra_subsetD derf e has_derivative_within_subset that)
+          by (metis Diff_iff contra_subsetD derf e has_derivative_subset that)
qed (use y e \<open>0 < e\<close> in auto)
qed
then show "\<exists>e>0. ball x e \<subseteq> (S \<inter> f -` {f x})"
@@ -4716,8 +4668,7 @@
unfolding S using B that
by (force intro: \<open>?l\<close>[unfolded S] has_integral_restrict_closed_subinterval)
then show "?r e"
-      apply (rule_tac x="B+1" in exI)
-      using \<open>B>0\<close> \<open>e>0\<close> by force
+      by (meson \<open>0 < B\<close> \<open>0 < e\<close> add_pos_pos le_less_trans zero_less_one norm_pths(2))
next
assume as: "\<forall>e>0. ?r e"
then obtain C
@@ -4884,12 +4835,11 @@
and as: "S \<subseteq> T" "(f has_integral i) S" "(f has_integral j) T" "\<And>x. x\<in>T \<Longrightarrow> 0 \<le> f(x)\<bullet>k"
shows "i\<bullet>k \<le> j\<bullet>k"
proof -
-  have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
-        "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
+  have \<section>: "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) UNIV"
+          "((\<lambda>x. if x \<in> T then f x else 0) has_integral j) UNIV"
-  then show ?thesis
-    apply (rule has_integral_component_le[OF k])
-    using as by auto
+  show ?thesis
+    using as by (force intro!: has_integral_component_le[OF k \<section>])
qed

subsection\<open>Integrals on set differences\<close>
@@ -4934,16 +4884,15 @@

lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> cbox a b))" (is "?l \<longleftrightarrow> ?r")
proof
-  assume ?r
+  assume R: ?r
show ?l
unfolding negligible_def
proof safe
fix a b
-    show "(indicator s has_integral 0) (cbox a b)"
-      apply (rule has_integral_negligible[OF \<open>?r\<close>[rule_format,of a b]])
-      unfolding indicator_def
-      apply auto
-      done
+    have "negligible (s \<inter> cbox a b)"
+    then show "(indicator s has_integral 0) (cbox a b)"
+      by (meson Diff_iff Int_iff has_integral_negligible indicator_simps(2))
qed

@@ -5061,10 +5010,7 @@
and "f integrable_on t"
and "\<forall>x \<in> t. 0 \<le> f x \<bullet> k"
shows "(integral s f)\<bullet>k \<le> (integral t f)\<bullet>k"
-  apply (rule has_integral_subset_component_le)
-  using assms
-  apply auto
-  done
+  by (meson assms has_integral_subset_component_le integrable_integral)

lemma integral_subset_le:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
@@ -5073,10 +5019,7 @@
and "f integrable_on t"
and "\<forall>x \<in> t. 0 \<le> f x"
shows "integral s f \<le> integral t f"
-  apply (rule has_integral_subset_le)
-  using assms
-  apply auto
-  done
+  using assms has_integral_subset_le by blast

lemma has_integral_alt':
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -5095,8 +5038,7 @@
show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z)
(cbox a b) \<and> norm (z - i) < e)"
-      apply (rule ex_forward)
-      using rhs by blast
+      by (simp add: has_integral_iff rhs)
qed
next
let ?\<Phi> = "\<lambda>e a b. \<exists>z. ((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b) \<and> norm (z - i) < e"
@@ -5424,8 +5366,7 @@
"(?hs has_integral integral (cbox a b) ?hs) (cbox a b)"
by (intro integrable_integral int_g int_h)+
then have "integral (cbox a b) ?gs \<le> integral (cbox a b) ?hs"
-        apply (rule has_integral_le)
-        using fgh by force
+        using fgh by (force intro: has_integral_le)
then have "0 \<le> integral (cbox a b) ?hs - integral (cbox a b) ?gs"
by simp
then have "\<bar>integral (cbox a b) ?hs - integral (cbox a b) ?gs\<bar>
@@ -5435,9 +5376,7 @@
using fgh apply (force simp: eq intro!: integral_subset_le [OF ab_cd int_hg])+
done
then show "\<bar>integral (cbox a b) ?gs - integral (cbox a b) ?hs\<bar> < e"
-        apply (rule **)
-         apply (rule Bg ballBg Bh ballBh)+
-        done
+        using ** Bg ballBg Bh ballBh by blast
show "\<And>x. x \<in> cbox a b \<Longrightarrow> ?gs x \<le> ?fs x" "\<And>x. x \<in> cbox a b \<Longrightarrow> ?fs x \<le> ?hs x"
using fgh by auto
qed
@@ -5564,8 +5503,7 @@
qed
next
show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
-      apply (rule has_integral_sum [OF \<T>])
-      using int by (simp add: has_integral_restrict_UNIV)
+      using int by (simp add: has_integral_restrict_UNIV has_integral_sum [OF \<T>])
qed
then show ?thesis
using has_integral_restrict_UNIV by blast
@@ -5598,8 +5536,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "\<D> division_of S" "\<And>k. k \<in> \<D> \<Longrightarrow> f integrable_on k"
shows "integral S f = sum (\<lambda>i. integral i f) \<D>"
-  apply (rule integral_unique)
-  by (meson assms has_integral_combine_division has_integral_integrable_integral)
+  by (meson assms integral_unique has_integral_combine_division has_integral_integrable_integral)

lemma has_integral_combine_division_topdown:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -5624,11 +5561,7 @@
assumes "f integrable_on S"
and "\<D> division_of S"
shows "integral S f = sum (\<lambda>i. integral i f) \<D>"
-  apply (rule integral_unique)
-  apply (rule has_integral_combine_division_topdown)
-  using assms
-  apply auto
-  done
+  using assms has_integral_combine_division_topdown by blast

lemma integrable_combine_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -5661,15 +5594,16 @@
lemma has_integral_combine_tagged_division:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "p tagged_division_of S"
-    and "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
+    and "\<And>x k. (x,k) \<in> p \<Longrightarrow> (f has_integral (i k)) k"
shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) S"
proof -
have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) S"
-    using assms(2)
-    apply (intro has_integral_combine_division)
-    apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)])
-    apply auto
-    done
+  proof -
+    have "snd ` p division_of S"
+      by (simp add: assms(1) division_of_tagged_division)
+    with assms show ?thesis
+      by (metis (mono_tags, lifting) has_integral_combine_division has_integral_integrable_integral imageE prod.collapse)
+  qed
also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)"
by (intro sum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null)
@@ -5679,14 +5613,10 @@

lemma integral_combine_tagged_division_bottomup:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "p tagged_division_of (cbox a b)"
-    and "\<forall>(x,k)\<in>p. f integrable_on k"
+  assumes p: "p tagged_division_of (cbox a b)"
+    and f: "\<And>x k. (x,k)\<in>p \<Longrightarrow> f integrable_on k"
shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
-  apply (rule integral_unique)
-  apply (rule has_integral_combine_tagged_division[OF assms(1)])
-  using assms(2)
-  apply auto
-  done
+  by (simp add: has_integral_combine_tagged_division[OF p] integral_unique f integrable_integral)

lemma has_integral_combine_tagged_division_topdown:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -5697,7 +5627,7 @@
have "(f has_integral integral K f) K" if "(x,K) \<in> p" for x K
by (metis assms integrable_integral integrable_on_subcbox tagged_division_ofD(3,4) that)
then show ?thesis
-    by (metis assms case_prodI2 has_integral_integrable_integral integral_combine_tagged_division_bottomup)
+    by (simp add: has_integral_combine_tagged_division p)
qed

lemma integral_combine_tagged_division_topdown:
@@ -5705,9 +5635,7 @@
assumes "f integrable_on cbox a b"
and "p tagged_division_of (cbox a b)"
shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
-  apply (rule integral_unique [OF has_integral_combine_tagged_division_topdown])
-  using assms apply auto
-  done
+  using assms by (auto intro: integral_unique [OF has_integral_combine_tagged_division_topdown])

subsection \<open>Henstock's lemma\<close>
@@ -5782,13 +5710,15 @@
by blast
show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
-        have "finite (snd ` p)"
+        have "interior T \<inter> interior (\<Union>(snd ` p)) = {}" if "T \<in> r" for T
+        proof (rule Int_interior_Union_intervals)
+          show "\<And>U. U \<in> snd ` p \<Longrightarrow> \<exists>a b. U = cbox a b"
+            using q q'(4) by blast
+          show "\<And>U. U \<in> snd ` p \<Longrightarrow> interior T \<inter> interior U = {}"
+            by (metis DiffE q q'(5) r_def subsetD that)
+        qed (use p' in auto)
then show "\<And>T. T \<in> r \<Longrightarrow> interior (\<Union>(snd ` p)) \<inter> interior T = {}"
-          apply (subst Int_commute)
-          apply (rule Int_interior_Union_intervals)
-          using r_def q'(5) q(1) apply auto
+          by (metis Int_commute)
qed
qed
moreover have "\<Union>(snd ` p) \<union> \<Union>r = cbox a b" and "{qq i |i. i \<in> r} = qq ` r"
@@ -5838,9 +5768,8 @@
if "K \<in> r" "L \<in> r" "K \<noteq> L" "qq K = qq L" "(x, M) \<in> qq K" for K L x M
using tagged_division_ofD(6) qq that by (metis (no_types, lifting))
ultimately have less_e: "norm (?SUM p + sum (?SUM \<circ> qq) r - integral (cbox a b) f) < e"
-    apply (subst (asm) sum.reindex_nontrivial [OF \<open>finite r\<close>])
-     apply (auto simp: split_paired_all sum.neutral)
-    done
+  proof (subst (asm) sum.reindex_nontrivial [OF \<open>finite r\<close>])
+    qed (auto simp: split_paired_all sum.neutral)
have norm_le: "norm (cp - ip) \<le> e + k"
if "norm ((cp + cr) - i) < e" "norm (cr - ir) < k" "ip + ir = i"
for ir ip i cr cp::'a
@@ -5874,7 +5803,7 @@
then show ?thesis
using uv by blast
qed
-    then have "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
+    then have "(\<Sum>(x, K)\<in>p. integral K f) = (\<Sum>K\<in>snd ` p. integral K f)"
apply (subst sum.reindex_nontrivial [OF \<open>finite p\<close>])
unfolding split_paired_all split_def by auto
then show "(\<Sum>(x, k)\<in>p. integral k f) + (\<Sum>k\<in>r. integral k f) = integral (cbox a b) f"
@@ -5905,8 +5834,7 @@
by (simp add: \<open>d fine p\<close> fine_subset)
show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
apply (rule Henstock_lemma_part1[OF fed less_e, unfolded split_def])
-      using Q tag tagged_partial_division_subset apply (force simp add: fine)+
-      done
+      using Q tag tagged_partial_division_subset by (force simp add: fine)+
qed
qed

@@ -5963,9 +5891,10 @@
have fg1: "(f k x) \<le> (g x)" if x: "x \<in> cbox a b" for x k
proof -
have "\<forall>\<^sub>F j in sequentially. f k x \<le> f j x"
-      apply (rule eventually_sequentiallyI [of k])
-      using le x apply (force intro: transitive_stepwise_le)
-      done
+    proof (rule eventually_sequentiallyI [of k])
+      show "\<And>j. k \<le> j \<Longrightarrow> f k x \<le> f j x"
+        using le x by (force intro: transitive_stepwise_le)
+    qed
then show "f k x \<le> g x"
using tendsto_lowerbound [OF fg] x trivial_limit_sequentially by blast
qed
@@ -6010,14 +5939,9 @@
with fg that LIMSEQ_D
obtain N where "\<forall>n\<ge>N. norm (f n x - g x) < e/(4 * content (cbox a b))"
by metis
-      then show "\<exists>n\<ge>r.
-            \<forall>k\<ge>n.
-               0 \<le> g x - f k x \<and>
-               g x - f k x
-               < e/(4 * content (cbox a b))"
+      then show "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> g x - f k x \<and> g x - f k x < e/(4 * content (cbox a b))"
apply (rule_tac x="N + r" in exI)
-        using fg1[OF that] apply (auto simp add: field_simps)
-        done
+        using fg1[OF that] by (auto simp add: field_simps)
qed
then obtain m where r_le_m: "\<And>x. x \<in> cbox a b \<Longrightarrow> r \<le> m x"
and m: "\<And>x k. \<lbrakk>x \<in> cbox a b; m x \<le> k\<rbrakk>
@@ -6080,8 +6004,10 @@
also have "... \<le> e/2 ^ (t + 2)"
proof (rule Henstock_lemma_part1 [OF intf])
show "{xk \<in> \<D>. m (fst xk) = t} tagged_partial_division_of cbox a b"
-                apply (rule tagged_partial_division_subset[of \<D>])
-                using ptag by (auto simp: tagged_division_of_def)
+              proof (rule tagged_partial_division_subset[of \<D>])
+                show "\<D> tagged_partial_division_of cbox a b"
+                  using ptag tagged_division_of_def by blast
+              qed auto
show "c t fine {xk \<in> \<D>. m (fst xk) = t}"
using \<open>d fine \<D>\<close> by (auto simp: fine_def d_def)
qed (use c e in auto)
@@ -6158,9 +6084,12 @@
for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
proof -
have fg: "(f k x) \<le> (g x)" if "x \<in> S" for x k
-      apply (rule tendsto_lowerbound [OF lim [OF that]])
-      apply (rule eventually_sequentiallyI [of k])
-      using le  by (force intro: transitive_stepwise_le that)+
+    proof -
+      have "\<And>xa. k \<le> xa \<Longrightarrow> f k x \<le> f xa x"
+        using le  by (force intro: transitive_stepwise_le that)
+      then show ?thesis
+        using tendsto_lowerbound [OF lim [OF that]] eventually_sequentiallyI by force
+    qed
obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
have i': "(integral S (f k)) \<le> i" for k
@@ -6171,7 +6100,6 @@
using tendsto_lowerbound [OF i eventually_sequentiallyI trivial_limit_sequentially]
by (meson int_f integral_le)
qed
-
let ?f = "(\<lambda>k x. if x \<in> S then f k x else 0)"
let ?g = "(\<lambda>x. if x \<in> S then g x else 0)"
have int: "?f k integrable_on cbox a b" for a b k
@@ -6230,9 +6158,10 @@
proof (intro ballI integral_le[OF int int])
fix x assume "x \<in> cbox a b"
have "(f m x) \<le> (f n x)" if "x \<in> S" "n \<ge> m" for m n
-              apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
-              using dual_order.trans apply blast
-              by (simp add: le \<open>x \<in> S\<close>)
+            proof (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
+              show "\<And>u y z. \<lbrakk>f u x \<le> f y x; f y x \<le> f z x\<rbrakk> \<Longrightarrow> f u x \<le> f z x"
+                using dual_order.trans by blast
+            qed (simp add: le \<open>x \<in> S\<close>)
then show "(?f N)x \<le> (?f (M+N))x"
by auto
qed
@@ -6474,10 +6403,8 @@
shows "norm (integral S f) \<le> (integral S g)\<bullet>k"
proof -
have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> g)"
-    apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]])
-    apply (metis fg o_def)
-    done
+    using integral_norm_bound_integral[OF f integrable_linear[OF g]]
+    by (simp add: bounded_linear_inner_left fg)
then show ?thesis
unfolding o_def integral_component_eq[OF g] .
qed
@@ -6692,7 +6619,7 @@
if "y \<in> X0 \<inter> U" for y
unfolding has_vector_derivative_def[symmetric]
using that \<open>x \<in> X0\<close>
-          by (intro has_derivative_within_subset[OF fx]) auto
+          by (intro has_derivative_subset[OF fx]) auto
have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
using fx_bound t
by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
@@ -6707,10 +6634,10 @@
also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
by simp
also have "\<dots> < e' * norm (x - x0)"
-        using \<open>e' > 0\<close>
-        apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
-        apply (simp add: divide_simps e_def not_less)
-        done
+      proof (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
+        show "content (cbox a b) * e < e'"
+          using \<open>e' > 0\<close> by (simp add: divide_simps e_def not_less)
+      qed
finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
then show ?case
by (auto simp: divide_simps)
@@ -6736,18 +6663,17 @@
note [continuous_intros] =
continuous_on_compose2[OF cont_fx, where f="\<lambda>y. Pair x y" for x,
unfolded split_beta fst_conv snd_conv]
-  have *: "blinfun_scaleR_left (integral (cbox a b) (fx x0)) =
-    integral (cbox a b) (\<lambda>t. blinfun_scaleR_left (fx x0 t))"
+  show ?thesis
+    unfolding has_vector_derivative_eq_has_derivative_blinfun
+  proof (rule has_derivative_eq_rhs [OF leibniz_rule[OF _ integrable_f2 _ U]])
+    show "continuous_on (U \<times> cbox a b) (\<lambda>(x, t). blinfun_scaleR_left (fx x t))"
+      using cont_fx by (auto simp: split_beta intro!: continuous_intros)
+    show "blinfun_apply (integral (cbox a b) (\<lambda>t. blinfun_scaleR_left (fx x0 t))) =
+          blinfun_apply (blinfun_scaleR_left (integral (cbox a b) (fx x0)))"
by (subst integral_linear[symmetric])
(auto simp: has_vector_derivative_def o_def
intro!: integrable_continuous U continuous_intros bounded_linear_intros)
-  show ?thesis
-    unfolding has_vector_derivative_eq_has_derivative_blinfun
-    apply (rule has_derivative_eq_rhs)
-    apply (rule leibniz_rule[OF _ integrable_f2 _ U, where fx="\<lambda>x t. blinfun_scaleR_left (fx x t)"])
-    using fx cont_fx
-    apply (auto simp: has_vector_derivative_def * split_beta intro!: continuous_intros)
-    done
+    qed (use fx in \<open>auto simp: has_vector_derivative_def\<close>)
qed

lemma has_field_derivative_eq_has_derivative_blinfun:
@@ -6772,11 +6698,15 @@
intro!: integrable_continuous U continuous_intros bounded_linear_intros)
show ?thesis
unfolding has_field_derivative_eq_has_derivative_blinfun
-    apply (rule has_derivative_eq_rhs)
-    apply (rule leibniz_rule[OF _ integrable_f2 _ U, where fx="\<lambda>x t. blinfun_mult_right (fx x t)"])
-    using fx cont_fx
-    apply (auto simp: has_field_derivative_def * split_beta intro!: continuous_intros)
-    done
+  proof (rule has_derivative_eq_rhs [OF leibniz_rule[OF _ integrable_f2 _ U, where fx="\<lambda>x t. blinfun_mult_right (fx x t)"]])
+    show "continuous_on (U \<times> cbox a b) (\<lambda>(x, t). blinfun_mult_right (fx x t))"
+      using cont_fx by (auto simp: split_beta intro!: continuous_intros)
+    show "blinfun_apply (integral (cbox a b) (\<lambda>t. blinfun_mult_right (fx x0 t))) =
+          blinfun_apply (blinfun_mult_right (integral (cbox a b) (fx x0)))"
+      by (subst integral_linear[symmetric])
+        (auto simp: has_vector_derivative_def o_def
+          intro!: integrable_continuous U continuous_intros bounded_linear_intros)
+  qed (use fx in \<open>auto simp: has_field_derivative_def\<close>)
qed

lemma leibniz_rule_field_differentiable:
@@ -7040,11 +6970,12 @@
shows "(\<lambda>y. f (x, y)) integrable_on (cbox c d)"
proof -
have "f \<circ> (\<lambda>y. (x, y)) integrable_on (cbox c d)"
-    apply (rule integrable_continuous)
-    apply (rule continuous_on_compose [OF _ continuous_on_subset [OF con]])
-    using x
-    apply (auto intro: continuous_on_Pair continuous_on_const continuous_on_id continuous_on_subset con)
-    done
+  proof (intro integrable_continuous continuous_on_compose [OF _ continuous_on_subset [OF con]])
+    show "continuous_on (cbox c d) (Pair x)"
+    show "Pair x ` cbox c d \<subseteq> cbox (a,c) (b,d)"
+      using x by blast
+  qed
then show ?thesis
qed
@@ -7071,18 +7002,18 @@
using uc [unfolded uniformly_continuous_on_def, THEN spec, of "e/(2 * content (cbox c d))"]
by (auto simp: dist_norm intro: less_imp_le)
have "\<exists>delta>0. \<forall>x'\<in>cbox a b. norm (x' - x) < delta \<longrightarrow> norm (integral (cbox c d) (\<lambda>u. f (x', u) - f (x, u))) < e"
+      using dd e2_gt assms x
apply (rule_tac x=dd in exI)
-      using dd e2_gt assms x
apply clarify
-      apply (rule le_less_trans [OF _ e2_less])
-      apply (rule integrable_bound)
+      apply (rule le_less_trans [OF integrable_bound e2_less])
apply (auto intro: integrable_diff continuous_on_imp_integrable_on_Pair1)
done
} note * = this
show ?thesis
-    apply (rule integrable_continuous)
-    apply (simp add: * continuous_on_iff dist_norm integral_diff [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
-    done
+  proof (rule integrable_continuous)
+    show "continuous_on (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))"
+      by (simp add: * continuous_on_iff dist_norm integral_diff [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
+  qed
qed

lemma integral_split:
@@ -7092,10 +7023,8 @@
shows "integral (cbox a b) f =
integral (cbox a b \<inter> {x. x\<bullet>k \<le> c}) f +
integral (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) f"
-  apply (rule integral_unique [OF has_integral_split [where c=c]])
using k f
-  apply (auto simp: has_integral_integral [symmetric])
-  done
+  by (auto simp: has_integral_integral intro: integral_unique [OF has_integral_split])

lemma integral_swap_operativeI:
fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
@@ -7158,10 +7087,9 @@
apply (rule norm_diff2 [OF integral_split [where c=M, OF fint ij] * e])
using 1 subs
apply (simp_all add: cbox_Pair_eq setcomp_dot1 [of "\<lambda>u. M\<le>u"] setcomp_dot1 [of "\<lambda>u. u\<le>M"] Sigma_Int_Paircomp1)
-      apply (simp_all add: interval_split ij)
-      apply (simp_all add: cbox_Pair_eq [symmetric] content_Pair [symmetric])
-      apply (force simp add: interval_split [symmetric] intro!: n1 [rule_format])
-      apply (force simp add: interval_split [symmetric] intro!: n2 [rule_format])
+      apply (simp_all add: interval_split ij flip: cbox_Pair_eq content_Pair)
+      apply (force simp flip: interval_split intro!: n1 [rule_format])
+      apply (force simp flip: interval_split intro!: n2 [rule_format])
done
next
case 2
@@ -7170,11 +7098,10 @@
e * (content (cbox u v) * content (cbox w z \<inter> {x. M \<le> x \<bullet> j}))"
by (simp add: content_split [where c=M] content_Pair algebra_simps)
have "(\<lambda>x. integral (cbox w z \<inter> {x. x \<bullet> j \<le> M}) (\<lambda>y. f (x, y))) integrable_on cbox u v"
-                "(\<lambda>x. integral (cbox w z \<inter> {x. M \<le> x \<bullet> j}) (\<lambda>y. f (x, y))) integrable_on cbox u v"
+         "(\<lambda>x. integral (cbox w z \<inter> {x. M \<le> x \<bullet> j}) (\<lambda>y. f (x, y))) integrable_on cbox u v"
using 2 subs
-      apply (rule_tac [!] integral_integrable_2dim [OF continuous_on_subset [OF f]])
-      apply (auto simp: cbox_Pair_eq interval_split [symmetric])
+      apply (rule integral_integrable_2dim [OF continuous_on_subset [OF f]]; auto simp: cbox_Pair_eq interval_split [symmetric])+
done
with 2 have *: "integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) =
integral (cbox u v) (\<lambda>x. integral (cbox w z \<inter> {x. x \<bullet> j \<le> M}) (\<lambda>y. f (x, y))) +
@@ -7185,10 +7112,9 @@
apply (rule norm_diff2 [OF integral_split [where c=M, OF fint ij] * e])
using 2 subs
apply (simp_all add: cbox_Pair_eq setcomp_dot2 [of "\<lambda>u. M\<le>u"] setcomp_dot2 [of "\<lambda>u. u\<le>M"] Sigma_Int_Paircomp2)
-      apply (simp_all add: interval_split ij)
-      apply (simp_all add: cbox_Pair_eq [symmetric] content_Pair [symmetric])
-      apply (force simp add: interval_split [symmetric] intro!: n1 [rule_format])
-      apply (force simp add: interval_split [symmetric] intro!: n2 [rule_format])
+      apply (simp_all add: interval_split ij flip: cbox_Pair_eq content_Pair)
+      apply (force simp flip: interval_split intro!: n1 [rule_format])
+      apply (force simp flip: interval_split intro!: n2 [rule_format])
done
qed
qed
@@ -7278,11 +7204,10 @@
using assms continuous_on_subset uwvz_sub
by (blast intro: continuous_on_imp_integrable_on_Pair1)
have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
-         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
+             \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
+        using cbp \<open>0 < e/content ?CBOX\<close> nf'
apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
-        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
-        using cbp \<open>0 < e/content ?CBOX\<close> nf'
-        apply (auto simp: integrable_diff f_int_uwvz integrable_const)
+        apply (auto simp: integrable_diff f_int_uwvz integrable_const intro: order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
done
have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast
@@ -7290,16 +7215,15 @@
"\<And>x. x \<in> cbox u v \<Longrightarrow>
norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
\<le> e * content (cbox w z) / content (cbox (a, c) (b, d))/2"
+        using cbp \<open>0 < e/content ?CBOX\<close> nf'
apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
-        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
-        using cbp \<open>0 < e/content ?CBOX\<close> nf'
-        apply (auto simp: integrable_diff f_int_uv integrable_const)
+        apply (auto simp: integrable_diff f_int_uv integrable_const intro: order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
done
have "norm (integral (cbox u v)
(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
-        apply (rule integrable_bound [OF _ _ normint_wz])
using cbp \<open>0 < e/content ?CBOX\<close>
+        apply (intro integrable_bound [OF _ _ normint_wz])
apply (auto simp: field_split_simps integrable_diff int_integrable integrable_const)
done
also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
@@ -7322,8 +7246,8 @@
and fine: "(\<lambda>x. ball x k) fine p"
using fine_division_exists \<open>0 < k\<close> by blast
show ?thesis
-        apply (rule op_acbd [OF division_of_tagged_division [OF ptag]])
-        using that fine ptag \<open>0 < k\<close> by (auto simp: *)
+        using that fine ptag \<open>0 < k\<close>
+        by (auto simp: * intro: op_acbd [OF division_of_tagged_division [OF ptag]])
qed
then show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
using compact_uniformly_continuous [OF assms compact_cbox]
@@ -7341,9 +7265,12 @@
shows "integral (cbox (a, c) (b, d)) (\<lambda>(x, y). f x y) = integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)"
proof -
have "((\<lambda>(x, y). f x y) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (prod.swap ` (cbox (c, a) (d, b)))"
-    apply (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
-    apply (force simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)+
-    done
+  proof (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
+    show "\<And>u v. content (prod.swap ` cbox u v) = content (cbox u v)"
+      by (metis content_Pair mult.commute old.prod.exhaust swap_cbox_Pair)
+    show "((\<lambda>(x, y). f y x) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (cbox (c, a) (d, b))"
+      by (simp add: assms integrable_continuous integrable_integral swap_continuous)
+  qed (use isCont_swap in \<open>fastforce+\<close>)
then show ?thesis
by force
qed```
```--- a/src/HOL/Deriv.thy	Sun Oct 11 17:42:32 2020 +0200
+++ b/src/HOL/Deriv.thy	Sun Oct 11 18:46:44 2020 +0100
@@ -238,8 +238,6 @@
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)

-lemmas has_derivative_within_subset = has_derivative_subset
-
lemma has_derivative_within_singleton_iff:
"(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
@@ -415,7 +413,7 @@
assumes "(f has_derivative f') (at x within s)"
shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
using assms
-  by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
+  by (auto intro: has_derivative_subset intro!: has_derivative_in_compose[of f f' x s g])

lemma (in bounded_bilinear) FDERIV:
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
@@ -750,7 +748,7 @@
lemma DERIV_subset:
"(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
(f has_field_derivative f') (at x within t)"
-  by (simp add: has_field_derivative_def has_derivative_within_subset)
+  by (simp add: has_field_derivative_def has_derivative_subset)

lemma has_field_derivative_at_within:
"(f has_field_derivative f') (at x) \<Longrightarrow> (f has_field_derivative f') (at x within s)"```