# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525602820 -3600
# Node ID 4fa3e63ecc7e22776b5f4450f7d23e3e9fe3cb3b
# Parent  b25ccd85b1fd2f696ab487cbb18085172b711d92
starting to tidy up Interval_Integral.thy

diff -r b25ccd85b1fd -r 4fa3e63ecc7e src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri May 04 22:26:25 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Sun May 06 11:33:40 2018 +0100
@@ -72,8 +72,8 @@
   by blast
 
 lemma has_derivative_within_open:
-  "a \<in> s \<Longrightarrow> open s \<Longrightarrow>
-    (f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a)"
+  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
+    (f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)"
   by (simp only: at_within_interior interior_open)
 
 lemma has_derivative_right:
@@ -98,8 +98,8 @@
 lemmas DERIV_within_iff = has_field_derivative_iff
 
 lemma DERIV_caratheodory_within:
-  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
-   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
+  "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
+   (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
       (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -107,14 +107,14 @@
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
-    show "continuous (at x within s) ?g" using \<open>?lhs\<close>
+    show "continuous (at x within S) ?g" using \<open>?lhs\<close>
       by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
     show "?g x = l" by simp
   qed
 next
   assume ?rhs
   then obtain g where
-    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within s) g" and "g x = l" by blast
+    "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
   thus ?lhs
     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
 qed
@@ -330,18 +330,23 @@
   using has_derivative_compose[of f f' x UNIV g g']
   by (simp add: comp_def)
 
+lemma has_vector_derivative_within_open:
+  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
+    (f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
+  by (simp only: at_within_interior interior_open)
+
 lemma field_vector_diff_chain_within:
- assumes Df: "(f has_vector_derivative f') (at x within s)"
-     and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
- shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
+ assumes Df: "(f has_vector_derivative f') (at x within S)"
+     and Dg: "(g has_field_derivative g') (at (f x) within f ` S)"
+ shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within S)"
 using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
                        Dg [unfolded has_field_derivative_def]]
  by (auto simp: o_def mult.commute has_vector_derivative_def)
 
 lemma vector_derivative_diff_chain_within:
-  assumes Df: "(f has_vector_derivative f') (at x within s)"
-     and Dg: "(g has_derivative g') (at (f x) within f`s)"
-  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
+  assumes Df: "(f has_vector_derivative f') (at x within S)"
+     and Dg: "(g has_derivative g') (at (f x) within f`S)"
+  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within S)"
 using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
   linear.scaleR[OF has_derivative_linear[OF Dg]]
   unfolding has_vector_derivative_def o_def
@@ -357,8 +362,8 @@
   by (meson diff_chain_at)
 
 lemma differentiable_chain_within:
-  "f differentiable (at x within s) \<Longrightarrow>
-    g differentiable (at(f x) within (f ` s)) \<Longrightarrow> (g \<circ> f) differentiable (at x within s)"
+  "f differentiable (at x within S) \<Longrightarrow>
+    g differentiable (at(f x) within (f ` S)) \<Longrightarrow> (g \<circ> f) differentiable (at x within S)"
   unfolding differentiable_def
   by (meson diff_chain_within)
 
diff -r b25ccd85b1fd -r 4fa3e63ecc7e src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri May 04 22:26:25 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun May 06 11:33:40 2018 +0100
@@ -12,20 +12,6 @@
   "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
   by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
 
-lemma has_vector_derivative_weaken:
-  fixes x D and f g s t
-  assumes f: "(f has_vector_derivative D) (at x within t)"
-    and "x \<in> s" "s \<subseteq> t"
-    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
-  shows "(g has_vector_derivative D) (at x within s)"
-proof -
-  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
-    unfolding has_vector_derivative_def has_derivative_iff_norm
-    using assms by (intro conj_cong Lim_cong_within refl) auto
-  then show ?thesis
-    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
-qed
-
 definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
 
 lemma einterval_eq[simp]:
@@ -59,8 +45,7 @@
 lemma ereal_incseq_approx:
   fixes a b :: ereal
   assumes "a < b"
-  obtains X :: "nat \<Rightarrow> real" where
-    "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
+  obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
 proof (cases b)
   case PInf
   with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
@@ -87,13 +72,12 @@
     by (intro mult_strict_left_mono) auto
   with \<open>a < b\<close> a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
     by (cases a) (auto simp: real d_def field_simps)
-  moreover have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
-    apply (subst filterlim_sequentially_Suc)
-    apply (subst filterlim_sequentially_Suc)
-    apply (rule tendsto_eq_intros)
-    apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1
-                simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
-    done
+  moreover
+  have "(\<lambda>i. b' - d / real i) \<longlonglongrightarrow> b'"
+    by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1
+              simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
+  then have "(\<lambda>i. b' - d / Suc (Suc i)) \<longlonglongrightarrow> b'"
+    by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2])
   ultimately show thesis
     by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
        (auto simp add: real incseq_def intro!: divide_left_mono)
@@ -601,14 +585,6 @@
   TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
 *)
 
-(*
-TODO: many proofs below require inferences like
-
-  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
-
-where x and y are real. These should be better automated.
-*)
-
 lemma interval_integral_FTC_finite:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   assumes f: "continuous_on {min a b..max a b} f"
@@ -646,7 +622,6 @@
 qed
 
 
-
 lemma interval_integral_FTC_nonneg:
   fixes f F :: "real \<Rightarrow> real" and a b :: ereal
   assumes "a < b"
@@ -659,7 +634,11 @@
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = B - A"
 proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
+  obtain u l where approx:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
   have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
@@ -705,7 +684,11 @@
   assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   shows "(LBINT x=a..b. f x) = B - A"
 proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx = this
+  obtain u l where approx:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
   have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
@@ -783,18 +766,20 @@
     have 2: "max c x < b" by simp
     from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b"
       by (auto simp add: einterval_def)
-    show "(?F has_vector_derivative f x) (at x)"
-      (* TODO: factor out the next three lines to has_field_derivative_within_open *)
-      unfolding has_vector_derivative_def
-      apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto)
-      apply (subst has_vector_derivative_def [symmetric])
-      apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
-      apply (rule interval_integral_FTC2, auto simp add: less_imp_le)
-      apply (rule continuous_at_imp_continuous_on)
-      apply (auto intro!: contf)
-      apply (rule order_less_le_trans, rule \<open>a < d\<close>, auto)
-      apply (rule order_le_less_trans) prefer 2
-      by (rule \<open>e < b\<close>, auto)
+    have "(?F has_vector_derivative f x) (at x within {d<..<e})"
+    proof (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
+      have "continuous_on {d..e} f"
+      proof (intro continuous_at_imp_continuous_on ballI contf; clarsimp)
+        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> a < ereal x"
+          using \<open>a < ereal d\<close> ereal_less_ereal_Ex by auto
+        show "\<And>x. \<lbrakk>d \<le> x; x \<le> e\<rbrakk> \<Longrightarrow> ereal x < b"
+          using \<open>ereal e < b\<close> ereal_less_eq(3) le_less_trans by blast
+      qed
+      then show "(?F has_vector_derivative f x) (at x within {d..e})"
+        by (intro interval_integral_FTC2) (use \<open>d < c\<close> \<open>c < e\<close> \<open>d < x\<close> \<open>x < e\<close> in \<open>linarith+\<close>)
+    qed auto
+    then show "(?F has_vector_derivative f x) (at x)"
+      by (force simp add: has_vector_derivative_within_open [of _ "{d<..<e}"])
   qed
 qed
 
@@ -871,27 +856,29 @@
   and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
   shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
 proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
+  obtain u l where approx [simp]:
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
+    by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])
   note less_imp_le [simp]
   have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
   have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
     by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
-  have [simp]: "\<And>i. l i < b"
-    apply (rule order_less_trans) prefer 2
-    by (rule approx, auto, rule approx)
+  then have lessb[simp]: "\<And>i. l i < b"
+    using approx(4) less_eq_real_def by blast
   have [simp]: "\<And>i. a < u i"
     by (rule order_less_trans, rule approx, auto, rule approx)
-  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
+  have lle[simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
-  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
-    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
-    apply (rule exI, rule conjI, rule deriv_g)
-    apply (erule order_less_le_trans, auto)
-    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
-    apply (rule g'_nonneg)
-    apply (rule less_imp_le, erule order_less_le_trans, auto)
-    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+      by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that)
+  qed
   have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   proof -
     have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
@@ -904,36 +891,36 @@
       by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
     hence B3: "\<And>i. g (u i) \<le> B"
       by (intro incseq_le, auto simp add: incseq_def)
-    show "A \<le> B"
-      apply (rule order_trans [OF A3 [of 0]])
-      apply (rule order_trans [OF _ B3 [of 0]])
+    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
       by auto
+    then show "A \<le> B"
+      by (meson A3 B3 order.trans)
     { fix x :: real
       assume "A < x" and "x < B"
       then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
-        apply (intro eventually_conj order_tendstoD)
-        by (rule A2, assumption, rule B2, assumption)
+        by (fast intro: eventually_conj order_tendstoD A2 B2)
       hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
         by (simp add: eventually_sequentially, auto)
     } note AB = this
     show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
-      apply (auto simp add: einterval_def)
-      apply (erule (1) AB)
-      apply (rule order_le_less_trans, rule A3, simp)
-      apply (rule order_less_le_trans) prefer 2
-      by (rule B3, simp)
+    proof
+      show "einterval A B \<subseteq> (\<Union>i. {g(l i)<..<g(u i)})"
+        by (auto simp add: einterval_def AB)
+      show "(\<Union>i. {g(l i)<..<g(u i)}) \<subseteq> einterval A B"
+      proof (clarsimp simp add: einterval_def, intro conjI)
+        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> A < ereal x"
+          using A3 le_ereal_less by blast
+        show "\<And>x i. \<lbrakk>g (l i) < x; x < g (u i)\<rbrakk> \<Longrightarrow> ereal x < B"
+          using B3 ereal_le_less by blast
+      qed
+    qed
   qed
   (* finally, the main argument *)
-  {
-     fix i
-     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
-        apply (rule interval_integral_substitution_finite, auto)
-        apply (rule DERIV_subset)
-        unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
-        apply (rule deriv_g)
-        apply (auto intro!: continuous_at_imp_continuous_on contf contg')
-        done
-  } note eq1 = this
+  have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
+    apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
+    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+         apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+    done
   have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
     apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
     by (rule assms)
@@ -941,9 +928,8 @@
     by (simp add: eq1)
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
     apply (auto simp add: incseq_def)
-    apply (rule order_le_less_trans)
-    prefer 2 apply (assumption, auto)
-    by (erule order_less_le_trans, rule g_nondec, auto)
+    using lessb lle approx(5) g_nondec le_less_trans apply blast
+    by (force intro: less_le_trans)
   have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x = A..B. f x)"
     apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
     apply (subst interval_lebesgue_integral_le_eq, rule \<open>A \<le> B\<close>)
@@ -977,23 +963,21 @@
   note less_imp_le [simp]
   have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
-  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+  have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
     by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
-  have [simp]: "\<And>i. l i < b"
-    apply (rule order_less_trans) prefer 2
-    by (rule approx, auto, rule approx)
-  have [simp]: "\<And>i. a < u i"
+  have llb[simp]: "\<And>i. l i < b"
+    using lessb approx(4) less_eq_real_def by blast
+  have alu[simp]: "\<And>i. a < u i"
     by (rule order_less_trans, rule approx, auto, rule approx)
   have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
-  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
-  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
-    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
-    apply (rule exI, rule conjI, rule deriv_g)
-    apply (erule order_less_le_trans, auto)
-    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
-    apply (rule g'_nonneg)
-    apply (rule less_imp_le, erule order_less_le_trans, auto)
-    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have uleu[simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
+  have g_nondec [simp]: "g x \<le> g y" if "a < x" "x \<le> y" "y < b" for x y
+  proof (rule DERIV_nonneg_imp_nondecreasing [OF \<open>x \<le> y\<close>], intro exI conjI allI impI)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> (g has_real_derivative g' u) (at u)"
+      by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that)
+    show "\<And>u. x \<le> u \<and> u \<le> y \<Longrightarrow> 0 \<le> g' u"
+      by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that)
+  qed
   have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   proof -
     have A2: "(\<lambda>i. g (l i)) \<longlonglongrightarrow> A"
@@ -1006,10 +990,10 @@
       by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
     hence B3: "\<And>i. g (u i) \<le> B"
       by (intro incseq_le, auto simp add: incseq_def)
-    show "A \<le> B"
-      apply (rule order_trans [OF A3 [of 0]])
-      apply (rule order_trans [OF _ B3 [of 0]])
+    have "ereal (g (l 0)) \<le> ereal (g (u 0))"
       by auto
+    then show "A \<le> B"
+      by (meson A3 B3 order.trans)
     { fix x :: real
       assume "A < x" and "x < B"
       then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
@@ -1019,23 +1003,26 @@
         by (simp add: eventually_sequentially, auto)
     } note AB = this
     show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
-      apply (auto simp add: einterval_def)
-      apply (erule (1) AB)
-      apply (rule order_le_less_trans, rule A3, simp)
-      apply (rule order_less_le_trans) prefer 2
-      by (rule B3, simp)
+    proof
+      show "einterval A B \<subseteq> (\<Union>i. {g (l i)<..<g (u i)})"
+        by (auto simp add: einterval_def AB)
+      show "(\<Union>i. {g (l i)<..<g (u i)}) \<subseteq> einterval A B"
+        apply (clarsimp simp: einterval_def, intro conjI)
+        using A3 le_ereal_less apply blast
+        using B3 ereal_le_less by blast
+    qed
   qed
-  (* finally, the main argument *)
-  {
-     fix i
-     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
-        apply (rule interval_integral_substitution_finite, auto)
-        apply (rule DERIV_subset, rule deriv_g, auto)
-        apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto)
-        by (rule continuous_at_imp_continuous_on, auto, rule contg', auto)
-     then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)"
-       by (simp add: ac_simps)
-  } note eq1 = this
+    (* finally, the main argument *)
+  have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i
+  proof -
+    have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
+      apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
+      unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+           apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+      done
+    then show ?thesis
+      by (simp add: ac_simps)
+  qed
   have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
       \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
     apply (rule interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
@@ -1043,15 +1030,16 @@
   hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> (LBINT x=a..b. f (g x) * g' x)"
     by (simp add: eq1)
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
-    apply (auto simp add: incseq_def)
-    apply (rule order_le_less_trans)
-    prefer 2 apply assumption
-    apply (rule g_nondec, auto)
-    by (erule order_less_le_trans, rule g_nondec, auto)
-  have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c"
-    apply (frule (1) IVT' [of g], auto)
-    apply (rule continuous_at_imp_continuous_on, auto)
-    by (rule DERIV_isCont, rule deriv_g, auto)
+    apply (clarsimp simp add: incseq_def, intro conjI)
+    apply (meson llb antimono_def approx(3) approx(5) g_nondec le_less_trans)
+    using alu uleu approx(6) g_nondec less_le_trans by blast
+  have img: "\<exists>c \<ge> l i. c \<le> u i \<and> x = g c" if "g (l i) \<le> x" "x \<le> g (u i)" for x i
+  proof -
+    have "continuous_on {l i..u i} g"
+      by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on)
+    with that show ?thesis
+      using IVT' [of g] approx(4) dual_order.strict_implies_order by blast
+  qed
   have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
     by (frule (1) img, auto, rule f_nonneg, auto)
   have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x"
diff -r b25ccd85b1fd -r 4fa3e63ecc7e src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri May 04 22:26:25 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun May 06 11:33:40 2018 +0100
@@ -627,6 +627,28 @@
   "real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
   by (cases y) auto
 
+(*To help with inferences like  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
+  where x and y are real.
+*)
+
+lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
+  using ereal_less_eq(3) order.trans by blast
+
+lemma le_ereal_less: "a \<le> ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y"
+  by (simp add: le_less_trans)
+
+lemma less_ereal_le: "a < ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a < ereal y"
+  using ereal_less_ereal_Ex by auto
+
+lemma ereal_le_le: "ereal y \<le> a \<Longrightarrow> x \<le> y \<Longrightarrow> ereal x \<le> a"
+  by (simp add: order_subst2)
+
+lemma ereal_le_less: "ereal y \<le> a \<Longrightarrow> x < y \<Longrightarrow> ereal x < a"
+  by (simp add: dual_order.strict_trans1)
+
+lemma ereal_less_le: "ereal y < a \<Longrightarrow> x \<le> y \<Longrightarrow> ereal x < a"
+  using ereal_less_eq(3) le_less_trans by blast
+
 lemma real_of_ereal_pos:
   fixes x :: ereal
   shows "0 \<le> x \<Longrightarrow> 0 \<le> real_of_ereal x" by (cases x) auto