src/HOL/Analysis/Interval_Integral.thy

   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: real incseq_def intro!: divide_left_mono)
-qed (insert \<open>a < b\<close>, auto)
+qed (use \<open>a < b\<close> in auto)
 
 lemma ereal_decseq_approx:
   fixes a b :: ereal
   assumes "a < b"
   obtains X :: "nat \<Rightarrow> real" where
     "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
 proof -
   have "-b < -a" using \<open>a < b\<close> by simp
-  from ereal_incseq_approx[OF this] guess X .
+  from ereal_incseq_approx[OF this] obtain X where
+    "incseq X"
+    "\<And>i. - b < ereal (X i)"
+    "\<And>i. ereal (X i) < - a"
+    "(\<lambda>x. ereal (X x)) \<longlonglongrightarrow> - a"
+    by auto
   then show thesis
     apply (intro that[of "\<lambda>i. - X i"])
     apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
     apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
     done

     "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"
 proof -
   from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
-  from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
-  from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
+  from ereal_incseq_approx[OF \<open>c < b\<close>] obtain u where u:
+    "incseq u"
+    "\<And>i. c < ereal (u i)"
+    "\<And>i. ereal (u i) < b"
+    "(\<lambda>x. ereal (u x)) \<longlonglongrightarrow> b"
+    by auto
+  from ereal_decseq_approx[OF \<open>a < c\<close>] obtain l where l:
+    "decseq l"
+    "\<And>i. a < ereal (l i)"
+    "\<And>i. ereal (l i) < c"
+    "(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
+    by auto
   { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
   have "einterval a b = (\<Union>i. {l i .. u i})"
   proof (auto simp: einterval_iff)
     fix x assume "a < ereal x" "ereal x < b"
     have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially"

   and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
   shows
     "set_integrable lborel (einterval A B) f"
     "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
 proof -
-  from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
-  note less_imp_le [simp]
+  from einterval_Icc_approximation[OF \<open>a < b\<close>] 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 < ereal (l i)"
+    "\<And>i. ereal (u i) < b"
+    "(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
+    "(\<lambda>x. ereal (u x)) \<longlonglongrightarrow> b" by this auto
   have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
   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 llb[simp]: "\<And>i. l i < b"

       using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
       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: incseq_def)
     have "ereal (g (l 0)) \<le> ereal (g (u 0))"
-      by auto
+      by (auto simp: less_imp_le)
     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"

   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')
+           apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
       done
     then show ?thesis
       by (simp add: ac_simps)
   qed
   have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"

     have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x) \<longlonglongrightarrow> ?l"
       by (intro assms interval_integral_Icc_approx_integrable [OF \<open>a < b\<close> approx])
     hence "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> ?l"
       by (simp add: eq1)
     then show "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) \<longlonglongrightarrow> ?l"
-      unfolding interval_lebesgue_integral_def by auto
+      unfolding interval_lebesgue_integral_def by (auto simp: less_imp_le)
     have "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
       using aless f_nonneg img lessb by blast
     then show "\<And>x i. x \<in> {g (l i)<..<g (u i)} \<Longrightarrow> 0 \<le> f x"
       using less_eq_real_def by auto
   qed (auto simp: greaterThanLessThan_borel)