diff -r 04f4b6e55620 -r 8281047b896d src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Mon Apr 14 20:42:03 2025 +0200
+++ b/src/HOL/Analysis/Measurable.thy	Tue Apr 15 15:30:21 2025 +0100
@@ -278,21 +278,12 @@
   unfolding measurable_count_space_eq2_countable
 proof safe
   fix n
-
-  { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
-    then have "infinite {i. P i x}"
-      unfolding infinite_nat_iff_unbounded_le by auto
-    then have "Max {i. P i x} = the None"
-      by (rule Max.infinite) }
-  note 1 = this
-
-  { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
-    then have "finite {i. P i x}"
-      by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
-    with \<open>P i x\<close> have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}"
-      using Max_in[of "{i. P i x}"] by auto }
-  note 2 = this
-
+  have 1: "Max {i. P i x} = the None" if "\<forall>i. \<exists>n\<ge>i. P n x" for x
+    by (simp add: Max.infinite infinite_nat_iff_unbounded_le that)
+  have 2: "finite {i. P i x}" if "\<forall>n\<ge>j. \<not> P n x" for j x
+    by (metis bounded_nat_set_is_finite leI mem_Collect_eq that)
+  have 3: "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" if "P i x" "\<forall>n\<ge>j. \<not> P n x" for x i j
+      using that 2 Max_in[of "{i. P i x}"] by auto 
   have "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Max {i. P i x} = n}"
     by auto
   also have "\<dots> =
@@ -300,7 +291,7 @@
       if (\<exists>i. P i x) then P n x \<and> (\<forall>i>n. \<not> P i x)
       else Max {} = n}"
     by (intro arg_cong[where f=Collect] ext conj_cong)
-       (auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI)
+       (auto simp add: 1 2 3 not_le[symmetric] intro!: Max_eqI)
   also have "\<dots> \<in> sets M"
     by measurable
   finally show "(\<lambda>x. Max {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
@@ -313,20 +304,12 @@
   unfolding measurable_count_space_eq2_countable
 proof safe
   fix n
-
-  { fix x assume "\<forall>i. \<exists>n\<ge>i. P n x"
-    then have "infinite {i. P i x}"
-      unfolding infinite_nat_iff_unbounded_le by auto
-    then have "Min {i. P i x} = the None"
-      by (rule Min.infinite) }
-  note 1 = this
-
-  { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x"
-    then have "finite {i. P i x}"
-      by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded)
-    with \<open>P i x\<close> have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}"
-      using Min_in[of "{i. P i x}"] by auto }
-  note 2 = this
+  have 1: "Min {i. P i x} = the None" if "\<forall>i. \<exists>n\<ge>i. P n x" for x
+    by (simp add: Min.infinite infinite_nat_iff_unbounded_le that)
+  have 2: "finite {i. P i x}" if "\<forall>n\<ge>j. \<not> P n x" for j x
+    by (metis bounded_nat_set_is_finite leI mem_Collect_eq that)
+  have 3: "P (Min {i. P i x}) x" "i \<ge> Min {i. P i x}" if "P i x" "\<forall>n\<ge>j. \<not> P n x" for x i j
+      using that 2 Min_in[of "{i. P i x}"] by auto 
 
   have "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M = {x\<in>space M. Min {i. P i x} = n}"
     by auto
@@ -335,7 +318,7 @@
       if (\<exists>i. P i x) then P n x \<and> (\<forall>i<n. \<not> P i x)
       else Min {} = n}"
     by (intro arg_cong[where f=Collect] ext conj_cong)
-       (auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI)
+       (auto simp add: 1 2 3 not_le[symmetric] intro!: Min_eqI)
   also have "\<dots> \<in> sets M"
     by measurable
   finally show "(\<lambda>x. Min {i. P i x}) -` {n} \<inter> space M \<in> sets M" .
@@ -365,7 +348,7 @@
   next
     case (Suc i)
     then have "(\<lambda>x. card (S x)) -` {n} \<inter> space M =
-      (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
+               (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
       unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
     also have "\<dots> \<in> sets M"
       by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
@@ -398,7 +381,7 @@
 proof (safe intro!: UNIV_I)
   fix a
   have "(\<lambda>x. SUP i\<in>I. F i x) -` {a} \<inter> space M =
-    {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
+        {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
     unfolding SUP_le_iff[symmetric] by auto
   also have "\<dots> \<in> sets M"
     by measurable
@@ -414,7 +397,7 @@
 proof (safe intro!: UNIV_I)
   fix a
   have "(\<lambda>x. INF i\<in>I. F i x) -` {a} \<inter> space M =
-    {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
+        {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
     unfolding le_INF_iff[symmetric] by auto
   also have "\<dots> \<in> sets M"
     by measurable
@@ -428,8 +411,8 @@
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "lfp F \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from \<open>P M\<close> have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)"
-      by (induct i arbitrary: M) (auto intro!: *) }
+  have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)" for i
+    using \<open>P M\<close> by (induct i arbitrary: M) (auto intro!: *) 
   then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
@@ -451,8 +434,8 @@
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)"
   shows "gfp F \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from \<open>P M\<close> have "((F ^^ i) top) \<in> measurable M (count_space UNIV)"
-      by (induct i arbitrary: M) (auto intro!: *) }
+  have "((F ^^ i) top) \<in> measurable M (count_space UNIV)" for i
+    using \<open>P M\<close> by (induct i arbitrary: M) (auto intro!: *) 
   then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
@@ -474,8 +457,8 @@
   assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   shows "lfp F s \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
-      by (induct i arbitrary: M s) (auto intro!: *) }
+  have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" for i
+    using \<open>P M s\<close> by (induct i arbitrary: M s) (auto intro!: *) 
   then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
@@ -490,8 +473,8 @@
   assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)"
   shows "gfp F s \<in> measurable M (count_space UNIV)"
 proof -
-  { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
-      by (induct i arbitrary: M s) (auto intro!: *) }
+  have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" for i
+    using \<open>P M s\<close> by (induct i arbitrary: M s) (auto intro!: *) 
   then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
     by measurable
   also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
@@ -511,35 +494,34 @@
   fix a :: enat
   have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}"
     by auto
-  { fix i :: nat
-    from \<open>R f\<close> have "Measurable.pred M (\<lambda>x. f x = enat i)"
-    proof (induction i arbitrary: f)
-      case 0
-      from *[OF this] obtain g h i P
-        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and
-          [measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
-        by auto
-      have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)"
-        by measurable
-      also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)"
-        by (auto simp: f zero_enat_def[symmetric])
-      finally show ?case .
-    next
-      case (Suc n)
-      from *[OF Suc.prems] obtain g h i P
-        where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and
-          M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
-        by auto
-      have "(\<lambda>x. f x = enat (Suc n)) =
+  have "Measurable.pred M (\<lambda>x. f x = enat i)" for i
+    using \<open>R f\<close>
+  proof (induction i arbitrary: f)
+    case 0
+    from *[OF this] obtain g h i P
+      where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and
+        [measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
+      by auto
+    have "Measurable.pred M (\<lambda>x. P x \<and> h x = 0)"
+      by measurable
+    also have "(\<lambda>x. P x \<and> h x = 0) = (\<lambda>x. f x = enat 0)"
+      by (auto simp: f zero_enat_def[symmetric])
+    finally show ?case .
+  next
+    case (Suc n)
+    from *[OF Suc.prems] obtain g h i P
+      where f: "f = (\<lambda>x. if P x then h x else eSuc (g (i x)))" and "R g" and
+        M[measurable]: "Measurable.pred M P" "i \<in> measurable M M" "h \<in> measurable M (count_space UNIV)"
+      by auto
+    have "(\<lambda>x. f x = enat (Suc n)) =
         (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))"
-        by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
-      also have "Measurable.pred M \<dots>"
-        by (intro pred_intros_logic measurable_compose[OF M(2)] Suc \<open>R g\<close>) measurable
-      finally show ?case .
-    qed
-    then have "f -` {enat i} \<inter> space M \<in> sets M"
-      by (simp add: pred_def Int_def conj_commute) }
-  note fin = this
+      by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
+    also have "Measurable.pred M \<dots>"
+      by (intro pred_intros_logic measurable_compose[OF M(2)] Suc \<open>R g\<close>) measurable
+    finally show ?case .
+  qed
+  then have fin: "f -` {enat i} \<inter> space M \<in> sets M" for i
+    by (simp add: pred_def Int_def conj_commute) 
   show "f -` {a} \<inter> space M \<in> sets M"
   proof (cases a)
     case infinity
@@ -562,16 +544,12 @@
   fix X
   define f where "f x = (THE i. P i x)" for x
   define undef where "undef = (THE i::'a. False)"
-  { fix i x assume "x \<in> space M" "P i x" then have "f x = i"
-      unfolding f_def using unique by auto }
-  note f_eq = this
-  { fix x assume "x \<in> space M" "\<forall>i\<in>I. \<not> P i x"
-    then have "\<And>i. \<not> P i x"
-      using I(2)[of x] by auto
-    then have "f x = undef"
-      by (auto simp: undef_def f_def) }
-  then have "f -` X \<inter> space M = (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union>
-     (if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})"
+  have f_eq: "f x = i" if "x \<in> space M" "P i x" for i x
+    unfolding f_def using unique that by auto
+  have "f x = undef" if "x \<in> space M" "\<forall>i\<in>I. \<not> P i x" for x
+    using that I f_def undef_def by moura
+  then have "f -` X \<inter> space M = 
+             (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union> (if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})"
     by (auto dest: f_eq)
   also have "\<dots> \<in> sets M"
     by (auto intro!: sets.Diff sets.countable_UN')
@@ -628,7 +606,7 @@
   have P_f: "{x \<in> space M. P (f x)} \<in> sets M"
     unfolding pred_def[symmetric] by (rule measurable_compose[OF f]) simp
   have "pred (restrict_space M {x\<in>space M. P (f x)}) (\<lambda>x. Q (f x) x)"
-  proof (rule measurable_compose_countable'[where g=f, OF _ _ P])
+  proof (rule measurable_compose_countable'[OF _ _ P])
     show "f \<in> restrict_space M {x\<in>space M. P (f x)} \<rightarrow>\<^sub>M count_space {i. P i}"
       by (rule measurable_count_space_extend[OF subset_UNIV])
          (auto simp: space_restrict_space intro!: measurable_restrict_space1 f)