# HG changeset patch
# User wenzelm
# Date 1632515006 -7200
# Node ID 0135a0c77b64e75eff1f5ddc4f4ea211001cfd1e
# Parent  9e71155e36666cf5fa6bbdc7462c08ec77d2daa1
tuned proofs --- avoid 'guess';

diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -50,9 +50,8 @@
   proof (cases "x \<in> A")
     assume x: "x \<in> A"
     hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
-    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
-      using 1 open_greaterThanLessThan by blast
-    then guess U .. note U = this
+    with 1 obtain U where U: "open U" "x \<in> U" "\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set)"
+      using open_greaterThanLessThan by metis
     hence "\<forall>y\<in>U. indicator A y > (0::real)"
       unfolding greaterThanLessThan_def by auto
     hence "U \<subseteq> A" using indicator_eq_0_iff by force
@@ -61,9 +60,8 @@
   next
     assume x: "x \<notin> A"
     hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
-    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
-      using 1 open_greaterThanLessThan by blast
-    then guess U .. note U = this
+    with 1 obtain U where U: "open U" "x \<in> U" "\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set)"
+      using 1 open_greaterThanLessThan by metis
     hence "\<forall>y\<in>U. indicator A y < (1::real)"
       unfolding greaterThanLessThan_def by auto
     hence "U \<subseteq> -A" by auto
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -242,7 +242,11 @@
 lemma (in sigma_finite_measure) measurable_emeasure_Pair:
   assumes Q: "Q \<in> sets (N \<Otimes>\<^sub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
 proof -
-  from sigma_finite_disjoint guess F . note F = this
+  obtain F :: "nat \<Rightarrow> 'a set" where F:
+    "range F \<subseteq> sets M"
+    "\<Union> (range F) = space M"
+    "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
+    "disjoint_family F" by (blast intro: sigma_finite_disjoint)
   then have F_sets: "\<And>i. F i \<in> sets M" by auto
   let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
   { fix i
@@ -361,8 +365,16 @@
   shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and>
     (\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>)"
 proof -
-  from M1.sigma_finite_incseq guess F1 . note F1 = this
-  from M2.sigma_finite_incseq guess F2 . note F2 = this
+  obtain F1 where F1: "range F1 \<subseteq> sets M1"
+    "\<Union> (range F1) = space M1"
+    "\<And>i. emeasure M1 (F1 i) \<noteq> \<infinity>"
+    "incseq F1"
+    by (rule M1.sigma_finite_incseq) blast
+  obtain F2 where F2: "range F2 \<subseteq> sets M2"
+    "\<Union> (range F2) = space M2"
+    "\<And>i. emeasure M2 (F2 i) \<noteq> \<infinity>"
+    "incseq F2"
+    by (rule M2.sigma_finite_incseq) blast
   from F1 F2 have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto
   let ?F = "\<lambda>i. F1 i \<times> F2 i"
   show ?thesis
@@ -396,9 +408,11 @@
 
 sublocale\<^marker>\<open>tag unimportant\<close> pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
 proof
-  from M1.sigma_finite_countable guess F1 ..
-  moreover from M2.sigma_finite_countable guess F2 ..
-  ultimately show
+  obtain F1 :: "'a set set" and F2 :: "'b set set" where
+      "countable F1 \<and> F1 \<subseteq> sets M1 \<and> \<Union> F1 = space M1 \<and> (\<forall>a\<in>F1. emeasure M1 a \<noteq> \<infinity>)"
+      "countable F2 \<and> F2 \<subseteq> sets M2 \<and> \<Union> F2 = space M2 \<and> (\<forall>a\<in>F2. emeasure M2 a \<noteq> \<infinity>)"
+    using M1.sigma_finite_countable M2.sigma_finite_countable by auto
+  then show
     "\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)"
     by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI)
        (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff)
@@ -422,8 +436,10 @@
 lemma (in pair_sigma_finite) distr_pair_swap:
   "M1 \<Otimes>\<^sub>M M2 = distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D")
 proof -
-  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
+  obtain F :: "nat \<Rightarrow> ('a \<times> 'b) set" where F: "range F \<subseteq> ?E"
+    "incseq F" "\<Union> (range F) = space M1 \<times> space M2" "\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>"
+    using sigma_finite_up_in_pair_measure_generator by auto
   show ?thesis
   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
     show "?E \<subseteq> Pow (space ?P)"
@@ -432,9 +448,8 @@
       by (simp add: sets_pair_measure space_pair_measure)
     then show "sets ?D = sigma_sets (space ?P) ?E"
       by simp
-  next
-    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
-      using F by (auto simp: space_pair_measure)
+    from F show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+      by (auto simp: space_pair_measure)
   next
     fix X assume "X \<in> ?E"
     then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
@@ -899,7 +914,9 @@
   shows "sigma_finite_measure M"
 proof -
   interpret sigma_finite_measure "distr M N f" by fact
-  from sigma_finite_countable guess A .. note A = this
+  obtain A where A: "countable A" "A \<subseteq> sets (distr M N f)"
+      "\<Union> A = space (distr M N f)" "\<forall>a\<in>A. emeasure (distr M N f) a \<noteq> \<infinity>"
+    using sigma_finite_countable by auto
   show ?thesis
   proof
     show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
@@ -933,9 +950,12 @@
   interpret M1: sigma_finite_measure M1 by fact
   interpret M2: sigma_finite_measure M2 by fact
   interpret pair_sigma_finite M1 M2 ..
-  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
   let ?P = "M1 \<Otimes>\<^sub>M M2"
+  obtain F :: "nat \<Rightarrow> ('a \<times> 'b) set" where F:
+    "range F \<subseteq> ?E" "incseq F" "\<Union> (range F) = space M1 \<times> space M2" "\<forall>i. emeasure ?P (F i) \<noteq> \<infinity>"
+    using sigma_finite_up_in_pair_measure_generator
+    by blast
   show ?thesis
   proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
     show "?E \<subseteq> Pow (space ?P)"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -2952,8 +2952,12 @@
   assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
   shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
 proof -
-  from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
-  then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
+  from borel_measurable_implies_sequence_metric[OF f, of 0]
+  obtain s where s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
+    and "\<forall>x\<in>space (N \<Otimes>\<^sub>M M). (\<lambda>i. s i x) \<longlonglongrightarrow> (case x of (x, y) \<Rightarrow> f x y)"
+    and "\<forall>i. \<forall>x\<in>space (N \<Otimes>\<^sub>M M). dist (s i x) 0 \<le> 2 * dist (case x of (x, xa) \<Rightarrow> f x xa) 0"
+    by auto
+  then have *:
     "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
     "\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
     by (auto simp: space_pair_measure)
@@ -2970,7 +2974,7 @@
   { fix i x assume "x \<in> space N"
     then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
       (\<Sum>z\<in>s i ` (space N \<times> space M). measure M {y \<in> space M. s i (x, y) = z} *\<^sub>R z)"
-      using s(1)[THEN simple_functionD(1)]
+      using s[THEN simple_functionD(1)]
       unfolding simple_bochner_integral_def
       by (intro sum.mono_neutral_cong_left)
          (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
@@ -2991,9 +2995,9 @@
         show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
           using x by simp
         show "AE xa in M. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f x xa"
-          using x s(2) by auto
+          using x * by auto
         show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
-          using x s(3) by auto
+          using x * by auto
       qed fact
       moreover
       { fix i
@@ -3006,7 +3010,7 @@
             by (intro simple_function_borel_measurable)
                (auto simp: space_pair_measure dest: finite_subset)
           have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
-            using x s by (intro nn_integral_mono) auto
+            using x * by (intro nn_integral_mono) auto
           also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
             using int_2f unfolding integrable_iff_bounded by simp
           finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -101,11 +101,10 @@
       thus ?thesis by auto
     qed
   qed
-  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
+  then obtain g :: "real \<Rightarrow> nat \<times> rat" where "\<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
       (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
       (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
-    by (rule bchoice)
-  then guess g ..
+    by (rule bchoice [THEN exE]) blast
   hence g: "\<And>a x. a \<in> A \<Longrightarrow> \<not> continuous (at a within A) f \<Longrightarrow> x \<in> A \<Longrightarrow>
       (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
       (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (x > a \<longrightarrow> f x > of_rat (snd (g a))))"
@@ -579,7 +578,8 @@
   "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
   unfolding second_countable_borel_measurable[OF open_generated_order]
 proof (intro sigma_eqI sigma_sets_eqI)
-  from countable_dense_setE guess D :: "'a set" . note D = this
+  obtain D :: "'a set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+    by (rule countable_dense_setE) blast
 
   interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
     by (rule sigma_algebra_sigma_sets) simp
@@ -617,7 +617,8 @@
   "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
   unfolding second_countable_borel_measurable[OF open_generated_order]
 proof (intro sigma_eqI sigma_sets_eqI)
-  from countable_dense_setE guess D :: "'a set" . note D = this
+  obtain D :: "'a set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+    by (rule countable_dense_setE) blast
 
   interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
     by (rule sigma_algebra_sigma_sets) simp
@@ -1027,7 +1028,8 @@
   then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})"
   proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
     fix x :: 'a
-    from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat ..
+    obtain k where "Max ((\<bullet>) x ` Basis) \<le> real k"
+      using real_arch_simple by blast
     then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k"
       by (subst (asm) Max_le_iff) auto
     then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia \<le> real k"
@@ -1048,8 +1050,8 @@
       (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
   proof (safe, simp_all add: eucl_less_def split: if_split_asm)
     fix x :: 'a
-    from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
-    guess k::nat .. note k = this
+    obtain k where k: "Max ((\<bullet>) (- x) ` Basis) < real k"
+      using reals_Archimedean2 by blast
     { fix i :: 'a assume "i \<in> Basis"
       then have "-x\<bullet>i < real k"
         using k by (subst (asm) Max_less_iff) auto
@@ -1074,8 +1076,8 @@
   also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
   proof (safe, simp_all add: eucl_less_def split: if_split_asm)
     fix x :: 'a
-    from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
-    guess k::nat .. note k = this
+    obtain k where k: "Max ((\<bullet>) x ` Basis) < real k"
+      using reals_Archimedean2 by blast
     { fix i :: 'a assume "i \<in> Basis"
       then have "x\<bullet>i < real k"
         using k by (subst (asm) Max_less_iff) auto
@@ -1098,8 +1100,8 @@
   have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
   proof (safe, simp_all add: eucl_le[where 'a='a])
     fix x :: 'a
-    from real_arch_simple[of "Max ((\<lambda>i. - x\<bullet>i)`Basis)"]
-    guess k::nat .. note k = this
+    obtain k where k: "Max ((\<bullet>) (- x) ` Basis) \<le> real k"
+      using real_arch_simple by blast
     { fix i :: 'a assume "i \<in> Basis"
       with k have "- x\<bullet>i \<le> real k"
         by (subst (asm) Max_le_iff) (auto simp: field_simps)
@@ -1808,9 +1810,7 @@
 proof -
   from assms is_real_interval have "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or>
     S = {a<..} \<or> S = {a..} \<or> S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}" by auto
-  then guess a ..
-  then guess b ..
-  thus ?thesis
+  then show ?thesis
     by auto
 qed
 
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Caratheodory.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -564,8 +564,9 @@
   let ?R = generated_ring
   have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)"
     by (auto simp: generated_ring_def)
-  from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this
-
+  from bchoice[OF this] obtain \<mu>'
+    where \<mu>'_spec: "\<forall>x\<in>generated_ring. \<exists>C\<subseteq>M. x = \<Union> C \<and> finite C \<and> disjoint C \<and> \<mu>' x = sum \<mu> C"
+    by blast
   { fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
     fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
     assume "\<Union>C = \<Union>D"
@@ -609,15 +610,19 @@
     fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a"
       by (simp add: disjoint_def)
   next
-    fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+    fix a assume "a \<in> ?R"
+    then obtain Ca where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca" ..
     with \<mu>'[of Ca] \<open>volume M \<mu>\<close>[THEN volume_positive]
     show "0 \<le> \<mu>' a"
       by (auto intro!: sum_nonneg)
   next
     show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto
   next
-    fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
-    fix b assume "b \<in> ?R" then guess Cb .. note Cb = this
+    fix a b assume "a \<in> ?R" "b \<in> ?R"
+    then obtain Ca Cb
+      where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+        and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+      by (meson generated_ringE)
     assume "a \<inter> b = {}"
     with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
     then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
@@ -650,7 +655,7 @@
     fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C"
     have "\<exists>F'. bij_betw F' {..<card C} C"
       by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
-    then guess F' .. note F' = this
+    then obtain F' where "bij_betw F' {..<card C} C" ..
     then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
       by (auto simp: bij_betw_def)
     { fix i j assume *: "i < card C" "j < card C" "i \<noteq> j"
@@ -698,10 +703,12 @@
 
   have "countably_additive generated_ring \<mu>_r"
   proof (rule countably_additiveI)
-    fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
+    fix A' :: "nat \<Rightarrow> 'a set"
+    assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
       and Un_A: "(\<Union>i. A' i) \<in> generated_ring"
 
-    from generated_ringE[OF Un_A] guess C' . note C' = this
+    obtain C' where C': "finite C'" "disjoint C'" "C' \<subseteq> M" "\<Union> (range A') = \<Union> C'"
+      using generated_ringE[OF Un_A] by auto
 
     { fix c assume "c \<in> C'"
       moreover define A where [abs_def]: "A i = A' i \<inter> c" for i
@@ -717,11 +724,11 @@
       proof
         fix i
         from A have Ai: "A i \<in> generated_ring" by auto
-        from generated_ringE[OF this] guess C . note C = this
-
+        from generated_ringE[OF this] obtain C
+          where C: "finite C" "disjoint C" "C \<subseteq> M" "A i = \<Union> C" by auto
         have "\<exists>F'. bij_betw F' {..<card C} C"
           by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
-        then guess F .. note F = this
+        then obtain F where F: "bij_betw F {..<card C} C" ..
         define f where [abs_def]: "f i = (if i < card C then F i else {})" for i
         then have f: "bij_betw f {..< card C} C"
           by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
@@ -750,7 +757,9 @@
         ultimately show "?P i"
           by blast
       qed
-      from choice[OF this] guess f .. note f = this
+      from choice[OF this] obtain f
+        where f: "\<forall>x. \<mu>_r (A x) = (\<Sum>j. \<mu>_r (f x j)) \<and> disjoint_family (f x) \<and> \<Union> (range (f x)) = A x \<and> (\<forall>j. f x j \<in> M)"
+        ..
       then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
         unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
 
@@ -808,8 +817,8 @@
     finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
       using C' by simp
   qed
-  from G.caratheodory'[OF \<open>positive generated_ring \<mu>_r\<close> \<open>countably_additive generated_ring \<mu>_r\<close>]
-  guess \<mu>' ..
+  obtain \<mu>' where "(\<forall>s\<in>generated_ring. \<mu>' s = \<mu>_r s) \<and> measure_space \<Omega> (sigma_sets \<Omega> generated_ring) \<mu>'"
+    using G.caratheodory'[OF pos \<open>countably_additive generated_ring \<mu>_r\<close>] by auto
   with V show ?thesis
     unfolding sigma_sets_generated_ring_eq
     by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -52,16 +52,18 @@
   show "{} \<in> ?A" by auto
 next
   let ?C = "space M"
-  fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .
+  fix A assume "A \<in> ?A"
+  then obtain S N N'
+    where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
+    by (rule completionE)
   then show "space M - A \<in> ?A"
     by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto
 next
   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A"
   then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'"
     by (auto simp: image_subset_iff)
-  from choice[OF this] guess S ..
-  from choice[OF this] guess N ..
-  from choice[OF this] guess N' ..
+  then obtain S N N' where "\<forall>x. A x = S x \<union> N x \<and> S x \<in> sets M \<and> N' x \<in> null_sets M \<and> N x \<subseteq> N' x"
+    by metis
   then show "\<Union>(A ` UNIV) \<in> ?A"
     using null_sets_UN[of N']
     by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
@@ -104,7 +106,8 @@
   show ?thesis
     unfolding main_part_def null_part_def if_not_P[OF nA]
   proof (rule someI2_ex)
-    from assms[THEN sets_completionE] guess S N N' . note A = this
+    from assms obtain S N N' where A: "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
+      by (blast intro: sets_completionE)
     let ?P = "(S, N - S)"
     show "\<exists>p. split_completion M A p"
       unfolding split_completion_def if_not_P[OF nA] using A
@@ -140,12 +143,11 @@
   assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
 proof -
   have S: "S \<in> sets (completion M)" using assms by auto
-  have "S - main_part M S \<in> sets M" using assms by auto
-  moreover
+  have *: "S - main_part M S \<in> sets M" using assms by auto
   from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
   have "S - main_part M S = null_part M S" by auto
-  ultimately show sets: "null_part M S \<in> sets M" by auto
-  from null_part[OF S] guess N ..
+  with * show sets: "null_part M S \<in> sets M" by auto
+  from null_part[OF S] obtain N where "N \<in> null_sets M \<and> null_part M S \<subseteq> N" ..
   with emeasure_eq_0[of N _ "null_part M S"] sets
   show "emeasure M (null_part M S) = 0" by auto
 qed
@@ -159,10 +161,10 @@
   then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto
   have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N"
     using null_part[OF S] by auto
-  from choice[OF this] guess N .. note N = this
+  then obtain N where N: "\<forall>x. N x \<in> null_sets M \<and> null_part M (S x) \<subseteq> N x" by metis
   then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto
-  have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto
-  from null_part[OF this] guess N' .. note N' = this
+  from S have "(\<Union>i. S i) \<in> sets (completion M)" by auto
+  from null_part[OF this] obtain N' where N': "N' \<in> null_sets M \<and> null_part M (\<Union> (range S)) \<subseteq> N'" ..
   let ?N = "(\<Union>i. N i) \<union> N'"
   have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto
   have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N"
@@ -288,21 +290,24 @@
   assumes g: "g \<in> borel_measurable (completion M)"
   shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
 proof -
-  from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
-  from this(1)[THEN completion_ex_simple_function]
+  obtain f :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal"
+    where *: "\<And>i. simple_function (completion M) (f i)"
+      and **: "\<And>x. (SUP i. f i x) = g x"
+    using g[THEN borel_measurable_implies_simple_function_sequence'] by metis
+  from *[THEN completion_ex_simple_function]
   have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
-  from this[THEN choice] obtain f' where
-    sf: "\<And>i. simple_function M (f' i)" and
-    AE: "\<forall>i. AE x in M. f i x = f' i x" by auto
+  then obtain f'
+    where sf: "\<And>i. simple_function M (f' i)"
+      and AE: "\<forall>i. AE x in M. f i x = f' i x"
+    by metis
   show ?thesis
   proof (intro bexI)
     from AE[unfolded AE_all_countable[symmetric]]
     show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
     proof (elim AE_mp, safe intro!: AE_I2)
       fix x assume eq: "\<forall>i. f i x = f' i x"
-      moreover have "g x = (SUP i. f i x)"
-        unfolding f by (auto split: split_max)
-      ultimately show "g x = ?f x" by auto
+      have "g x = (SUP i. f i x)" by (auto simp: ** split: split_max)
+      with eq show "g x = ?f x" by auto
     qed
     show "?f \<in> borel_measurable M"
       using sf[THEN borel_measurable_simple_function] by auto
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -269,11 +269,24 @@
 qed
 
 lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
-proof (unfold Int_stable_def, safe)
+  unfolding Int_stable_def
+proof safe
   fix A assume "A \<in> prod_algebra I M"
-  from prod_algebraE[OF this] guess J E . note A = this
+  from prod_algebraE[OF this] obtain J E where A:
+    "A = prod_emb I M J (Pi\<^sub>E J E)"
+    "finite J"
+    "J \<noteq> {} \<or> I = {}"
+    "J \<subseteq> I"
+    "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
+    by auto
   fix B assume "B \<in> prod_algebra I M"
-  from prod_algebraE[OF this] guess K F . note B = this
+  from prod_algebraE[OF this] obtain K F where B:
+    "B = prod_emb I M K (Pi\<^sub>E K F)"
+    "finite K"
+    "K \<noteq> {} \<or> I = {}"
+    "K \<subseteq> I"
+    "\<And>i. i \<in> K \<Longrightarrow> F i \<in> sets (M i)"
+    by auto
   have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^sub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter>
       (if i \<in> K then F i else space (M i)))"
     unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
@@ -360,7 +373,13 @@
 proof (rule sigma_sets_eqI)
   interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
   fix A assume "A \<in> prod_algebra I M"
-  from prod_algebraE[OF this] guess J X . note X = this
+  from prod_algebraE[OF this] obtain J X where X:
+    "A = prod_emb I M J (Pi\<^sub>E J X)"
+    "finite J"
+    "J \<noteq> {} \<or> I = {}"
+    "J \<subseteq> I"
+    "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+    by auto
   show "A \<in> sigma_sets ?\<Omega> ?R"
   proof cases
     assume "I = {}"
@@ -525,7 +544,13 @@
   using sets_PiM prod_algebra_sets_into_space space
 proof (rule measurable_sigma_sets)
   fix A assume "A \<in> prod_algebra I M"
-  from prod_algebraE[OF this] guess J X .
+  from prod_algebraE[OF this] obtain J X where
+    "A = prod_emb I M J (Pi\<^sub>E J X)"
+    "finite J"
+    "J \<noteq> {} \<or> I = {}"
+    "J \<subseteq> I"
+    "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+    by auto
   with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
 qed
 
@@ -537,7 +562,14 @@
   using sets_PiM prod_algebra_sets_into_space space
 proof (rule measurable_sigma_sets)
   fix A assume "A \<in> prod_algebra I M"
-  from prod_algebraE[OF this] guess J X . note X = this
+  from prod_algebraE[OF this] obtain J X
+    where X:
+      "A = prod_emb I M J (Pi\<^sub>E J X)"
+      "finite J"
+      "J \<noteq> {} \<or> I = {}"
+      "J \<subseteq> I"
+      "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+    by auto
   then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
     using space by (auto simp: prod_emb_def del: PiE_I)
   also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
@@ -844,7 +876,9 @@
 proof -
   have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. emeasure (M i) (F k) \<noteq> \<infinity>)"
     using M.sigma_finite_incseq by metis
-  from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
+  then obtain F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
+    where "\<forall>x. range (F x) \<subseteq> sets (M x) \<and> incseq (F x) \<and> \<Union> (range (F x)) = space (M x) \<and> (\<forall>k. emeasure (M x) (F x k) \<noteq> \<infinity>)"
+    by metis
   then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. emeasure (M i) (F i k) \<noteq> \<infinity>"
     by auto
   let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k"
@@ -950,8 +984,11 @@
   shows "P = PiM I M"
 proof -
   interpret finite_product_sigma_finite M I
-    proof qed fact
-  from sigma_finite_pairs guess C .. note C = this
+    by standard fact
+  from sigma_finite_pairs obtain C where C:
+    "\<forall>i\<in>I. range (C i) \<subseteq> sets (M i)" "\<forall>k. \<forall>i\<in>I. emeasure (M i) (C i k) \<noteq> \<infinity>"
+    "incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I. C i k)" "(\<Union>k. \<Pi>\<^sub>E i\<in>I. C i k) = space (Pi\<^sub>M I M)"
+    by auto
   show ?thesis
   proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
     show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -388,7 +388,9 @@
 
   have "summable (\<lambda>k. inverse ((real_of_nat k)^2))"
     by (rule inverse_power_summable) simp
-  from summable_partial_sum_bound[OF this e'] guess M . note M = this
+  from summable_partial_sum_bound[OF this e']
+  obtain M where M: "\<And>m n. M \<le> m \<Longrightarrow> norm (\<Sum>k = m..n. inverse ((real k)\<^sup>2)) < e'"
+    by auto
 
   define N where "N = max 2 (max (nat \<lceil>2 * (norm z + d)\<rceil>) M)"
   {
@@ -910,7 +912,8 @@
   assume n: "n = 0"
   let ?f = "\<lambda>k z. inverse (of_nat (Suc k)) - inverse (z + of_nat k)"
   let ?F = "\<lambda>z. \<Sum>k. ?f k z" and ?f' = "\<lambda>k z. inverse ((z + of_nat k)\<^sup>2)"
-  from no_nonpos_Int_in_ball'[OF z] guess d . note d = this
+  from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\<And>t. t \<in> ball z d \<Longrightarrow> t \<notin> \<int>\<^sub>\<le>\<^sub>0"
+    by auto
   from z have summable: "summable (\<lambda>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k))"
     by (intro summable_Digamma) force
   from z have conv: "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)\<^sup>2))"
@@ -931,7 +934,8 @@
 next
   assume n: "n \<noteq> 0"
   from z have z': "z \<noteq> 0" by auto
-  from no_nonpos_Int_in_ball'[OF z] guess d . note d = this
+  from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\<And>t. t \<in> ball z d \<Longrightarrow> t \<notin> \<int>\<^sub>\<le>\<^sub>0"
+    by auto
   define n' where "n' = Suc n"
   from n have n': "n' \<ge> 2" by (simp add: n'_def)
   have "((\<lambda>z. \<Sum>k. inverse ((z + of_nat k) ^ n')) has_field_derivative
@@ -1293,7 +1297,9 @@
     case False
     have "rGamma_series z \<longlonglongrightarrow> exp (- ln_Gamma z)"
     proof (rule Lim_transform_eventually)
-      from ln_Gamma_series_complex_converges'[OF False] guess d by (elim exE conjE)
+      from ln_Gamma_series_complex_converges'[OF False]
+      obtain d where "0 < d" "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n)"
+        by auto
       from this(1) uniformly_convergent_imp_convergent[OF this(2), of z]
         have "ln_Gamma_series z \<longlonglongrightarrow> lim (ln_Gamma_series z)" by (simp add: convergent_LIMSEQ_iff)
       thus "(\<lambda>n. exp (-ln_Gamma_series z n)) \<longlonglongrightarrow> exp (- ln_Gamma z)"
@@ -1762,9 +1768,12 @@
 proof -
   have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
-  then guess \<xi> by (elim exE conjE) note \<xi> = this
-  note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> > 0"
+  then obtain \<xi>
+    where \<xi>: "x < \<xi>" "\<xi> < y"
+      and Polygamma: "Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
+    by auto
+  note Polygamma
+  also from \<xi> assms have "(y - x) * Polygamma (Suc n) \<xi> > 0"
     by (intro mult_pos_pos Polygamma_real_odd_pos) (auto elim!: nonpos_Ints_cases)
   finally show ?thesis by simp
 qed
@@ -1775,9 +1784,12 @@
 proof -
   have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
-  then guess \<xi> by (elim exE conjE) note \<xi> = this
-  note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> < 0"
+  then obtain \<xi>
+    where \<xi>: "x < \<xi>" "\<xi> < y"
+      and Polygamma: "Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
+    by auto
+  note Polygamma
+  also from \<xi> assms have "(y - x) * Polygamma (Suc n) \<xi> < 0"
     by (intro mult_pos_neg Polygamma_real_even_neg) simp_all
   finally show ?thesis by simp
 qed
@@ -1809,9 +1821,11 @@
 proof -
   have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> ln_Gamma y - ln_Gamma x = (y - x) * Digamma \<xi>"
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
-  then guess \<xi> by (elim exE conjE) note \<xi> = this
-  note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Digamma \<xi> > 0"
+  then obtain \<xi> where \<xi>: "x < \<xi>" "\<xi> < y"
+    and ln_Gamma: "ln_Gamma y - ln_Gamma x = (y - x) * Digamma \<xi>"
+    by auto
+  note ln_Gamma
+  also from \<xi> assms have "(y - x) * Digamma \<xi> > 0"
     by (intro mult_pos_pos Digamma_real_ge_three_halves_pos) simp_all
   finally show ?thesis by simp
 qed
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -72,7 +72,7 @@
   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
@@ -81,7 +81,12 @@
     "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)
@@ -98,8 +103,18 @@
     "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)
@@ -944,8 +959,15 @@
     "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"
@@ -976,7 +998,7 @@
     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
@@ -1002,7 +1024,7 @@
     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)
@@ -1031,7 +1053,7 @@
     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"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -1142,7 +1142,9 @@
   assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M")
   shows "emeasure M {x\<in>space M. P x} = emeasure M (space M)"
 proof -
-  from AE_E[OF AE] guess N . note N = this
+  from AE_E[OF AE] obtain N
+    where N: "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+    by auto
   with sets have "emeasure M (space M) \<le> emeasure M (?P \<union> N)"
     by (intro emeasure_mono) auto
   also have "\<dots> \<le> emeasure M ?P + emeasure M N"
@@ -1513,10 +1515,13 @@
     and AE: "AE x in distr M M' f. P x"
   shows "AE x in M. P (f x)"
 proof -
-  from AE[THEN AE_E] guess N .
+  from AE[THEN AE_E] obtain N
+    where "{x \<in> space (distr M M' f). \<not> P x} \<subseteq> N"
+      "emeasure (distr M M' f) N = 0"
+      "N \<in> sets (distr M M' f)"
+    by auto
   with f show ?thesis
-    unfolding eventually_ae_filter
-    by (intro bexI[of _ "f -` N \<inter> space M"])
+    by (simp add: eventually_ae_filter, intro bexI[of _ "f -` N \<inter> space M"])
        (auto simp: emeasure_distr measurable_def)
 qed
 
@@ -2352,9 +2357,9 @@
     show "(\<lambda>i. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
     proof cases
       assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
-      then guess i .. note i = this
-      { fix j from i \<open>incseq F\<close> have "F j \<subseteq> F i"
-          by (cases "i \<le> j") (auto simp: incseq_def) }
+      then obtain i where i: "\<forall>j\<ge>i. F i = F j" ..
+      with \<open>incseq F\<close> have "F j \<subseteq> F i" for j
+        by (cases "i \<le> j") (auto simp: incseq_def)
       then have eq: "(\<Union>i. F i) = F i"
         by auto
       with i show ?thesis
@@ -2375,7 +2380,7 @@
         fix n :: nat show "\<exists>k::nat\<in>UNIV. of_nat n \<le> ?M (F k)"
         proof (induct n)
           case (Suc n)
-          then guess k .. note k = this
+          then obtain k where "of_nat n \<le> ?M (F k)" ..
           moreover have "finite (F k) \<Longrightarrow> finite (F (f k)) \<Longrightarrow> card (F k) < card (F (f k))"
             using \<open>F k \<subset> F (f k)\<close> by (simp add: psubset_card_mono)
           moreover have "finite (F (f k)) \<Longrightarrow> finite (F k)"
@@ -2842,16 +2847,19 @@
     show "finite_measure (restrict_space M A)" "finite_measure (restrict_space N A)"
       by (auto simp: space_restrict_space emeasure_restrict_space less_top intro!: finite_measureI)
   qed (simp add: sets_restrict_space)
-  then guess Y ..
   then show ?thesis
-    apply (intro bexI[of _ Y] conjI ballI conjI)
-    apply (simp_all add: sets_restrict_space emeasure_restrict_space)
-    apply safe
-    subgoal for X Z
-      by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
-    subgoal for X Z
-      by (erule ballE[of _ _ X])  (auto simp add: Int_absorb1 ac_simps)
-    apply auto
+    apply -
+    apply (erule bexE)
+    subgoal for Y
+      apply (intro bexI[of _ Y] conjI ballI conjI)
+         apply (simp_all add: sets_restrict_space emeasure_restrict_space)
+         apply safe
+      subgoal for X Z
+        by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
+      subgoal for X Z
+        by (erule ballE[of _ _ X])  (auto simp add: Int_absorb1 ac_simps)
+      apply auto
+      done
     done
 qed
 
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -862,7 +862,9 @@
   unfolding nn_integral_def
 proof (safe intro!: SUP_mono)
   fix n assume n: "simple_function M n" "n \<le> u"
-  from ae[THEN AE_E] guess N . note N = this
+  from ae[THEN AE_E] obtain N
+    where N: "{x \<in> space M. \<not> u x \<le> v x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+    by auto
   then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in)
   let ?n = "\<lambda>x. n x * indicator (space M - N) x"
   have "AE x in M. n x \<le> ?n x" "simple_function M ?n"
@@ -1000,7 +1002,9 @@
 proof -
   from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x"
     by (simp add: AE_all_countable)
-  from this[THEN AE_E] guess N . note N = this
+  from this[THEN AE_E] obtain N
+    where N: "{x \<in> space M. \<not> (\<forall>i. f i x \<le> f (Suc i) x)} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+    by auto
   let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
   have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
   then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
@@ -1045,14 +1049,24 @@
   shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
     (is "integral\<^sup>N M ?L = _")
 proof -
-  from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
+  obtain u
+    where "\<And>i. simple_function M (u i)" "incseq u" "\<And>i x. u i x < top" "\<And>x. (SUP i. u i x) = f x"
+    using borel_measurable_implies_simple_function_sequence' f(1)
+    by auto
   note u = nn_integral_monotone_convergence_simple[OF this(2,1)] this
-  from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
+
+  obtain v where
+    "\<And>i. simple_function M (v i)" "incseq v" "\<And>i x. v i x < top" "\<And>x. (SUP i. v i x) = g x"
+    using borel_measurable_implies_simple_function_sequence' g(1)
+    by auto
   note v = nn_integral_monotone_convergence_simple[OF this(2,1)] this
+
   let ?L' = "\<lambda>i x. a * u i x + v i x"
 
   have "?L \<in> borel_measurable M" using assms by auto
-  from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
+  from borel_measurable_implies_simple_function_sequence'[OF this]
+  obtain l where "\<And>i. simple_function M (l i)" "incseq l" "\<And>i x. l i x < top" "\<And>x. (SUP i. l i x) = a * f x + g x"
+    by auto
   note l = nn_integral_monotone_convergence_simple[OF this(2,1)] this
 
   have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -261,7 +261,10 @@
     from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \<le> N (space M)"
       by (simp cong: nn_integral_cong)
   qed
-  from ennreal_SUP_countable_SUP [OF \<open>G \<noteq> {}\<close>, of "integral\<^sup>N M"] guess ys .. note ys = this
+  from ennreal_SUP_countable_SUP [OF \<open>G \<noteq> {}\<close>, of "integral\<^sup>N M"]
+  obtain ys :: "nat \<Rightarrow> ennreal"
+    where ys: "range ys \<subseteq> integral\<^sup>N M ` G \<and> Sup (integral\<^sup>N M ` G) = Sup (range ys)"
+    by auto
   then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n"
   proof safe
     fix n assume "range ys \<subseteq> integral\<^sup>N M ` G"
@@ -774,8 +777,11 @@
 next
   assume eq: "density M f = density M g"
   interpret f: sigma_finite_measure "density M f" by fact
-  from f.sigma_finite_incseq guess A . note cover = this
-
+  from f.sigma_finite_incseq obtain A where cover: "range A \<subseteq> sets (density M f)"
+    "\<Union> (range A) = space (density M f)"
+    "\<And>i. emeasure (density M f) (A i) \<noteq> \<infinity>"
+    "incseq A"
+    by auto
   have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
     unfolding AE_all_countable
   proof
@@ -821,7 +827,9 @@
     using fin by (auto elim!: AE_Ball_mp simp: less_top ennreal_mult_less_top)
 next
   assume AE: "AE x in M. f x \<noteq> \<infinity>"
-  from sigma_finite guess Q . note Q = this
+  from sigma_finite obtain Q :: "nat \<Rightarrow> 'a set"
+    where Q: "range Q \<subseteq> sets M" "\<Union> (range Q) = space M" "\<And>i. emeasure M (Q i) \<noteq> \<infinity>"
+    by auto
   define A where "A i =
     f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ennreal(of_nat (Suc n))}) \<inter> space M" for i
   { fix i j have "A i \<inter> Q j \<in> sets M"
@@ -977,7 +985,8 @@
   let ?M' = "distr M M' T" and ?N' = "distr N M' T"
   interpret M': sigma_finite_measure ?M'
   proof
-    from sigma_finite_countable guess F .. note F = this
+    from sigma_finite_countable obtain F
+      where F: "countable F \<and> F \<subseteq> sets M \<and> \<Union> F = space M \<and> (\<forall>a\<in>F. emeasure M a \<noteq> \<infinity>)" ..
     show "\<exists>A. countable A \<and> A \<subseteq> sets (distr M M' T) \<and> \<Union>A = space (distr M M' T) \<and> (\<forall>a\<in>A. emeasure (distr M M' T) a \<noteq> \<infinity>)"
     proof (intro exI conjI ballI)
       show *: "(\<lambda>A. T' -` A \<inter> space ?M') ` F \<subseteq> sets ?M'"
@@ -992,7 +1001,7 @@
       have Fi: "A \<in> sets M" using F \<open>A\<in>F\<close> by auto
       ultimately show "emeasure ?M' X \<noteq> \<infinity>"
         using F T T' \<open>A\<in>F\<close> by (simp add: emeasure_distr)
-    qed (insert F, auto)
+    qed (use F in auto)
   qed
   have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
     using T ac by measurable
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Regularity.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -30,7 +30,9 @@
     (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ennreal e) \<Longrightarrow> ?outer A"
     by (rule ennreal_approx_INF)
        (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
-  from countable_dense_setE guess X::"'a set"  . note X = this
+  from countable_dense_setE obtain X :: "'a set"
+    where X: "countable X" "\<And>Y :: 'a set. open Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> \<exists>d\<in>X. d \<in> Y"
+    by auto
   {
     fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
     with X(2)[OF this]
@@ -114,7 +116,7 @@
     proof safe
       show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed)
       fix e'::real assume "0 < e'"
-      from nat_approx_posE[OF this] guess n . note n = this
+      then obtain n where n: "1 / real (Suc n) < e'" by (rule nat_approx_posE)
       let ?k = "from_nat_into X ` {0..k e (Suc n)}"
       have "finite ?k" by simp
       moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
@@ -164,12 +166,11 @@
       proof (auto simp del: of_nat_Suc, rule ccontr)
         fix x
         assume "infdist x A \<noteq> 0"
-        hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
-        from nat_approx_posE[OF this] guess n .
-        moreover
+        then have pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
+        then obtain n where n: "1 / real (Suc n) < infdist x A" by (rule nat_approx_posE)
         assume "\<forall>i. infdist x A < 1 / real (Suc i)"
-        hence "infdist x A < 1 / real (Suc n)" by auto
-        ultimately show False by simp
+        then have "infdist x A < 1 / real (Suc n)" by auto
+        with n show False by simp
       qed
       also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
       proof (rule INF_emeasure_decseq[symmetric], safe)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -415,7 +415,7 @@
     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
     proof cases
       assume "\<exists>i. x \<in> A i"
-      then guess i ..
+      then obtain i where "x \<in> A i" ..
       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
       show ?thesis
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -669,7 +669,8 @@
     case (Union a)
     then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x"
       by (auto simp: image_iff Bex_def)
-    from choice[OF this] guess f ..
+    then obtain f where "\<forall>x. f x \<in> sigma_sets sp st \<and> a x = A \<inter> f x"
+      by metis
     then show ?case
       by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
                simp add: image_iff)
@@ -771,8 +772,9 @@
     next
       case (Union F)
       then have "\<forall>i. \<exists>B. F i = X -` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" by auto
-      from choice[OF this] guess A .. note A = this
-      with A show ?case
+      then obtain A where "\<forall>x. F x = X -` A x \<inter> \<Omega> \<and> A x \<in> sigma_sets \<Omega>' M'"
+        by metis
+      then show ?case
         by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union)
     qed
   qed
@@ -843,13 +845,15 @@
   and "a \<inter> b = {}"
   shows "a \<union> b \<in> generated_ring"
 proof -
-  from a guess Ca .. note Ca = this
-  from b guess Cb .. note Cb = this
+  from a b obtain Ca Cb
+    where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+      and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+    using generated_ringE by metis
   show ?thesis
   proof
-    show "disjoint (Ca \<union> Cb)"
-      using \<open>a \<inter> b = {}\<close> Ca Cb by (auto intro!: disjoint_union)
-  qed (insert Ca Cb, auto)
+    from \<open>a \<inter> b = {}\<close> Ca Cb show "disjoint (Ca \<union> Cb)"
+      by (auto intro!: disjoint_union)
+  qed (use Ca Cb in auto)
 qed
 
 lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring"
@@ -867,8 +871,10 @@
   assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
   shows "a \<inter> b \<in> generated_ring"
 proof -
-  from a guess Ca .. note Ca = this
-  from b guess Cb .. note Cb = this
+  from a b obtain Ca Cb
+    where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+      and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+    using generated_ringE by metis
   define C where "C = (\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
   show ?thesis
   proof
@@ -890,7 +896,7 @@
         then show ?thesis by auto
       qed
     qed
-  qed (insert Ca Cb, auto simp: C_def)
+  qed (use Ca Cb in \<open>auto simp: C_def\<close>)
 qed
 
 lemma (in semiring_of_sets) generated_ring_Inter:
@@ -909,9 +915,12 @@
     using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
   show "{} \<in> ?R" by (rule generated_ring_empty)
 
-  { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this
-    fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this
-
+  {
+    fix a b assume "a \<in> ?R" "b \<in> ?R"
+    then obtain Ca Cb
+      where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+        and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+      using generated_ringE by metis
     show "a - b \<in> ?R"
     proof cases
       assume "Cb = {}" with Cb \<open>a \<in> ?R\<close> show ?thesis
@@ -932,7 +941,8 @@
         show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+
       qed
       finally show "a - b \<in> ?R" .
-    qed }
+    qed
+  }
   note Diff = this
 
   fix a b assume sets: "a \<in> ?R" "b \<in> ?R"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -115,7 +115,7 @@
   define n where "n = nat \<lceil>log c K\<rceil>"
   from unbounded have "\<exists>m>n. c < root m (norm (f m))" unfolding bdd_above_def
     by (auto simp: not_le)
-  then guess m by (elim exE conjE) note m = this
+  then obtain m where m: "n < m" "c < root m (norm (f m))" by auto
   from c K have "K = c powr log c K" by (simp add: powr_def log_def)
   also from c have "c powr log c K \<le> c powr real n" unfolding n_def
     by (intro powr_mono, linarith, simp)
@@ -526,7 +526,7 @@
     with assms show ?thesis by simp
   next
     assume "\<exists>l'. l = ereal l' \<and> l' > 0"
-    then guess l' by (elim exE conjE) note l' = this
+    then obtain l' where l': "l = ereal l'" "0 < l'" by auto
     hence "l \<noteq> \<infinity>" by auto
     have "l * ereal (norm z) < l * conv_radius f"
       by (intro ereal_mult_strict_left_mono) (simp_all add: l' assms)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Combinatorics/Multiset_Permutations.thy
--- a/src/HOL/Combinatorics/Multiset_Permutations.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Combinatorics/Multiset_Permutations.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -131,7 +131,7 @@
 
 lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \<noteq> {}"
 proof -
-  from ex_mset[of A] guess xs ..
+  from ex_mset[of A] obtain xs where "mset xs = A" ..
   thus ?thesis by (auto simp: permutations_of_multiset_def)
 qed
 
@@ -142,7 +142,8 @@
   from ex_mset[of A] obtain ys where ys: "mset ys = A" ..
   with A have "mset xs = mset (map f ys)" 
     by (simp add: permutations_of_multiset_def)
-  from mset_eq_permutation[OF this] guess \<sigma> . note \<sigma> = this
+  then obtain \<sigma> where \<sigma>: "\<sigma> permutes {..<length (map f ys)}" "permute_list \<sigma> (map f ys) = xs"
+    by (rule mset_eq_permutation)
   with ys have "xs = map f (permute_list \<sigma> ys)"
     by (simp add: permute_list_map)
   moreover from \<sigma> ys have "permute_list \<sigma> ys \<in> permutations_of_multiset A"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Complex_Analysis/Complex_Residues.thy
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -363,9 +363,11 @@
   assumes "f has_fps_expansion F"
   shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
 proof -
-  from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
-  have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
-    using assms s unfolding has_fps_expansion_def
+  from has_fps_expansion_imp_holomorphic[OF assms] obtain s
+    where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
+    by auto
+  with assms have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
+    unfolding has_fps_expansion_def
     by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
   also from assms have "\<dots> = fps_nth F n"
     by (subst fps_nth_fps_expansion) auto
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -755,8 +755,7 @@
       thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
     next
       case True
-      then guess b by (elim exE conjE) note b = this
-
+      then obtain b where b: "b dvd a" "\<not> is_unit b" "\<not> a dvd b" by auto
       from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
       moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
       hence "?fctrs b \<noteq> ?fctrs a" by blast
@@ -766,7 +765,8 @@
       moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
       ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize b"
         by (intro less) auto
-      then guess A .. note A = this
+      then obtain A where A: "(\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (\<Prod>\<^sub># A) = normalize b"
+        by auto
 
       define c where "c = a div b"
       from b have c: "a = b * c" by (simp add: c_def)
@@ -785,7 +785,8 @@
         by (rule psubset_card_mono)
       with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize c"
         by (intro less) auto
-      then guess B .. note B = this
+      then obtain B where B: "(\<forall>x. x \<in># B \<longrightarrow> prime_elem x) \<and> normalize (\<Prod>\<^sub># B) = normalize c"
+        by auto
 
       show ?thesis
       proof (rule exI[of _ "A + B"]; safe)
@@ -840,7 +841,15 @@
     case False
     hence "a \<noteq> 0" "b \<noteq> 0" by blast+
     note nz = \<open>x \<noteq> 0\<close> this
-    from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
+    from nz[THEN prime_factorization_exists'] obtain A B C
+      where ABC:
+        "\<And>z. z \<in># A \<Longrightarrow> prime z"
+        "normalize (\<Prod>\<^sub># A) = normalize x"
+        "\<And>z. z \<in># B \<Longrightarrow> prime z"
+        "normalize (\<Prod>\<^sub># B) = normalize a"
+        "\<And>z. z \<in># C \<Longrightarrow> prime z"
+        "normalize (\<Prod>\<^sub># C) = normalize b"
+      by this blast
 
     have "irreducible (prod_mset A)"
       by (subst irreducible_cong[OF ABC(2)]) fact
@@ -855,7 +864,7 @@
            normalize (prod_mset A) dvd normalize (prod_mset C)" by simp
     thus ?thesis unfolding ABC by simp
   qed auto
-qed (insert assms, simp_all add: irreducible_def)
+qed (use assms in \<open>simp_all add: irreducible_def\<close>)
 
 lemma finite_divisor_powers:
   assumes "y \<noteq> 0" "\<not>is_unit x"
@@ -867,7 +876,14 @@
 next
   case False
   note nz = this \<open>y \<noteq> 0\<close>
-  from nz[THEN prime_factorization_exists'] guess A B . note AB = this
+  from nz[THEN prime_factorization_exists'] obtain A B
+    where AB:
+      "\<And>z. z \<in># A \<Longrightarrow> prime z"
+      "normalize (\<Prod>\<^sub># A) = normalize x"
+      "\<And>z. z \<in># B \<Longrightarrow> prime z"
+      "normalize (\<Prod>\<^sub># B) = normalize y"
+    by this blast
+
   from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
   from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
     have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp
@@ -883,7 +899,8 @@
   assumes "x \<noteq> 0"
   shows   "finite {p. prime p \<and> p dvd x}"
 proof -
-  from prime_factorization_exists'[OF assms] guess A . note A = this
+  from prime_factorization_exists'[OF assms] obtain A
+    where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize x" by this blast
   have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
   proof safe
     fix p assume p: "prime p" and dvd: "p dvd x"
@@ -925,12 +942,14 @@
   assumes "a \<noteq> 0" "\<not>is_unit a"
   shows   "\<exists>b. b dvd a \<and> prime b"
 proof -
-  from prime_factorization_exists'[OF assms(1)] guess A . note A = this
-  moreover from A and assms have "A \<noteq> {#}" by auto
+  from prime_factorization_exists'[OF assms(1)]
+  obtain A where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize a"
+    by this blast
+  with assms have "A \<noteq> {#}" by auto
   then obtain x where "x \<in># A" by blast
   with A(1) have *: "x dvd normalize (prod_mset A)" "prime x"
     by (auto simp: dvd_prod_mset)
-  hence "x dvd a" unfolding A by simp
+  hence "x dvd a" by (simp add: A(2))
   with * show ?thesis by blast
 qed
 
@@ -939,7 +958,9 @@
   shows   "P x"
 proof (cases "x = 0")
   case False
-  from prime_factorization_exists'[OF this] guess A . note A = this
+  from prime_factorization_exists'[OF this]
+  obtain A where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize x"
+    by this blast
   from A obtain u where u: "is_unit u" "x = u * prod_mset A"
     by (elim associatedE2)
 
@@ -959,7 +980,7 @@
   shows "is_unit a"
 proof (rule ccontr)
   assume "\<not>is_unit a"
-  from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
+  from prime_divisor_exists[OF assms(1) this] obtain b where "b dvd a" "prime b" by auto
   with assms(2)[of b] show False by (simp add: prime_def)
 qed
 
@@ -1138,7 +1159,8 @@
   next
     define n where "n = multiplicity p x"
     from assms have "\<not>is_unit p" by simp
-    from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
+    from multiplicity_decompose'[OF False this]
+    obtain y where y [folded n_def]: "x = p ^ multiplicity p x * y" "\<not> p dvd y" .
     from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
     also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
     also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -4079,7 +4079,7 @@
     from v have [simp]: "length v = Suc m" by (simp add: A_def natpermute_def)
     from v have "\<exists>j. j \<le> m \<and> v ! j = k" 
       by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
-    then guess j by (elim exE conjE) note j = this
+    then obtain j where j: "j \<le> m" "v ! j = k" by auto
     
     from v have "k = sum_list v" by (simp add: A_def natpermute_def)
     also have "\<dots> = (\<Sum>i=0..m. v ! i)"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -64,8 +64,13 @@
   obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d"
                   "d dvd fst x" "d dvd snd x" "d \<noteq> 0"
 proof -
-  from normalize_quotE[OF assms, of "fst x"] guess d .
-  from this show ?thesis unfolding prod.collapse by (intro that[of d])
+  from normalize_quotE[OF assms, of "fst x"] obtain d where
+    "fst x = fst (normalize_quot (fst x, snd x)) * d"
+    "snd x = snd (normalize_quot (fst x, snd x)) * d"
+    "d dvd fst x"
+    "d dvd snd x"
+    "d \<noteq> 0" .
+  then show ?thesis unfolding prod.collapse by (intro that[of d])
 qed
   
 lemma coprime_normalize_quot:
@@ -130,7 +135,13 @@
   define x' where "x' = normalize_quot x"
   obtain a b where [simp]: "x = (a, b)" by (cases x)
   from rel have "b \<noteq> 0" by simp
-  from normalize_quotE[OF this, of a] guess d .
+  from normalize_quotE[OF this, of a] obtain d
+    where
+      "a = fst (normalize_quot (a, b)) * d"
+      "b = snd (normalize_quot (a, b)) * d"
+      "d dvd a"
+      "d dvd b"
+      "d \<noteq> 0" .
   hence "a = fst x' * d" "b = snd x' * d" "d \<noteq> 0" "snd x' \<noteq> 0" by (simp_all add: x'_def)
   thus "fractrel (case x' of (a, b) \<Rightarrow> if b = 0 then (0, 1) else (a, b)) x"
     by (auto simp add: case_prod_unfold)
@@ -173,8 +184,20 @@
              snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) +
              snd (normalize_quot x) * fst (normalize_quot y))"
 proof -
-  from normalize_quotE'[OF assms(1)] guess d . note d = this
-  from normalize_quotE'[OF assms(2)] guess e . note e = this
+  from normalize_quotE'[OF assms(1)] obtain d
+    where d:
+      "fst x = fst (normalize_quot x) * d"
+      "snd x = snd (normalize_quot x) * d"
+      "d dvd fst x"
+      "d dvd snd x"
+      "d \<noteq> 0" .
+  from normalize_quotE'[OF assms(2)] obtain e
+    where e:
+      "fst y = fst (normalize_quot y) * e"
+      "snd y = snd (normalize_quot y) * e"
+      "e dvd fst y"
+      "e dvd snd y"
+      "e \<noteq> 0" .
   show ?thesis by (simp_all add: d e algebra_simps)
 qed
 
@@ -218,9 +241,16 @@
   from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
   with assms have "normalize b = b" "normalize d = d"
     by (auto intro: normalize_unit_factor_eqI)
-  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
+  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] obtain k
+    where
+      "c = fst (normalize_quot (c, b)) * k"
+      "b = snd (normalize_quot (c, b)) * k"
+      "k dvd c" "k dvd b" "k \<noteq> 0" .
   note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
-  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
+  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] obtain l
+    where "a = fst (normalize_quot (a, d)) * l"
+      "d = snd (normalize_quot (a, d)) * l"
+      "l dvd a" "l dvd d" "l \<noteq> 0" .
   note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
   from k l show "a * c * (f * h) = b * d * (e * g)"
     by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
@@ -241,8 +271,18 @@
              (fst (normalize_quot x) * fst (normalize_quot y),
               snd (normalize_quot x) * snd (normalize_quot y))"
 proof -
-  from normalize_quotE'[OF assms(1)] guess d . note d = this
-  from normalize_quotE'[OF assms(2)] guess e . note e = this
+  from normalize_quotE'[OF assms(1)] obtain d where d:
+    "fst x = fst (normalize_quot x) * d"
+    "snd x = snd (normalize_quot x) * d"
+    "d dvd fst x"
+    "d dvd snd x"
+    "d \<noteq> 0" .
+  from normalize_quotE'[OF assms(2)] obtain e where e:
+    "fst y = fst (normalize_quot y) * e"
+    "snd y = snd (normalize_quot y) * e"
+    "e dvd fst y"
+    "e dvd snd y"
+    "e \<noteq> 0" .
   show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff)
 qed
 
@@ -269,7 +309,11 @@
   defines "a' \<equiv> fst (normalize_quot (a, b))" and "b' \<equiv> snd (normalize_quot (a, b))"
   shows   "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')"
 proof (rule normalize_quotI)
-  from normalize_quotE[OF assms(2), of a] guess d . note d = this [folded assms(3,4)]
+  from normalize_quotE[OF assms(2), of a] obtain d where
+    "a = fst (normalize_quot (a, b)) * d"
+    "b = snd (normalize_quot (a, b)) * d"
+    "d dvd a" "d dvd b" "d \<noteq> 0" .
+  note d = this [folded assms(3,4)]
   show "b * (a' div unit_factor a') = a * (b' div unit_factor a')"
     using assms(1,2) d 
     by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
@@ -301,7 +345,10 @@
     by simp_all
   from \<open>is_unit v\<close> have "coprime v = top"
     by (simp add: fun_eq_iff is_unit_left_imp_coprime)
-  from normalize_quotE[OF False, of x] guess d .
+  from normalize_quotE[OF False, of x] obtain d where
+    "x = fst (normalize_quot (x, y)) * d"
+    "y = snd (normalize_quot (x, y)) * d"
+    "d dvd x" "d dvd y" "d \<noteq> 0" .
   note d = this[folded assms(2,3)]
   from assms have "coprime x' y'" "unit_factor y' = 1"
     by (simp_all add: coprime_normalize_quot)
@@ -318,7 +365,12 @@
   shows "normalize_quot (x, y div u) = (x' * u, y')"
 proof (cases "y = 0")
   case False
-  from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
+  from normalize_quotE[OF this, of x]
+  obtain d where d:
+    "x = fst (normalize_quot (x, y)) * d"
+    "y = snd (normalize_quot (x, y)) * d"
+    "d dvd x" "d dvd y" "d \<noteq> 0" .
+  note d = this[folded assms(2,3)]
   from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
   with d \<open>is_unit u\<close> show ?thesis
     by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -2661,11 +2661,14 @@
   shows "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) x"
 proof (cases a b rule: linorder_cases)
   case less
-  from poly_MVT[OF less, of p] guess x by (elim exE conjE)
+  from poly_MVT[OF less, of p] obtain x
+    where "a < x" "x < b" "poly p b - poly p a = (b - a) * poly (pderiv p) x"
+    by auto
   then show ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
 next
   case greater
-  from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
+  from poly_MVT[OF greater, of p] obtain x
+    where "b < x" "x < a" "poly p a - poly p b = (a - b) * poly (pderiv p) x" by auto
   then show ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
 qed (use assms in auto)
 
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -357,9 +357,15 @@
   shows   "p dvd q"
 proof -
   from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
-  from content_decompose_fract[of r] guess c r' . note r' = this
+  from content_decompose_fract[of r]
+  obtain c r' where r': "r = smult c (map_poly to_fract r')" "content r' = 1" .
   from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
-  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+  from fract_poly_smult_eqE[OF this] obtain a b
+    where ab:
+      "c = to_fract b / to_fract a"
+      "smult a q = smult b (p * r')"
+      "coprime a b"
+      "normalize a = a" .
   have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
   hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
   have "1 = gcd a (normalize b)" by (simp add: ab)
@@ -444,7 +450,7 @@
 proof safe
   assume p: "irreducible p"
 
-  from content_decompose[of p] guess p' . note p' = this
+  from content_decompose[of p] obtain p' where p': "p = smult (content p) p'" "content p' = 1" .
   hence "p = [:content p:] * p'" by simp
   from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
   moreover have "\<not>p' dvd 1"
@@ -470,12 +476,16 @@
    qed
  next
    fix q r assume qr: "fract_poly p = q * r"
-   from content_decompose_fract[of q] guess cg q' . note q = this
-   from content_decompose_fract[of r] guess cr r' . note r = this
+   from content_decompose_fract[of q]
+   obtain cg q' where q: "q = smult cg (map_poly to_fract q')" "content q' = 1" .
+   from content_decompose_fract[of r]
+   obtain cr r' where r: "r = smult cr (map_poly to_fract r')" "content r' = 1" .
    from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
    from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
      by (simp add: q r)
-   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+   from fract_poly_smult_eqE[OF this] obtain a b
+     where ab: "cr * cg = to_fract b / to_fract a"
+       "smult a p = smult b (q' * r')" "coprime a b" "normalize a = a" .
    hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
    with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
    then have "normalize b = gcd a b"
@@ -641,7 +651,12 @@
   finally have eq: "fract_poly p = smult c' (fract_poly e)" .
   also obtain b where b: "c' = to_fract b" "is_unit b"
   proof -
-    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
+    from fract_poly_smult_eqE[OF eq]
+    obtain a b where ab:
+      "c' = to_fract b / to_fract a"
+      "smult a p = smult b e"
+      "coprime a b"
+      "normalize a = a" .
     from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
     with assms content_e have "a = normalize b" by (simp add: ab(4))
     with ab have ab': "a = 1" "is_unit b"
@@ -673,7 +688,8 @@
   define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
   have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
     by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
-  then guess A by (elim exE conjE) note A = this
+  then obtain A where A: "\<forall>p. p \<in># A \<longrightarrow> prime_elem p" "\<Prod>\<^sub># A = normalize (primitive_part p)"
+    by blast
   have "normalize (prod_mset (A + B)) = normalize (prod_mset A * normalize (prod_mset B))"
     by simp
   also from assms have "normalize (prod_mset B) = normalize [:content p:]"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Number_Theory/Residue_Primitive_Roots.thy
--- a/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -755,7 +755,15 @@
   from assms have "n \<noteq> 0" by auto
   from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
     using assms Ex_other_prime_factor[of n 2] by auto
-  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
+  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this]
+  obtain p k n'
+    where p:
+      "p \<noteq> 2"
+      "prime p"
+      "p dvd n"
+      "\<not> p dvd n'"
+      "0 < k"
+      "n = p ^ k * n'" .
   from p have coprime: "coprime (p ^ k) n'"
     using p prime_imp_coprime by auto
   have "odd p"
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -32,10 +32,10 @@
 
 instance discrete :: (type) complete_space
 proof
-  fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
-  hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
+  fix X::"nat\<Rightarrow>'a discrete"
+  assume "Cauchy X"
+  then obtain n where "\<forall>m\<ge>n. X n = X m"
     by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
-  then guess n ..
   thus "convergent X"
     by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
        (simp add: dist_discrete_def)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -195,10 +195,20 @@
   have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
     (\<forall>S. open S \<and> x i \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" (is "\<forall>i. ?th i")
   proof
-    fix i from first_countable_basis_Int_stableE[of "x i"] guess A .
+    fix i from first_countable_basis_Int_stableE[of "x i"]
+    obtain A where
+      "countable A"
+      "\<And>C. C \<in> A \<Longrightarrow> (x)\<^sub>F i \<in> C"
+      "\<And>C. C \<in> A \<Longrightarrow> open C"
+      "\<And>S. open S \<Longrightarrow> (x)\<^sub>F i \<in> S \<Longrightarrow> \<exists>A\<in>A. A \<subseteq> S"
+      "\<And>C D. C \<in> A \<Longrightarrow> D \<in> A \<Longrightarrow> C \<inter> D \<in> A"
+      by auto
     thus "?th i" by (intro exI[where x=A]) simp
   qed
-  then guess A unfolding choice_iff .. note A = this
+  then obtain A
+    where A: "\<forall>i. countable (A i) \<and> Ball (A i) ((\<in>) ((x)\<^sub>F i)) \<and> Ball (A i) open \<and>
+      (\<forall>S. open S \<and> (x)\<^sub>F i \<in> S \<longrightarrow> (\<exists>a\<in>A i. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A i \<longrightarrow> b \<in> A i \<longrightarrow> a \<inter> b \<in> A i)"
+    by (auto simp: choice_iff)
   hence open_sub: "\<And>i S. i\<in>domain x \<Longrightarrow> open (S i) \<Longrightarrow> x i\<in>(S i) \<Longrightarrow> (\<exists>a\<in>A i. a\<subseteq>(S i))" by auto
   have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
   let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)"
@@ -492,7 +502,8 @@
       fix i assume "i \<in> d"
       from p[OF \<open>i \<in> d\<close>, THEN metric_LIMSEQ_D, OF \<open>0 < e\<close>]
       show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" .
-    qed then guess ni .. note ni = this
+    qed
+    then obtain ni where ni: "\<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e" ..
     define N where "N = max Nd (Max (ni ` d))"
     show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e"
     proof (safe intro!: exI[where x="N"])
@@ -586,10 +597,13 @@
   proof (rule bchoice, safe)
     fix i assume "i \<in> domain x"
     hence "open (a i)" "x i \<in> a i" using a by auto
-    from topological_basisE[OF basis_proj this] guess b' .
+    from topological_basisE[OF basis_proj this] obtain b'
+      where "b' \<in> basis_proj" "(x)\<^sub>F i \<in> b'" "b' \<subseteq> a i"
+      by blast
     thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto
   qed
-  then guess B .. note B = this
+  then obtain B where B: "\<forall>i\<in>domain x. (x)\<^sub>F i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> basis_proj"
+    by auto
   define B' where "B' = Pi' (domain x) (\<lambda>i. (B i)::'b set)"
   have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def)
   also note \<open>\<dots> \<subseteq> O'\<close>
@@ -1016,7 +1030,7 @@
   shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P"
 proof
   let ?P = "sigma (space (Pi\<^sub>F {I} M)) P"
-  from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] guess T ..
+  from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] obtain T where "bij_betw T I {0..<card I}" ..
   then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
     by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: \<open>finite I\<close>)
   have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>F {I} M))"
@@ -1080,7 +1094,9 @@
   shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
     sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
 proof -
-  from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
+  from open_countable_basisE[OF open_UNIV] obtain S::"'b set set"
+    where S: "S \<subseteq> (SOME B. countable B \<and> topological_basis B)" "UNIV = \<Union> S"
+    by auto
   show ?thesis
   proof (rule sigma_fprod_algebra_sigma_eq)
     show "finite I" by simp
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -423,7 +423,7 @@
     have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
     proof (rule sigma_sets_eqI)
       fix A assume "A \<in> (\<Union>i\<in>I j. E i)"
-      then guess i ..
+      then obtain i where "i \<in> I j" "A \<in> E i" ..
       then show "A \<in> sigma_sets (space M) (?E j)"
         by (auto intro!: sigma_sets.intros(2-) exI[of _ "{i}"] exI[of _ "\<lambda>i. A"])
     next
@@ -446,13 +446,14 @@
         and "\<forall>j\<in>K. A j \<in> ?E j"
       then have "\<forall>j\<in>K. \<exists>E' L. A j = (\<Inter>l\<in>L. E' l) \<and> finite L \<and> L \<noteq> {} \<and> L \<subseteq> I j \<and> (\<forall>l\<in>L. E' l \<in> E l)"
         by simp
-      from bchoice[OF this] guess E' ..
+      from bchoice[OF this] obtain E'
+        where "\<forall>x\<in>K. \<exists>L. A x = \<Inter> (E' x ` L) \<and> finite L \<and> L \<noteq> {} \<and> L \<subseteq> I x \<and> (\<forall>l\<in>L. E' x l \<in> E l)"
+        ..
       from bchoice[OF this] obtain L
         where A: "\<And>j. j\<in>K \<Longrightarrow> A j = (\<Inter>l\<in>L j. E' j l)"
         and L: "\<And>j. j\<in>K \<Longrightarrow> finite (L j)" "\<And>j. j\<in>K \<Longrightarrow> L j \<noteq> {}" "\<And>j. j\<in>K \<Longrightarrow> L j \<subseteq> I j"
         and E': "\<And>j l. j\<in>K \<Longrightarrow> l \<in> L j \<Longrightarrow> E' j l \<in> E l"
         by auto
-
       { fix k l j assume "k \<in> K" "j \<in> K" "l \<in> L j" "l \<in> L k"
         have "k = j"
         proof (rule ccontr)
@@ -747,8 +748,9 @@
     then show "?A \<subseteq> Pow (space M)" by auto
     show "Int_stable ?A"
     proof (rule Int_stableI)
-      fix a assume "a \<in> ?A" then guess n .. note a = this
-      fix b assume "b \<in> ?A" then guess m .. note b = this
+      fix a b assume "a \<in> ?A" "b \<in> ?A" then obtain n m
+        where a: "n \<in> UNIV" "a \<in> sigma_sets (space M) (\<Union> (A ` {..n}))"
+          and b: "m \<in> UNIV" "b \<in> sigma_sets (space M) (\<Union> (A ` {..m}))" by auto
       interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
         using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
       have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
@@ -1083,8 +1085,14 @@
       { fix i show "emeasure ?D (\<Pi>\<^sub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
     next
       fix E assume E: "E \<in> prod_algebra I M'"
-      from prod_algebraE[OF E] guess J Y . note J = this
-
+      from prod_algebraE[OF E] obtain J Y
+        where J:
+          "E = prod_emb I M' J (Pi\<^sub>E J Y)"
+          "finite J"
+          "J \<noteq> {} \<or> I = {}"
+          "J \<subseteq> I"
+          "\<And>i. i \<in> J \<Longrightarrow> Y i \<in> sets (M' i)"
+        by auto
       from E have "E \<in> sets ?P" by (auto simp: sets_PiM)
       then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
         by (simp add: emeasure_distr X)
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -273,7 +273,13 @@
 proof -
   interpret N: prob_space N by fact
   have "finite_measure N" by unfold_locales
-  from real_RN_deriv[OF this ac] guess D . note D = this
+  from real_RN_deriv[OF this ac] obtain D
+    where D:
+      "random_variable borel D"
+      "AE x in M. RN_deriv M N x = ennreal (D x)"
+      "AE x in N. 0 < D x"
+      "\<And>x. 0 \<le> D x"
+    by this auto
 
   have "N = density M (RN_deriv M N)"
     using ac by (rule density_RN_deriv[symmetric])
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Levy.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -422,7 +422,9 @@
       by (subst (asm) dist_complex_def, drule spec, erule mp, auto)
     hence "\<exists>N. \<forall>n \<ge> N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
         (CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by (simp add: eventually_sequentially)
-    then guess N ..
+    then obtain N
+      where "\<forall>n\<ge>N. cmod ((CLBINT t:{- d / 2..d / 2}. 1 - char (M n) t) -
+        (CLBINT t:{- d / 2..d / 2}. 1 - char M' t)) < d * \<epsilon> / 4" ..
     hence N: "\<And>n. n \<ge> N \<Longrightarrow> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
         (CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by auto
     { fix n
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -220,7 +220,8 @@
       using \<open>I \<noteq> {}\<close> by auto
   next
     fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
-    then guess x .. note x = this
+    then obtain x
+      where x: "k = q x + (INF t\<in>{x<..} \<inter> I. (q x - q t) / (x - t)) * (expectation X - x)" "x \<in> I" ..
     have "q x + ?F x * (expectation X  - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
       using prob_space by (simp add: X)
     also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
@@ -320,7 +321,8 @@
   assumes ae: "AE x in M. P x"
   obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
 proof -
-  from ae[THEN AE_E] guess N .
+  from ae[THEN AE_E] obtain N
+    where "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> events" by auto
   then show thesis
     by (intro that[of "space M - N"])
        (auto simp: prob_compl prob_space emeasure_eq_measure measure_nonneg)
@@ -365,7 +367,12 @@
   assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
   shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
 proof -
-  from ae[THEN AE_E_prob] guess S . note S = this
+  from ae[THEN AE_E_prob] obtain S
+    where S:
+      "S \<subseteq> {x \<in> space M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))}"
+      "S \<in> events"
+      "prob S = 1"
+    by auto
   then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
     by (auto simp: disjoint_family_on_def)
   from S have ae_S:
@@ -390,7 +397,12 @@
   assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))"
   shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))"
 proof -
-  from ae[THEN AE_E_prob] guess S . note S = this
+  from ae[THEN AE_E_prob] obtain S
+    where S:
+      "S \<subseteq> {x \<in> space M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. n \<in> I \<and> P n x))}"
+      "S \<in> events"
+      "prob S = 1"
+    by auto
   then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I"
     by (auto simp: disjoint_family_on_def)
   from S have ae_S:
@@ -692,7 +704,10 @@
   interpret T: sigma_finite_measure T by fact
   interpret ST: pair_sigma_finite S T ..
 
-  from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
+  from ST.sigma_finite_up_in_pair_measure_generator
+  obtain F :: "nat \<Rightarrow> ('b \<times> 'c) set"
+    where F: "range F \<subseteq> {A \<times> B |A B. A \<in> sets S \<and> B \<in> sets T} \<and> incseq F \<and>
+      \<Union> (range F) = space S \<times> space T \<and> (\<forall>i. emeasure (S \<Otimes>\<^sub>M T) (F i) \<noteq> \<infinity>)" ..
   let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
   let ?P = "S \<Otimes>\<^sub>M T"
   show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -49,7 +49,8 @@
 proof atomize_elim
   have "strict_mono ((+) m)" by (simp add: strict_mono_def)
   have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
-  from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
+  from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this]
+  obtain l r where "l \<in> S" "strict_mono r" "(f \<circ> (+) m \<circ> r) \<longlonglongrightarrow> l" by blast
   hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
     using strict_mono_o[OF \<open>strict_mono ((+) m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def)
   thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
@@ -59,7 +60,8 @@
 proof
   fix n and s :: "nat \<Rightarrow> nat"
   assume "strict_mono s"
-  from proj_in_KE[of n] guess n0 . note n0 = this
+  from proj_in_KE[of n] obtain n0 where n0: "\<And>m. n0 \<le> m \<Longrightarrow> (f m)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
+    by blast
   have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
   proof safe
     fix i assume "n0 \<le> i"
@@ -68,7 +70,9 @@
     with n0 show "((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0 "
       by auto
   qed
-  from compactE'[OF compact_projset this] guess ls rs .
+  then obtain ls rs
+    where "ls \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0" "strict_mono rs" "((\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<circ> rs) \<longlonglongrightarrow> ls"
+    by (rule compactE'[OF compact_projset])
   thus "\<exists>r'. strict_mono r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
 qed
 
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Probability/Stopping_Time.thy
--- a/src/HOL/Probability/Stopping_Time.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Stopping_Time.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -143,8 +143,9 @@
 lemma stopping_time_less_const:
   assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
 proof -
-  guess D :: "'t set" by (rule countable_dense_setE)
-  note D = this
+  obtain D :: "'t set"
+    where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+  using countable_dense_setE by auto
   show ?thesis
   proof cases
     assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"