# HG changeset patch
# User wenzelm
# Date 1378829687 -7200
# Node ID 29af7bb89757714fbc1e11a1b9cf5dbb2289e529
# Parent  3c977c570e20bda96f82c2d85f2b40aa50c9c8e9
tuned proofs;

diff -r 3c977c570e20 -r 29af7bb89757 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 16:09:33 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 10 18:14:47 2013 +0200
@@ -3324,12 +3324,13 @@
   have *: "\<And>(a::'a) b c. content ({a..b} \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
     interior({a..b} \<inter> {x. x\<bullet>k \<le> c}) = {}"
     unfolding  interval_split[OF k] content_eq_0_interior by auto
-  guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
+  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
+  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
   have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
     by auto
   show ?thesis
-    unfolding uv1 uv2 * apply(rule **[OF d(5)[OF assms(2-4)]])
+    unfolding uv1 uv2 *
+    apply (rule **[OF d(5)[OF assms(2-4)]])
     defer
     apply (subst assms(5)[unfolded uv1 uv2])
     unfolding uv1 uv2
@@ -3686,7 +3687,7 @@
         unfolding lem3[OF p(3)]
         apply (subst setsum_reindex_nonzero[OF p(3)])
         defer
-        apply(subst setsum_reindex_nonzero[OF p(3)])
+        apply (subst setsum_reindex_nonzero[OF p(3)])
         defer
         unfolding lem4[symmetric]
         apply (rule refl)
@@ -3903,7 +3904,7 @@
           unfolding interval_split[OF k] b'_def[symmetric] a'_def[symmetric]
           using p
           using assms
-          by (auto simp add:algebra_simps)
+          by (auto simp add: algebra_simps)
       qed
     qed
   qed
@@ -3927,7 +3928,7 @@
       opp (f ({a..b} \<inter> {x. x\<bullet>k \<le> c})) (f ({a..b} \<inter> {x. x\<bullet>k \<ge> c}))"
   using assms unfolding operative_def by auto
 
-lemma operative_trivial: "operative opp f \<Longrightarrow> content({a..b}) = 0 \<Longrightarrow> f({a..b}) = neutral opp"
+lemma operative_trivial: "operative opp f \<Longrightarrow> content {a..b} = 0 \<Longrightarrow> f {a..b} = neutral opp"
   unfolding operative_def by auto
 
 lemma property_empty_interval: "\<forall>a b. content {a..b} = 0 \<longrightarrow> P {a..b} \<Longrightarrow> P {}"
@@ -5180,7 +5181,7 @@
   by auto
 
 lemma has_integral_component_lbound:
-  fixes f :: "'a::ordered_euclidean_space => 'b::ordered_euclidean_space"
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
   assumes "(f has_integral i) {a..b}"
     and "\<forall>x\<in>{a..b}. B \<le> f(x)\<bullet>k"
     and "k \<in> Basis"
@@ -6354,54 +6355,121 @@
   using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)]
   by auto
 
-lemma operative_approximable: assumes "0 \<le> e" fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)" unfolding operative_def neutral_and
+lemma operative_approximable:
+  fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "0 \<le> e"
+  shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
+  unfolding operative_def neutral_and
 proof safe
-  fix a b::"'b"
-  { assume "content {a..b} = 0"
-    thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}"
-      apply(rule_tac x=f in exI) using assms by(auto intro!:integrable_on_null) }
-  { fix c g and k :: 'b
-    assume as:"\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}" and k:"k\<in>Basis"
+  fix a b :: 'b
+  {
+    assume "content {a..b} = 0"
+    then show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}"
+      apply (rule_tac x=f in exI)
+      using assms
+      apply (auto intro!:integrable_on_null)
+      done
+  }
+  {
+    fix c g
+    fix k :: 'b
+    assume as: "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}"
+    assume k: "k \<in> Basis"
     show "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}"
       "\<exists>g. (\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}"
-      apply(rule_tac[!] x=g in exI) using as(1) integrable_split[OF as(2) k] by auto }
-  fix c k g1 g2 assume as:"\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}"
-                          "\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}"
-  assume k:"k\<in>Basis"
+      apply (rule_tac[!] x=g in exI)
+      using as(1) integrable_split[OF as(2) k]
+      apply auto
+      done
+  }
+  fix c k g1 g2
+  assume as: "\<forall>x\<in>{a..b} \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}"
+    "\<forall>x\<in>{a..b} \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on {a..b} \<inter> {x. c \<le> x \<bullet> k}"
+  assume k: "k \<in> Basis"
   let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
-  show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" apply(rule_tac x="?g" in exI)
-  proof safe case goal1 thus ?case apply- apply(cases "x\<bullet>k=c", case_tac "x\<bullet>k < c") using as assms by auto
-  next case goal2 presume "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}"
-    then guess h1 h2 unfolding integrable_on_def by auto from has_integral_split[OF this k]
-    show ?case unfolding integrable_on_def by auto
-  next show "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}"
-      apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]]) using k as(2,4) by auto qed qed
-
-lemma approximable_on_division: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "0 \<le> e" "d division_of {a..b}" "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
+  show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}"
+    apply (rule_tac x="?g" in exI)
+  proof safe
+    case goal1
+    then show ?case
+      apply -
+      apply (cases "x\<bullet>k=c")
+      apply (case_tac "x\<bullet>k < c")
+      using as assms
+      apply auto
+      done
+  next
+    case goal2
+    presume "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}"
+      and "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}"
+    then guess h1 h2 unfolding integrable_on_def by auto
+    from has_integral_split[OF this k] show ?case
+      unfolding integrable_on_def by auto
+  next
+    show "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on {a..b} \<inter> {x. x \<bullet> k \<ge> c}"
+      apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]])
+      using k as(2,4)
+      apply auto
+      done
+  qed
+qed
+
+lemma approximable_on_division:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "0 \<le> e"
+    and "d division_of {a..b}"
+    and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   obtains g where "\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e" "g integrable_on {a..b}"
-proof- note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)]
-  note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]] from assms(3)[unfolded this[of f]]
-  guess g .. thus thesis apply-apply(rule that[of g]) by auto qed
-
-lemma integrable_continuous: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "continuous_on {a..b} f" shows "f integrable_on {a..b}"
-proof(rule integrable_uniform_limit,safe) fix e::real assume e:"0 < e"
+proof -
+  note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)]
+  note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]]
+  from assms(3)[unfolded this[of f]] guess g ..
+  then show thesis
+    apply -
+    apply (rule that[of g])
+    apply auto
+    done
+qed
+
+lemma integrable_continuous:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "continuous_on {a..b} f"
+  shows "f integrable_on {a..b}"
+proof (rule integrable_uniform_limit, safe)
+  fix e :: real
+  assume e: "e > 0"
   from compact_uniformly_continuous[OF assms compact_interval,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d ..
   note d=conjunctD2[OF this,rule_format]
   from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this
   note p' = tagged_division_ofD[OF p(1)]
-  have *:"\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
-  proof(safe,unfold snd_conv) fix x l assume as:"(x,l) \<in> p"
-    from p'(4)[OF this] guess a b apply-by(erule exE)+ note l=this
-    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 show "(\<lambda>y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const)
-      fix y assume y:"y\<in>l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
+  have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
+  proof (safe, unfold snd_conv)
+    fix x l
+    assume as: "(x, l) \<in> p"
+    from p'(4)[OF this] guess a b by (elim exE) note l=this
+    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
+      show "(\<lambda>y. f x) integrable_on l"
+        unfolding integrable_on_def l
+        apply rule
+        apply (rule has_integral_const)
+        done
+      fix y
+      assume y: "y \<in> l"
+      note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
       note d(2)[OF _ _ this[unfolded mem_ball]]
-      thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce qed qed
-  from e have "0 \<le> e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
-  thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" by auto qed
+      then show "norm (f y - f x) \<le> e"
+        using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce
+    qed
+  qed
+  from e have "e \<ge> 0"
+    by auto
+  from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
+  then show "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}"
+    by auto
+qed
+
 
 subsection {* Specialization of additivity to one dimension. *}
 
@@ -6410,374 +6478,978 @@
   and real_inner_1_right: "inner x 1 = x"
   by simp_all
 
-lemma operative_1_lt: assumes "monoidal opp"
+lemma operative_1_lt:
+  assumes "monoidal opp"
   shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and>
-                (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))"
-  apply (simp add: operative_def content_eq_0 less_one)
-proof safe fix a b c::"real" assume as:"\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c}))
-    (f ({a..b} \<inter> {x. c \<le> x}))" "a < c" "c < b"
-    from this(2-) have "{a..b} \<inter> {x. x \<le> c} = {a..c}" "{a..b} \<inter> {x. x \<ge> c} = {c..b}" by auto
-    thus "opp (f {a..c}) (f {c..b}) = f {a..b}" unfolding as(1)[rule_format,of a b "c"] by auto
-next fix a b c::real
-  assume as:"\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp" "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
+    (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}))"
+  apply (simp add: operative_def content_eq_0)
+proof safe
+  fix a b c :: real
+  assume as:
+    "\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> {x. c \<le> x}))"
+    "a < c"
+    "c < b"
+    from this(2-) have "{a..b} \<inter> {x. x \<le> c} = {a..c}" "{a..b} \<inter> {x. x \<ge> c} = {c..b}"
+      by auto
+    then show "opp (f {a..c}) (f {c..b}) = f {a..b}"
+      unfolding as(1)[rule_format,of a b "c"] by auto
+next
+  fix a b c :: real
+  assume as: "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp"
+    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
   show "f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> {x. c \<le> x}))"
-  proof(cases "c \<in> {a .. b}")
-    case False hence "c<a \<or> c>b" by auto
-    thus ?thesis apply-apply(erule disjE)
-    proof- assume "c<a" hence *:"{a..b} \<inter> {x. x \<le> c} = {1..0}"  "{a..b} \<inter> {x. c \<le> x} = {a..b}" by auto
-      show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto
-    next   assume "b<c" hence *:"{a..b} \<inter> {x. x \<le> c} = {a..b}"  "{a..b} \<inter> {x. c \<le> x} = {1..0}" by auto
-      show ?thesis unfolding * apply(subst as(1)[rule_format,of 0 1]) using assms by auto
+  proof (cases "c \<in> {a..b}")
+    case False
+    then have "c < a \<or> c > b" by auto
+    then show ?thesis
+    proof
+      assume "c < a"
+      then have *: "{a..b} \<inter> {x. x \<le> c} = {1..0}" "{a..b} \<inter> {x. c \<le> x} = {a..b}"
+        by auto
+      show ?thesis
+        unfolding *
+        apply (subst as(1)[rule_format,of 0 1])
+        using assms
+        apply auto
+        done
+    next
+      assume "b < c"
+      then have *: "{a..b} \<inter> {x. x \<le> c} = {a..b}" "{a..b} \<inter> {x. c \<le> x} = {1..0}"
+        by auto
+      show ?thesis
+        unfolding *
+        apply (subst as(1)[rule_format,of 0 1])
+        using assms
+        apply auto
+        done
     qed
-  next case True hence *:"min (b) c = c" "max a c = c" by auto
-    have **: "(1::real) \<in> Basis" by simp
-    have ***:"\<And>P Q. (\<Sum>i\<in>Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)"
+  next
+    case True
+    then have *: "min (b) c = c" "max a c = c"
+      by auto
+    have **: "(1::real) \<in> Basis"
+      by simp
+    have ***: "\<And>P Q. (\<Sum>i\<in>Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)"
       by simp
     show ?thesis
       unfolding interval_split[OF **, unfolded real_inner_1_right] unfolding *** *
-    proof(cases "c = a \<or> c = b")
-      case False thus "f {a..b} = opp (f {a..c}) (f {c..b})"
-        apply-apply(subst as(2)[rule_format]) using True by auto
-    next case True thus "f {a..b} = opp (f {a..c}) (f {c..b})" apply-
-      proof(erule disjE) assume *:"c=a"
-        hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto
-        thus ?thesis using assms unfolding * by auto
-      next assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto
-        thus ?thesis using assms unfolding * by auto qed qed qed qed
-
-lemma operative_1_le: assumes "monoidal opp"
+    proof (cases "c = a \<or> c = b")
+      case False
+      then show "f {a..b} = opp (f {a..c}) (f {c..b})"
+        apply -
+        apply (subst as(2)[rule_format])
+        using True
+        apply auto
+        done
+    next
+      case True
+      then show "f {a..b} = opp (f {a..c}) (f {c..b})"
+      proof
+        assume *: "c = a"
+        then have "f {a..c} = neutral opp"
+          apply -
+          apply (rule as(1)[rule_format])
+          apply auto
+          done
+        then show ?thesis
+          using assms unfolding * by auto
+      next
+        assume *: "c = b"
+        then have "f {c..b} = neutral opp"
+          apply -
+          apply (rule as(1)[rule_format])
+          apply auto
+          done
+        then show ?thesis
+          using assms unfolding * by auto
+      qed
+    qed
+  qed
+qed
+
+lemma operative_1_le:
+  assumes "monoidal opp"
   shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and>
-                (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))"
-unfolding operative_1_lt[OF assms]
-proof safe fix a b c::"real" assume as:"\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" "a < c" "c < b"
-  show "opp (f {a..c}) (f {c..b}) = f {a..b}" apply(rule as(1)[rule_format]) using as(2-) by auto
-next fix a b c ::"real" assume "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp"
-    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}" "a \<le> c" "c \<le> b"
+    (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}))"
+  unfolding operative_1_lt[OF assms]
+proof safe
+  fix a b c :: real
+  assume as:
+    "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
+    "a < c"
+    "c < b"
+  show "opp (f {a..c}) (f {c..b}) = f {a..b}"
+    apply (rule as(1)[rule_format])
+    using as(2-)
+    apply auto
+    done
+next
+  fix a b c :: real
+  assume "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp"
+    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
+    and "a \<le> c"
+    and "c \<le> b"
   note as = this[rule_format]
   show "opp (f {a..c}) (f {c..b}) = f {a..b}"
-  proof(cases "c = a \<or> c = b")
-    case False thus ?thesis apply-apply(subst as(2)) using as(3-) by(auto)
-    next case True thus ?thesis apply-
-      proof(erule disjE) assume *:"c=a" hence "f {a..c} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto
-        thus ?thesis using assms unfolding * by auto
-      next               assume *:"c=b" hence "f {c..b} = neutral opp" apply-apply(rule as(1)[rule_format]) by auto
-        thus ?thesis using assms unfolding * by auto qed qed qed
+  proof (cases "c = a \<or> c = b")
+    case False
+    then show ?thesis
+      apply -
+      apply (subst as(2))
+      using as(3-)
+      apply auto
+      done
+  next
+    case True
+    then show ?thesis
+    proof
+      assume *: "c = a"
+      then have "f {a..c} = neutral opp"
+        apply -
+        apply (rule as(1)[rule_format])
+        apply auto
+        done
+      then show ?thesis
+        using assms unfolding * by auto
+    next
+      assume *: "c = b"
+      then have "f {c..b} = neutral opp"
+        apply -
+        apply (rule as(1)[rule_format])
+        apply auto
+        done
+      then show ?thesis
+        using assms unfolding * by auto
+    qed
+  qed
+qed
+
 
 subsection {* Special case of additivity we need for the FCT. *}
 
-lemma interval_bound_sing[simp]: "interval_upperbound {a} = a"  "interval_lowerbound {a} = a"
-  unfolding interval_upperbound_def interval_lowerbound_def by (auto simp: euclidean_representation)
-
-lemma additive_tagged_division_1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
-  assumes "a \<le> b" "p tagged_division_of {a..b}"
+lemma interval_bound_sing[simp]:
+  "interval_upperbound {a} = a"
+  "interval_lowerbound {a} = a"
+  unfolding interval_upperbound_def interval_lowerbound_def
+  by (auto simp: euclidean_representation)
+
+lemma additive_tagged_division_1:
+  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+  assumes "a \<le> b"
+    and "p tagged_division_of {a..b}"
   shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
-proof- let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
-  have ***:"\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" using assms by auto
-  have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto
-  have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
+proof -
+  let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
+  have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
+    using assms by auto
+  have *: "operative op + ?f"
+    unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty by auto
+  have **: "{a..b} \<noteq> {}"
+    using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
   note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
-  show ?thesis unfolding * apply(subst setsum_iterate[symmetric]) defer
-    apply(rule setsum_cong2) unfolding split_paired_all split_conv using assms(2) by auto qed
+  show ?thesis
+    unfolding *
+    apply (subst setsum_iterate[symmetric])
+    defer
+    apply (rule setsum_cong2)
+    unfolding split_paired_all split_conv
+    using assms(2)
+    apply auto
+    done
+qed
+
 
 subsection {* A useful lemma allowing us to factor out the content size. *}
 
 lemma has_integral_factor_content:
-  "(f has_integral i) {a..b} \<longleftrightarrow> (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p
-    \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a..b}))"
-proof(cases "content {a..b} = 0")
-  case True show ?thesis unfolding has_integral_null_eq[OF True] apply safe
-    apply(rule,rule,rule gauge_trivial,safe) unfolding setsum_content_null[OF True] True defer
-    apply(erule_tac x=1 in allE,safe) defer apply(rule fine_division_exists[of _ a b],assumption)
-    apply(erule_tac x=p in allE) unfolding setsum_content_null[OF True] by auto
-next case False note F = this[unfolded content_lt_nz[symmetric]]
-  let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {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 fix e::real assume e:"e>0"
-    { assume "\<forall>e>0. ?P e op <" thus "?P (e * content {a..b}) op \<le>" apply(erule_tac x="e * content {a..b}" in allE)
-        apply(erule impE) defer apply(erule exE,rule_tac x=d in exI)
-        using F e by(auto simp add:field_simps intro:mult_pos_pos) }
-    {  assume "\<forall>e>0. ?P (e * content {a..b}) op \<le>" thus "?P e op <" apply(erule_tac x="e / 2 / content {a..b}" in allE)
-        apply(erule impE) defer apply(erule exE,rule_tac x=d in exI)
-        using F e by(auto simp add:field_simps intro:mult_pos_pos) } qed qed
+  "(f has_integral i) {a..b} \<longleftrightarrow>
+    (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
+      norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content {a..b}))"
+proof (cases "content {a..b} = 0")
+  case True
+  show ?thesis
+    unfolding has_integral_null_eq[OF True]
+    apply safe
+    apply (rule, rule, rule gauge_trivial, safe)
+    unfolding setsum_content_null[OF True] True
+    defer
+    apply (erule_tac x=1 in allE)
+    apply safe
+    defer
+    apply (rule fine_division_exists[of _ a b])
+    apply assumption
+    apply (erule_tac x=p in allE)
+    unfolding setsum_content_null[OF True]
+    apply auto
+    done
+next
+  case False
+  note F = this[unfolded content_lt_nz[symmetric]]
+  let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and>
+    (\<forall>p. p tagged_division_of {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
+    fix e :: real
+    assume e: "e > 0"
+    {
+      assume "\<forall>e>0. ?P e op <"
+      then show "?P (e * content {a..b}) op \<le>"
+        apply (erule_tac x="e * content {a..b}" in allE)
+        apply (erule impE)
+        defer
+        apply (erule exE,rule_tac x=d in exI)
+        using F e
+        apply (auto simp add:field_simps intro:mult_pos_pos)
+        done
+    }
+    {
+      assume "\<forall>e>0. ?P (e * content {a..b}) op \<le>"
+      then show "?P e op <"
+        apply (erule_tac x="e / 2 / content {a..b}" in allE)
+        apply (erule impE)
+        defer
+        apply (erule exE,rule_tac x=d in exI)
+        using F e
+        apply (auto simp add: field_simps intro: mult_pos_pos)
+        done
+    }
+  qed
+qed
+
 
 subsection {* Fundamental theorem of calculus. *}
 
-lemma interval_bounds_real: assumes "a\<le>(b::real)"
-  shows "interval_upperbound {a..b} = b" "interval_lowerbound {a..b} = a"
-  apply(rule_tac[!] interval_bounds) using assms by auto
-
-lemma fundamental_theorem_of_calculus: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "a \<le> b"  "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
-  shows "(f' has_integral (f b - f a)) ({a..b})"
-unfolding has_integral_factor_content
-proof safe fix e::real assume e:"e>0"
+lemma interval_bounds_real:
+  fixes q b :: real
+  assumes "a \<le> b"
+  shows "interval_upperbound {a..b} = b"
+    and "interval_lowerbound {a..b} = a"
+  apply (rule_tac[!] interval_bounds)
+  using assms
+  apply auto
+  done
+
+lemma fundamental_theorem_of_calculus:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "a \<le> b"
+    and "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
+  shows "(f' has_integral (f b - f a)) {a..b}"
+  unfolding has_integral_factor_content
+proof safe
+  fix e :: real
+  assume e: "e > 0"
   note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt]
-  have *:"\<And>P Q. \<forall>x\<in>{a..b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a..b} \<longrightarrow> Q x e d" using e by blast
-  note this[OF assm,unfolded gauge_existence_lemma] from choice[OF this,unfolded Ball_def[symmetric]]
-  guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
+  have *: "\<And>P Q. \<forall>x\<in>{a..b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a..b} \<longrightarrow> Q x e d"
+    using e by blast
+  note this[OF assm,unfolded gauge_existence_lemma]
+  from choice[OF this,unfolded Ball_def[symmetric]] guess d ..
+  note d=conjunctD2[OF this[rule_format],rule_format]
   show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
-                 norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
-    apply(rule_tac x="\<lambda>x. ball x (d x)" in exI,safe)
-    apply(rule gauge_ball_dependent,rule,rule d(1))
-  proof- fix p assume as:"p tagged_division_of {a..b}" "(\<lambda>x. ball x (d x)) fine p"
+    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
+    apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
+    apply safe
+    apply (rule gauge_ball_dependent)
+    apply rule
+    apply (rule d(1))
+  proof -
+    fix p
+    assume as: "p tagged_division_of {a..b}" "(\<lambda>x. ball x (d x)) fine p"
     show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
       unfolding content_real[OF assms(1)] additive_tagged_division_1[OF assms(1) as(1),of f,symmetric]
       unfolding additive_tagged_division_1[OF assms(1) as(1),of "\<lambda>x. x",symmetric]
-      unfolding setsum_right_distrib defer unfolding setsum_subtractf[symmetric]
-    proof(rule setsum_norm_le,safe) fix x k assume "(x,k)\<in>p"
-      note xk = tagged_division_ofD(2-4)[OF as(1) this] from this(3) guess u v apply-by(erule exE)+ note k=this
-      have *:"u \<le> v" using xk unfolding k by auto
-      have ball:"\<forall>xa\<in>k. xa \<in> ball x (d x)" using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`,
-        unfolded split_conv subset_eq] .
+      unfolding setsum_right_distrib
+      defer
+      unfolding setsum_subtractf[symmetric]
+    proof (rule setsum_norm_le,safe)
+      fix x k
+      assume "(x, k) \<in> p"
+      note xk = tagged_division_ofD(2-4)[OF as(1) this]
+      from this(3) guess u v by (elim exE) note k=this
+      have *: "u \<le> v"
+        using xk unfolding k by auto
+      have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
+        using as(2)[unfolded fine_def,rule_format,OF `(x,k)\<in>p`,unfolded split_conv subset_eq] .
       have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
         norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
-        apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm])
-        unfolding scaleR_diff_left by(auto simp add:algebra_simps)
-      also have "... \<le> e * norm (u - x) + e * norm (v - x)"
-        apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4
-        apply(rule d(2)[of "x" "v",unfolded o_def])
+        apply (rule order_trans[OF _ norm_triangle_ineq4])
+        apply (rule eq_refl)
+        apply (rule arg_cong[where f=norm])
+        unfolding scaleR_diff_left
+        apply (auto simp add:algebra_simps)
+        done
+      also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
+        apply (rule add_mono)
+        apply (rule d(2)[of "x" "u",unfolded o_def])
+        prefer 4
+        apply (rule d(2)[of "x" "v",unfolded o_def])
         using ball[rule_format,of u] ball[rule_format,of v]
-        using xk(1-2) unfolding k subset_eq by(auto simp add:dist_real_def)
-      also have "... \<le> e * (interval_upperbound k - interval_lowerbound k)"
-        unfolding k interval_bounds_real[OF *] using xk(1) unfolding k by(auto simp add:dist_real_def field_simps)
+        using xk(1-2)
+        unfolding k subset_eq
+        apply (auto simp add:dist_real_def)
+        done
+      also have "\<dots> \<le> e * (interval_upperbound k - interval_lowerbound k)"
+        unfolding k interval_bounds_real[OF *]
+        using xk(1)
+        unfolding k
+        by (auto simp add: dist_real_def field_simps)
       finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \<le>
-        e * (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bounds_real[OF *] content_real[OF *] .
-    qed qed qed
+        e * (interval_upperbound k - interval_lowerbound k)"
+        unfolding k interval_bounds_real[OF *] content_real[OF *] .
+    qed
+  qed
+qed
+
 
 subsection {* Attempt a systematic general set of "offset" results for components. *}
 
 lemma gauge_modify:
   assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
-  using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE)
-  apply(erule_tac x="d (f x)" in allE) by auto
+  using assms
+  unfolding gauge_def
+  apply safe
+  defer
+  apply (erule_tac x="f x" in allE)
+  apply (erule_tac x="d (f x)" in allE)
+  apply auto
+  done
+
 
 subsection {* Only need trivial subintervals if the interval itself is trivial. *}
 
-lemma division_of_nontrivial: fixes s::"('a::ordered_euclidean_space) set set"
-  assumes "s division_of {a..b}" "content({a..b}) \<noteq> 0"
-  shows "{k. k \<in> s \<and> content k \<noteq> 0} division_of {a..b}" using assms(1) apply-
-proof(induct "card s" arbitrary:s rule:nat_less_induct)
-  fix s::"'a set set" assume assm:"s division_of {a..b}"
-    "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow> x division_of {a..b} \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of {a..b}"
-  note s = division_ofD[OF assm(1)] let ?thesis = "{k \<in> s. content k \<noteq> 0} division_of {a..b}"
-  { presume *:"{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis"
-    show ?thesis apply cases defer apply(rule *,assumption) using assm(1) by auto }
-  assume noteq:"{k \<in> s. content k \<noteq> 0} \<noteq> s"
-  then obtain k where k:"k\<in>s" "content k = 0" by auto
-  from s(4)[OF k(1)] guess c d apply-by(erule exE)+ note k=k this
-  from k have "card s > 0" unfolding card_gt_0_iff using assm(1) by auto
-  hence card:"card (s - {k}) < card s" using assm(1) k(1) apply(subst card_Diff_singleton_if) by auto
-  have *:"closed (\<Union>(s - {k}))" apply(rule closed_Union) defer apply rule apply(drule DiffD1,drule s(4))
-    apply safe apply(rule closed_interval) using assm(1) by auto
-  have "k \<subseteq> \<Union>(s - {k})" apply safe apply(rule *[unfolded closed_limpt,rule_format]) unfolding islimpt_approachable
-  proof safe fix x and e::real assume as:"x\<in>k" "e>0"
+lemma division_of_nontrivial:
+  fixes s :: "'a::ordered_euclidean_space set set"
+  assumes "s division_of {a..b}"
+    and "content {a..b} \<noteq> 0"
+  shows "{k. k \<in> s \<and> content k \<noteq> 0} division_of {a..b}"
+  using assms(1)
+  apply -
+proof (induct "card s" arbitrary: s rule: nat_less_induct)
+  fix s::"'a set set"
+  assume assm: "s division_of {a..b}"
+    "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow>
+      x division_of {a..b} \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of {a..b}"
+  note s = division_ofD[OF assm(1)]
+  let ?thesis = "{k \<in> s. content k \<noteq> 0} division_of {a..b}"
+  {
+    presume *: "{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      defer
+      apply (rule *)
+      apply assumption
+      using assm(1)
+      apply auto
+      done
+  }
+  assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
+  then obtain k where k: "k \<in> s" "content k = 0"
+    by auto
+  from s(4)[OF k(1)] guess c d by (elim exE) note k=k this
+  from k have "card s > 0"
+    unfolding card_gt_0_iff using assm(1) by auto
+  then have card: "card (s - {k}) < card s"
+    using assm(1) k(1)
+    apply (subst card_Diff_singleton_if)
+    apply auto
+    done
+  have *: "closed (\<Union>(s - {k}))"
+    apply (rule closed_Union)
+    defer
+    apply rule
+    apply (drule DiffD1,drule s(4))
+    apply safe
+    apply (rule closed_interval)
+    using assm(1)
+    apply auto
+    done
+  have "k \<subseteq> \<Union>(s - {k})"
+    apply safe
+    apply (rule *[unfolded closed_limpt,rule_format])
+    unfolding islimpt_approachable
+  proof safe
+    fix x
+    fix e :: real
+    assume as: "x \<in> k" "e > 0"
     from k(2)[unfolded k content_eq_0] guess i ..
-    hence i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis" using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto
-    hence xi:"x\<bullet>i = d\<bullet>i" using as unfolding k mem_interval by (metis antisym)
-    def y \<equiv> "(\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
-      min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)::'a"
-    show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x=y in bexI)
-    proof have "d \<in> {c..d}" using s(3)[OF k(1)] unfolding k interval_eq_empty mem_interval by(fastforce simp add: not_less)
-      hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN bspec[where x=i]]
-      hence xyi:"y\<bullet>i \<noteq> x\<bullet>i"
-        unfolding y_def i xi using as(2) assms(2)[unfolded content_eq_0] i(2)
+    then have i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis"
+      using s(3)[OF k(1),unfolded k] unfolding interval_ne_empty by auto
+    then have xi: "x\<bullet>i = d\<bullet>i"
+      using as unfolding k mem_interval by (metis antisym)
+    def y \<equiv> "\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
+      min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j"
+    show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e"
+      apply (rule_tac x=y in bexI)
+    proof
+      have "d \<in> {c..d}"
+        using s(3)[OF k(1)]
+        unfolding k interval_eq_empty mem_interval
+        by (fastforce simp add: not_less)
+      then have "d \<in> {a..b}"
+        using s(2)[OF k(1)]
+        unfolding k
+        by auto
+      note di = this[unfolded mem_interval,THEN bspec[where x=i]]
+      then have xyi: "y\<bullet>i \<noteq> x\<bullet>i"
+        unfolding y_def i xi
+        using as(2) assms(2)[unfolded content_eq_0] i(2)
         by (auto elim!: ballE[of _ _ i])
-      thus "y \<noteq> x" unfolding euclidean_eq_iff[where 'a='a] using i by auto
-      have *:"Basis = insert i (Basis - {i})" using i by auto
-      have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis" apply(rule le_less_trans[OF norm_le_l1])
-        apply(subst *,subst setsum_insert) prefer 3 apply(rule add_less_le_mono)
-      proof-
+      then show "y \<noteq> x"
+        unfolding euclidean_eq_iff[where 'a='a] using i by auto
+      have *: "Basis = insert i (Basis - {i})"
+        using i by auto
+      have "norm (y - x) < e + setsum (\<lambda>i. 0) Basis"
+        apply (rule le_less_trans[OF norm_le_l1])
+        apply (subst *)
+        apply (subst setsum_insert)
+        prefer 3
+        apply (rule add_less_le_mono)
+      proof -
         show "\<bar>(y - x) \<bullet> i\<bar> < e"
           using di as(2) y_def i xi by (auto simp: inner_simps)
         show "(\<Sum>i\<in>Basis - {i}. \<bar>(y - x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
           unfolding y_def by (auto simp: inner_simps)
-      qed auto thus "dist y x < e" unfolding dist_norm by auto
-      have "y\<notin>k" unfolding k mem_interval apply rule apply(erule_tac x=i in ballE) using xyi k i xi by auto
-      moreover have "y \<in> \<Union>s"
-        using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i unfolding s mem_interval y_def
+      qed auto
+      then show "dist y x < e"
+        unfolding dist_norm by auto
+      have "y \<notin> k"
+        unfolding k mem_interval
+        apply rule
+        apply (erule_tac x=i in ballE)
+        using xyi k i xi
+        apply auto
+        done
+      moreover
+      have "y \<in> \<Union>s"
+        using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i
+        unfolding s mem_interval y_def
         by (auto simp: field_simps elim!: ballE[of _ _ i])
-      ultimately show "y \<in> \<Union>(s - {k})" by auto
-    qed qed hence "\<Union>(s - {k}) = {a..b}" unfolding s(6)[symmetric] by auto
-  hence  "{ka \<in> s - {k}. content ka \<noteq> 0} division_of {a..b}" apply-apply(rule assm(2)[rule_format,OF card refl])
-    apply(rule division_ofI) defer apply(rule_tac[1-4] s) using assm(1) by auto
-  moreover have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}" using k by auto ultimately show ?thesis by auto qed
+      ultimately
+      show "y \<in> \<Union>(s - {k})" by auto
+    qed
+  qed
+  then have "\<Union>(s - {k}) = {a..b}"
+    unfolding s(6)[symmetric] by auto
+  then have  "{ka \<in> s - {k}. content ka \<noteq> 0} division_of {a..b}"
+    apply -
+    apply (rule assm(2)[rule_format,OF card refl])
+    apply (rule division_ofI)
+    defer
+    apply (rule_tac[1-4] s)
+    using assm(1)
+    apply auto
+    done
+  moreover
+  have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}"
+    using k by auto
+  ultimately show ?thesis by auto
+qed
+
 
 subsection {* Integrability on subintervals. *}
 
-lemma operative_integrable: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach" shows
-  "operative op \<and> (\<lambda>i. f integrable_on i)"
-  unfolding operative_def neutral_and apply safe apply(subst integrable_on_def)
-  unfolding has_integral_null_eq apply(rule,rule refl) apply(rule,assumption,assumption)+
-  unfolding integrable_on_def by(auto intro!: has_integral_split)
-
-lemma integrable_subinterval: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on {a..b}" "{c..d} \<subseteq> {a..b}" shows "f integrable_on {c..d}"
-  apply(cases "{c..d} = {}") defer apply(rule partial_division_extend_1[OF assms(2)],assumption)
-  using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1) by auto
+lemma operative_integrable:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  shows "operative op \<and> (\<lambda>i. f integrable_on i)"
+  unfolding operative_def neutral_and
+  apply safe
+  apply (subst integrable_on_def)
+  unfolding has_integral_null_eq
+  apply (rule, rule refl)
+  apply (rule, assumption, assumption)+
+  unfolding integrable_on_def
+  by (auto intro!: has_integral_split)
+
+lemma integrable_subinterval:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "f integrable_on {a..b}"
+    and "{c..d} \<subseteq> {a..b}"
+  shows "f integrable_on {c..d}"
+  apply (cases "{c..d} = {}")
+  defer
+  apply (rule partial_division_extend_1[OF assms(2)],assumption)
+  using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1)
+  apply auto
+  done
+
 
 subsection {* Combining adjacent intervals in 1 dimension. *}
 
-lemma has_integral_combine: assumes "(a::real) \<le> c" "c \<le> b"
-  "(f has_integral i) {a..c}" "(f has_integral (j::'a::banach)) {c..b}"
+lemma has_integral_combine:
+  fixes a b c :: real
+  assumes "a \<le> c"
+    and "c \<le> b"
+    and "(f has_integral i) {a..c}"
+    and "(f has_integral (j::'a::banach)) {c..b}"
   shows "(f has_integral (i + j)) {a..b}"
-proof- note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]]
-  note conjunctD2[OF this,rule_format] note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]]
-  hence "f integrable_on {a..b}" apply- apply(rule ccontr) apply(subst(asm) if_P) defer
-    apply(subst(asm) if_P) using assms(3-) by auto
-  with * show ?thesis apply-apply(subst(asm) if_P) defer apply(subst(asm) if_P) defer apply(subst(asm) if_P)
-    unfolding lifted.simps using assms(3-) by(auto simp add: integrable_on_def integral_unique) qed
-
-lemma integral_combine: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "a \<le> c" "c \<le> b" "f integrable_on ({a..b})"
-  shows "integral {a..c} f + integral {c..b} f = integral({a..b}) f"
-  apply(rule integral_unique[symmetric]) apply(rule has_integral_combine[OF assms(1-2)])
-  apply(rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+ using assms(1-2) by auto
-
-lemma integrable_combine: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "a \<le> c" "c \<le> b" "f integrable_on {a..c}" "f integrable_on {c..b}"
-  shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by(fastforce intro!:has_integral_combine)
+proof -
+  note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]]
+  note conjunctD2[OF this,rule_format]
+  note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]]
+  then have "f integrable_on {a..b}"
+    apply -
+    apply (rule ccontr)
+    apply (subst(asm) if_P)
+    defer
+    apply (subst(asm) if_P)
+    using assms(3-)
+    apply auto
+    done
+  with *
+  show ?thesis
+    apply -
+    apply (subst(asm) if_P)
+    defer
+    apply (subst(asm) if_P)
+    defer
+    apply (subst(asm) if_P)
+    unfolding lifted.simps
+    using assms(3-)
+    apply (auto simp add: integrable_on_def integral_unique)
+    done
+qed
+
+lemma integral_combine:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "a \<le> c"
+    and "c \<le> b"
+    and "f integrable_on {a..b}"
+  shows "integral {a..c} f + integral {c..b} f = integral {a..b} f"
+  apply (rule integral_unique[symmetric])
+  apply (rule has_integral_combine[OF assms(1-2)])
+  apply (rule_tac[!] integrable_integral integrable_subinterval[OF assms(3)])+
+  using assms(1-2)
+  apply auto
+  done
+
+lemma integrable_combine:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "a \<le> c"
+    and "c \<le> b"
+    and "f integrable_on {a..c}"
+    and "f integrable_on {c..b}"
+  shows "f integrable_on {a..b}"
+  using assms
+  unfolding integrable_on_def
+  by (fastforce intro!:has_integral_combine)
+
 
 subsection {* Reduce integrability to "local" integrability. *}
 
-lemma integrable_on_little_subintervals: fixes f::"'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "\<forall>x\<in>{a..b}. \<exists>d>0. \<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> f integrable_on {u..v}"
+lemma integrable_on_little_subintervals:
+  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "\<forall>x\<in>{a..b}. \<exists>d>0. \<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow>
+    f integrable_on {u..v}"
   shows "f integrable_on {a..b}"
-proof- have "\<forall>x. \<exists>d. x\<in>{a..b} \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow> f integrable_on {u..v})"
-    using assms by auto note this[unfolded gauge_existence_lemma] from choice[OF this] guess d .. note d=this[rule_format]
-  guess p apply(rule fine_division_exists[OF gauge_ball_dependent,of d a b]) using d by auto note p=this(1-2)
-  note division_of_tagged_division[OF this(1)] note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f]
-  show ?thesis unfolding * apply safe unfolding snd_conv
-  proof- fix x k assume "(x,k) \<in> p" note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this]
-    thus "f integrable_on k" apply safe apply(rule d[THEN conjunct2,rule_format,of x]) by auto qed qed
+proof -
+  have "\<forall>x. \<exists>d. x\<in>{a..b} \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> {u..v} \<and> {u..v} \<subseteq> ball x d \<and> {u..v} \<subseteq> {a..b} \<longrightarrow>
+    f integrable_on {u..v})"
+    using assms by auto
+  note this[unfolded gauge_existence_lemma]
+  from choice[OF this] guess d .. note d=this[rule_format]
+  guess p
+    apply (rule fine_division_exists[OF gauge_ball_dependent,of d a b])
+    using d
+    by auto
+  note p=this(1-2)
+  note division_of_tagged_division[OF this(1)]
+  note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f]
+  show ?thesis
+    unfolding *
+    apply safe
+    unfolding snd_conv
+  proof -
+    fix x k
+    assume "(x, k) \<in> p"
+    note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this]
+    then show "f integrable_on k"
+      apply safe
+      apply (rule d[THEN conjunct2,rule_format,of x])
+      apply auto
+      done
+  qed
+qed
+
 
 subsection {* Second FCT or existence of antiderivative. *}
 
-lemma integrable_const[intro]:"(\<lambda>x. c) integrable_on {a..b}"
-  unfolding integrable_on_def by(rule,rule has_integral_const)
-
-lemma integral_has_vector_derivative: fixes f::"real \<Rightarrow> 'a::banach"
-  assumes "continuous_on {a..b} f" "x \<in> {a..b}"
+lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on {a..b}"
+  unfolding integrable_on_def
+  apply rule
+  apply (rule has_integral_const)
+  done
+
+lemma integral_has_vector_derivative:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "continuous_on {a..b} f"
+    and "x \<in> {a..b}"
   shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
   unfolding has_vector_derivative_def has_derivative_within_alt
-apply safe apply(rule bounded_linear_scaleR_left)
-proof- fix e::real assume e:"e>0"
+  apply safe
+  apply (rule bounded_linear_scaleR_left)
+proof -
+  fix e :: real
+  assume e: "e > 0"
   note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def]
-  from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format]
+  from this[rule_format,OF e] guess d by (elim conjE exE) note d=this[rule_format]
   let ?I = "\<lambda>a b. integral {a..b} f"
-  show "\<exists>d>0. \<forall>y\<in>{a..b}. norm (y - x) < d \<longrightarrow> norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
-  proof(rule,rule,rule d,safe) case goal1 show ?case proof(cases "y < x")
-      case False have "f integrable_on {a..y}" apply(rule integrable_subinterval,rule integrable_continuous)
-        apply(rule assms)  unfolding not_less using assms(2) goal1 by auto
-      hence *:"?I a y - ?I a x = ?I x y" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
-        using False unfolding not_less using assms(2) goal1 by auto
-      have **:"norm (y - x) = content {x..y}" apply(subst content_real) using False unfolding not_less by auto
-      show ?thesis unfolding ** apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) unfolding * unfolding o_def
-        defer apply(rule has_integral_sub) apply(rule integrable_integral)
-        apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+
-      proof- show "{x..y} \<subseteq> {a..b}" using goal1 assms(2) by auto
-        have *:"y - x = norm(y - x)" using False by auto
-        show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}" apply(subst *) unfolding ** by auto
-        show "\<forall>xa\<in>{x..y}. norm (f xa - f x) \<le> e" apply safe apply(rule less_imp_le)
-          apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
-      qed(insert e,auto)
-    next case True have "f integrable_on {a..x}" apply(rule integrable_subinterval,rule integrable_continuous)
-        apply(rule assms)+  unfolding not_less using assms(2) goal1 by auto
-      hence *:"?I a x - ?I a y = ?I y x" unfolding algebra_simps apply(subst eq_commute) apply(rule integral_combine)
-        using True using assms(2) goal1 by auto
-      have **:"norm (y - x) = content {y..x}" apply(subst content_real) using True unfolding not_less by auto
-      have ***:"\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)" unfolding scaleR_left.diff by auto
-      show ?thesis apply(subst ***) unfolding norm_minus_cancel **
-        apply(rule has_integral_bound[where f="(\<lambda>u. f u - f x)"]) unfolding * unfolding o_def
-        defer apply(rule has_integral_sub) apply(subst minus_minus[symmetric]) unfolding minus_minus
-        apply(rule integrable_integral) apply(rule integrable_subinterval,rule integrable_continuous) apply(rule assms)+
-      proof- show "{y..x} \<subseteq> {a..b}" using goal1 assms(2) by auto
-        have *:"x - y = norm(y - x)" using True by auto
-        show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" apply(subst *) unfolding ** by auto
-        show "\<forall>xa\<in>{y..x}. norm (f xa - f x) \<le> e" apply safe apply(rule less_imp_le)
-          apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto
-      qed(insert e,auto) qed qed qed
-
-lemma antiderivative_continuous: assumes "continuous_on {a..b::real} f"
-  obtains g where "\<forall>x\<in> {a..b}. (g has_vector_derivative (f(x)::_::banach)) (at x within {a..b})"
-  apply(rule that,rule) using integral_has_vector_derivative[OF assms] by auto
+  show "\<exists>d>0. \<forall>y\<in>{a..b}. norm (y - x) < d \<longrightarrow>
+    norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
+  proof (rule, rule, rule d, safe)
+    case goal1
+    show ?case
+    proof (cases "y < x")
+      case False
+      have "f integrable_on {a..y}"
+        apply (rule integrable_subinterval,rule integrable_continuous)
+        apply (rule assms)
+        unfolding not_less
+        using assms(2) goal1
+        apply auto
+        done
+      then have *: "?I a y - ?I a x = ?I x y"
+        unfolding algebra_simps
+        apply (subst eq_commute)
+        apply (rule integral_combine)
+        using False
+        unfolding not_less
+        using assms(2) goal1
+        apply auto
+        done
+      have **: "norm (y - x) = content {x..y}"
+        apply (subst content_real)
+        using False
+        unfolding not_less
+        apply auto
+        done
+      show ?thesis
+        unfolding **
+        apply (rule has_integral_bound[where f="(\<lambda>u. f u - f x)"])
+        unfolding *
+        unfolding o_def
+        defer
+        apply (rule has_integral_sub)
+        apply (rule integrable_integral)
+        apply (rule integrable_subinterval)
+        apply (rule integrable_continuous)
+        apply (rule assms)+
+      proof -
+        show "{x..y} \<subseteq> {a..b}"
+          using goal1 assms(2) by auto
+        have *: "y - x = norm (y - x)"
+          using False by auto
+        show "((\<lambda>xa. f x) has_integral (y - x) *\<^sub>R f x) {x.. y}"
+          apply (subst *)
+          unfolding **
+          apply auto
+          done
+        show "\<forall>xa\<in>{x..y}. norm (f xa - f x) \<le> e"
+          apply safe
+          apply (rule less_imp_le)
+          apply (rule d(2)[unfolded dist_norm])
+          using assms(2)
+          using goal1
+          apply auto
+          done
+      qed (insert e, auto)
+    next
+      case True
+      have "f integrable_on {a..x}"
+        apply (rule integrable_subinterval,rule integrable_continuous)
+        apply (rule assms)+
+        unfolding not_less
+        using assms(2) goal1
+        apply auto
+        done
+      then have *: "?I a x - ?I a y = ?I y x"
+        unfolding algebra_simps
+        apply (subst eq_commute)
+        apply (rule integral_combine)
+        using True using assms(2) goal1
+        apply auto
+        done
+      have **: "norm (y - x) = content {y..x}"
+        apply (subst content_real)
+        using True
+        unfolding not_less
+        apply auto
+        done
+      have ***: "\<And>fy fx c::'a. fx - fy - (y - x) *\<^sub>R c = -(fy - fx - (x - y) *\<^sub>R c)"
+        unfolding scaleR_left.diff by auto
+      show ?thesis
+        apply (subst ***)
+        unfolding norm_minus_cancel **
+        apply (rule has_integral_bound[where f="(\<lambda>u. f u - f x)"])
+        unfolding *
+        unfolding o_def
+        defer
+        apply (rule has_integral_sub)
+        apply (subst minus_minus[symmetric])
+        unfolding minus_minus
+        apply (rule integrable_integral)
+        apply (rule integrable_subinterval,rule integrable_continuous)
+        apply (rule assms)+
+      proof -
+        show "{y..x} \<subseteq> {a..b}"
+          using goal1 assms(2) by auto
+        have *: "x - y = norm (y - x)"
+          using True by auto
+        show "((\<lambda>xa. f x) has_integral (x - y) *\<^sub>R f x) {y..x}"
+          apply (subst *)
+          unfolding **
+          apply auto
+          done
+        show "\<forall>xa\<in>{y..x}. norm (f xa - f x) \<le> e"
+          apply safe
+          apply (rule less_imp_le)
+          apply (rule d(2)[unfolded dist_norm])
+          using assms(2)
+          using goal1
+          apply auto
+          done
+      qed (insert e, auto)
+    qed
+  qed
+qed
+
+lemma antiderivative_continuous:
+  fixes q b :: real
+  assumes "continuous_on {a..b} f"
+  obtains g where "\<forall>x\<in> {a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
+  apply (rule that)
+  apply rule
+  using integral_has_vector_derivative[OF assms]
+  apply auto
+  done
+
 
 subsection {* Combined fundamental theorem of calculus. *}
 
-lemma antiderivative_integral_continuous: fixes f::"real \<Rightarrow> 'a::banach" assumes "continuous_on {a..b} f"
+lemma antiderivative_integral_continuous:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "continuous_on {a..b} f"
   obtains g where "\<forall>u\<in>{a..b}. \<forall>v \<in> {a..b}. u \<le> v \<longrightarrow> (f has_integral (g v - g u)) {u..v}"
-proof- from antiderivative_continuous[OF assms] guess g . note g=this
-  show ?thesis apply(rule that[of g])
-  proof safe case goal1 have "\<forall>x\<in>{u..v}. (g has_vector_derivative f x) (at x within {u..v})"
-      apply(rule,rule has_vector_derivative_within_subset) apply(rule g[rule_format]) using goal1(1-2) by auto
-    thus ?case using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto qed qed
+proof -
+  from antiderivative_continuous[OF assms] guess g . note g=this
+  show ?thesis
+    apply (rule that[of g])
+  proof safe
+    case goal1
+    have "\<forall>x\<in>{u..v}. (g has_vector_derivative f x) (at x within {u..v})"
+      apply rule
+      apply (rule has_vector_derivative_within_subset)
+      apply (rule g[rule_format])
+      using goal1(1-2)
+      apply auto
+      done
+    then show ?case
+      using fundamental_theorem_of_calculus[OF goal1(3),of "g" "f"] by auto
+  qed
+qed
+
 
 subsection {* General "twiddling" for interval-to-interval function image. *}
 
 lemma has_integral_twiddle:
-  assumes "0 < r" "\<forall>x. h(g x) = x" "\<forall>x. g(h x) = x" "\<forall>x. continuous (at x) g"
-  "\<forall>u v. \<exists>w z. g ` {u..v} = {w..z}"
-  "\<forall>u v. \<exists>w z. h ` {u..v} = {w..z}"
-  "\<forall>u v. content(g ` {u..v}) = r * content {u..v}"
-  "(f has_integral i) {a..b}"
+  assumes "0 < r"
+    and "\<forall>x. h(g x) = x"
+    and "\<forall>x. g(h x) = x"
+    and "\<forall>x. continuous (at x) g"
+    and "\<forall>u v. \<exists>w z. g ` {u..v} = {w..z}"
+    and "\<forall>u v. \<exists>w z. h ` {u..v} = {w..z}"
+    and "\<forall>u v. content(g ` {u..v}) = r * content {u..v}"
+    and "(f has_integral i) {a..b}"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` {a..b})"
-proof- { presume *:"{a..b} \<noteq> {} \<Longrightarrow> ?thesis"
-    show ?thesis apply cases defer apply(rule *,assumption)
-    proof- case goal1 thus ?thesis unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed }
-  assume "{a..b} \<noteq> {}" from assms(6)[rule_format,of a b] guess w z apply-by(erule exE)+ note wz=this
-  have inj:"inj g" "inj h" unfolding inj_on_def apply safe apply(rule_tac[!] ccontr)
-    using assms(2) apply(erule_tac x=x in allE) using assms(2) apply(erule_tac x=y in allE) defer
-    using assms(3) apply(erule_tac x=x in allE) using assms(3) apply(erule_tac x=y in allE) by auto
-  show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz)
-  proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos)
-    from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format]
-    def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def ..
+proof -
+  {
+    presume *: "{a..b} \<noteq> {} \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      defer
+      apply (rule *)
+      apply assumption
+    proof -
+      case goal1
+      then show ?thesis
+        unfolding goal1 assms(8)[unfolded goal1 has_integral_empty_eq] by auto qed
+  }
+  assume "{a..b} \<noteq> {}"
+  from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this
+  have inj: "inj g" "inj h"
+    unfolding inj_on_def
+    apply safe
+    apply(rule_tac[!] ccontr)
+    using assms(2)
+    apply(erule_tac x=x in allE)
+    using assms(2)
+    apply(erule_tac x=y in allE)
+    defer
+    using assms(3)
+    apply (erule_tac x=x in allE)
+    using assms(3)
+    apply(erule_tac x=y in allE)
+    apply auto
+    done
+  show ?thesis
+    unfolding has_integral_def has_integral_compact_interval_def
+    apply (subst if_P)
+    apply rule
+    apply rule
+    apply (rule wz)
+  proof safe
+    fix e :: real
+    assume e: "e > 0"
+    then have "e * r > 0"
+      using assms(1) by (rule mult_pos_pos)
+    from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format]
+    def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}"
+    have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
+      unfolding d'_def ..
     show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
-    proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto
-      fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)]
-      have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p" unfolding tagged_division_of
-      proof safe show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)" using as by auto
-        show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p" using as(2) unfolding fine_def d' by auto
-        fix x k assume xk[intro]:"(x,k) \<in> p" show "g x \<in> g ` k" using p(2)[OF xk] by auto
-        show "\<exists>u v. g ` k = {u..v}" using p(4)[OF xk] using assms(5-6) by auto
-        { fix y assume "y \<in> k" thus "g y \<in> {a..b}" "g y \<in> {a..b}" using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
-            using assms(2)[rule_format,of y] unfolding inj_image_mem_iff[OF inj(2)] by auto }
-        fix x' k' assume xk':"(x',k') \<in> p" fix z assume "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
-        hence *:"interior (g ` k) \<inter> interior (g ` k') \<noteq> {}" by auto
-        have same:"(x, k) = (x', k')" apply-apply(rule ccontr,drule p(5)[OF xk xk'])
-        proof- assume as:"interior k \<inter> interior k' = {}" from nonempty_witness[OF *] guess z .
-          hence "z \<in> g ` (interior k \<inter> interior k')" using interior_image_subset[OF assms(4) inj(1)]
-            unfolding image_Int[OF inj(1)] by auto thus False using as by blast
-        qed thus "g x = g x'" by auto
-        { fix z assume "z \<in> k"  thus  "g z \<in> g ` k'" using same by auto }
-        { fix z assume "z \<in> k'" thus  "g z \<in> g ` k"  using same by auto }
-      next fix x assume "x \<in> {a..b}" hence "h x \<in>  \<Union>{k. \<exists>x. (x, k) \<in> p}" using p(6) by auto
-        then guess X unfolding Union_iff .. note X=this from this(1) guess y unfolding mem_Collect_eq ..
-        thus "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}" apply-
-          apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI)
-          using X(2) assms(3)[rule_format,of x] by auto
-      qed note ** = d(2)[OF this] 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 = _") unfolding algebra_simps add_left_cancel
-        unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
-        apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
-      also have "... = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR
-        using assms(1) by auto finally have *:"?l = ?r" .
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR
-        using assms(1) by(auto simp add:field_simps) qed qed qed
+    proof (rule_tac x=d' in exI, safe)
+      show "gauge d'"
+        using d(1)
+        unfolding gauge_def d'
+        using continuous_open_preimage_univ[OF assms(4)]
+        by auto
+      fix p
+      assume as: "p tagged_division_of h ` {a..b}" "d' fine p"
+      note p = tagged_division_ofD[OF as(1)]
+      have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of {a..b} \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
+        unfolding tagged_division_of
+      proof safe
+        show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
+          using as by auto
+        show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
+          using as(2) unfolding fine_def d' by auto
+        fix x k
+        assume xk[intro]: "(x, k) \<in> p"
+        show "g x \<in> g ` k"
+          using p(2)[OF xk] by auto
+        show "\<exists>u v. g ` k = {u..v}"
+          using p(4)[OF xk] using assms(5-6) by auto
+        {
+          fix y
+          assume "y \<in> k"
+          then show "g y \<in> {a..b}" "g y \<in> {a..b}"
+            using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
+            using assms(2)[rule_format,of y]
+            unfolding inj_image_mem_iff[OF inj(2)]
+            by auto
+        }
+        fix x' k'
+        assume xk': "(x', k') \<in> p"
+        fix z
+        assume "z \<in> interior (g ` k)" and "z \<in> interior (g ` k')"
+        then have *: "interior (g ` k) \<inter> interior (g ` k') \<noteq> {}"
+          by auto
+        have same: "(x, k) = (x', k')"
+          apply -
+          apply (rule ccontr,drule p(5)[OF xk xk'])
+        proof -
+          assume as: "interior k \<inter> interior k' = {}"
+          from nonempty_witness[OF *] guess z .
+          then have "z \<in> g ` (interior k \<inter> interior k')"
+            using interior_image_subset[OF assms(4) inj(1)]
+            unfolding image_Int[OF inj(1)]
+            by auto
+          then show False
+            using as by blast
+        qed
+        then show "g x = g x'"
+          by auto
+        {
+          fix z
+          assume "z \<in> k"
+          then show "g z \<in> g ` k'"
+            using same by auto
+        }
+        {
+          fix z
+          assume "z \<in> k'"
+          then show "g z \<in> g ` k"
+            using same by auto
+        }
+      next
+        fix x
+        assume "x \<in> {a..b}"
+        then have "h x \<in>  \<Union>{k. \<exists>x. (x, k) \<in> p}"
+          using p(6) by auto
+        then guess X unfolding Union_iff .. note X=this
+        from this(1) guess y unfolding mem_Collect_eq ..
+        then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
+          apply -
+          apply (rule_tac X="g ` X" in UnionI)
+          defer
+          apply (rule_tac x="h x" in image_eqI)
+          using X(2) assms(3)[rule_format,of x]
+          apply auto
+          done
+      qed
+        note ** = d(2)[OF this]
+        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 = _")
+          unfolding algebra_simps add_left_cancel
+          unfolding setsum_reindex[OF *]
+          apply (subst scaleR_right.setsum)
+          defer
+          apply (rule setsum_cong2)
+          unfolding o_def split_paired_all split_conv
+          apply (drule p(4))
+          apply safe
+          unfolding assms(7)[rule_format]
+          using p
+          apply auto
+          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")
+        unfolding scaleR_diff_right scaleR_scaleR
+        using assms(1)
+        by auto
+      finally have *: "?l = ?r" .
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
+        using **
+        unfolding *
+        unfolding norm_scaleR
+        using assms(1)
+        by (auto simp add:field_simps)
+    qed
+  qed
+qed
+
 
 subsection {* Special case of a basic affine transformation. *}
 
-lemma interval_image_affinity_interval: shows "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}"
-  unfolding image_affinity_interval by auto
-
-lemma setprod_cong2: assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x" shows "setprod f A = setprod g A"
-  apply(rule setprod_cong) using assms by auto
+lemma interval_image_affinity_interval:
+  "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::ordered_euclidean_space) + c) ` {a..b} = {u..v}"
+  unfolding image_affinity_interval
+  by auto
+
+lemma setprod_cong2:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
+  shows "setprod f A = setprod g A"
+  apply (rule setprod_cong)
+  using assms
+  apply auto
+  done
 
 lemma content_image_affinity_interval:
- "content((\<lambda>x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) = (abs m) ^ DIM('a) * content {a..b}" (is "?l = ?r")
-proof- { presume *:"{a..b}\<noteq>{} \<Longrightarrow> ?thesis" show ?thesis apply(cases,rule *,assumption)
-      unfolding not_not using content_empty by auto }
-  assume as: "{a..b}\<noteq>{}"
+  "content((\<lambda>x::'a::ordered_euclidean_space. m *\<^sub>R x + c) ` {a..b}) =
+    abs m ^ DIM('a) * content {a..b}" (is "?l = ?r")
+proof -
+  {
+    presume *: "{a..b} \<noteq> {} \<Longrightarrow> ?thesis"
+    show ?thesis
+      apply cases
+      apply (rule *)
+      apply assumption
+      unfolding not_not
+      using content_empty
+      apply auto
+      done
+  }
+  assume as: "{a..b} \<noteq> {}"
   show ?thesis
   proof (cases "m \<ge> 0")
     case True
@@ -6791,7 +7463,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis
       by (simp add: image_affinity_interval True content_closed_interval'
-                    setprod_timesf setprod_constant inner_diff_left)
+        setprod_timesf setprod_constant inner_diff_left)
   next
     case False
     with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
@@ -6804,20 +7476,43 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
       by (simp add: image_affinity_interval content_closed_interval'
-                    setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left)
+        setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left)
   qed
 qed
 
-lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \<noteq> 0"
+lemma has_integral_affinity:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "(f has_integral i) {a..b}"
+    and "m \<noteq> 0"
   shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\<lambda>x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})"
-  apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq_iff[where 'a='a]
+  apply (rule has_integral_twiddle)
+  apply safe
+  apply (rule zero_less_power)
+  unfolding euclidean_eq_iff[where 'a='a]
   unfolding scaleR_right_distrib inner_simps scaleR_scaleR
-  defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps)
-  apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto
-
-lemma integrable_affinity: assumes "f integrable_on {a..b}" "m \<noteq> 0"
+  defer
+  apply (insert assms(2))
+  apply (simp add: field_simps)
+  apply (insert assms(2))
+  apply (simp add: field_simps)
+  apply (rule continuous_intros)+
+  apply (rule interval_image_affinity_interval)+
+  apply (rule content_image_affinity_interval)
+  using assms
+  apply auto
+  done
+
+lemma integrable_affinity:
+  assumes "f integrable_on {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)) ` {a..b})"
-  using assms unfolding integrable_on_def apply safe apply(drule has_integral_affinity) by auto
+  using assms
+  unfolding integrable_on_def
+  apply safe
+  apply (drule has_integral_affinity)
+  apply auto
+  done
+
 
 subsection {* Special case of stretching coordinate axes separately. *}