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")