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