# HG changeset patch
# User paulson
# Date 1672433978 0
# Node ID 6be3459fc4c1c26ca97071ab562ef778cf07e177
# Parent  72daee8a39cad989e75aee1835297e4bf3b9af07# Parent  ab08604729a2e1c75fca89525ddf10bd9326c8d2
merged

diff -r 72daee8a39ca -r 6be3459fc4c1 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Dec 30 21:27:57 2022 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Dec 30 20:59:38 2022 +0000
@@ -47,8 +47,7 @@
     (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
   apply (simp add: has_derivative_within)
   apply (subst tendsto_componentwise_iff)
-  apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib)
-  apply (simp add: algebra_simps)
+  apply (simp add: ball_conj_distrib  inner_diff_left inner_left_distrib flip: bounded_linear_componentwise_iff)
   done
 
 lemma has_derivative_at_withinI:
@@ -1181,9 +1180,7 @@
         (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
         \<Longrightarrow> DERIV g y :> inverse (f')"
   unfolding has_field_derivative_def
-  apply (rule has_derivative_inverse_basic)
-  apply (auto simp:  bounded_linear_mult_right)
-  done
+  by (rule has_derivative_inverse_basic) (auto simp: bounded_linear_mult_right)
 
 text \<open>Simply rewrite that based on the domain point x.\<close>
 
@@ -1205,20 +1202,13 @@
 lemma has_derivative_inverse_dieudonne:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "open S"
-    and "open (f ` S)"
-    and "continuous_on S f"
-    and "continuous_on (f ` S) g"
-    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
-    and "x \<in> S"
-    and "(f has_derivative f') (at x)"
-    and "bounded_linear g'"
-    and "g' \<circ> f' = id"
+    and fS: "open (f ` S)"
+    and A: "continuous_on S f" "continuous_on (f ` S) g" 
+           "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" "x \<in> S"
+    and B: "(f has_derivative f') (at x)" "bounded_linear g'" "g' \<circ> f' = id"
   shows "(g has_derivative g') (at (f x))"
-  apply (rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)])
-  using assms(3-6)
-  unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)]
-  apply auto
-  done
+  using A fS continuous_on_eq_continuous_at
+  by (intro has_derivative_inverse_basic_x[OF B _ _ fS]) force+
 
 text \<open>Here's the simplest way of not assuming much about g.\<close>
 
@@ -1229,19 +1219,14 @@
     and fx: "f x \<in> interior (f ` S)"
     and "continuous_on S f"
     and gf: "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
-    and "(f has_derivative f') (at x)"
-    and "bounded_linear g'"
-    and "g' \<circ> f' = id"
+    and B: "(f has_derivative f') (at x)" "bounded_linear g'" "g' \<circ> f' = id"
   shows "(g has_derivative g') (at (f x))"
 proof -
   have *: "\<And>y. y \<in> interior (f ` S) \<Longrightarrow> f (g y) = y"
     by (metis gf image_iff interior_subset subsetCE)
   show ?thesis
-    apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
-    apply (rule continuous_on_interior[OF _ fx])
-    apply (rule continuous_on_inv)
-    apply (simp_all add: assms *)
-    done
+    using assms * continuous_on_interior continuous_on_inv fx 
+    by (intro has_derivative_inverse_basic_x[OF B, where T = "interior (f`S)"]) blast+
 qed
 
 
@@ -1316,7 +1301,8 @@
         also have "\<dots> \<le> onorm g' * k"
           apply (rule mult_left_mono)
           using d1(2)[of u]
-          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"] d u onorm_pos_le[OF bling] apply (auto simp: algebra_simps)
+          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"] d u onorm_pos_le[OF bling] 
+           apply (auto simp: algebra_simps)
           done
         also have "\<dots> \<le> 1 / 2"
           unfolding k_def by auto
@@ -1498,17 +1484,16 @@
       fix x' y z :: 'a
       fix c :: real
       note lin = assms(2)[rule_format,OF \<open>x\<in>S\<close>,THEN has_derivative_bounded_linear]
-      show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
-        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
+      have "(\<lambda>n. f' n x (c *\<^sub>R x')) \<longlonglongrightarrow> c *\<^sub>R g' x x'"
         unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
-        apply (intro tendsto_intros tog')
-        done
-      show "g' x (y + z) = g' x y + g' x z"
-        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
+        by (intro tendsto_intros tog')
+      then show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
+        using LIMSEQ_unique tog' by blast
+      have "(\<lambda>n. f' n x (y + z)) \<longlonglongrightarrow> g' x y + g' x z"
         unfolding lin[THEN bounded_linear.linear, THEN linear_add]
-        apply (rule tendsto_add)
-        apply (rule tog')+
-        done
+        by (simp add: tendsto_add tog')
+      then show "g' x (y + z) = g' x y + g' x z"
+        using LIMSEQ_unique tog' by blast
       obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
         using nle \<open>x \<in> S\<close> unfolding eventually_sequentially by (fast intro: zero_less_one)
       have "bounded_linear (f' N x)"
@@ -1621,9 +1606,8 @@
       fix n x h
       assume n: "N \<le> n" and x: "x \<in> S"
       have *: "inverse (real (Suc n)) \<le> e"
-        apply (rule order_trans[OF _ N[THEN less_imp_le]])
-        using n apply (auto simp add: field_simps)
-        done
+        using n N
+        by (smt (verit, best) le_imp_inverse_le of_nat_0_less_iff of_nat_Suc of_nat_le_iff zero_less_Suc)
       show "norm (f' n x h - g' x h) \<le> e * norm h"
         by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
     qed
@@ -1822,12 +1806,19 @@
 lemma has_vector_derivative_cong_ev:
   assumes *: "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x = g x) (nhds x)" "f x = g x"
   shows "(f has_vector_derivative f') (at x within S) = (g has_vector_derivative f') (at x within S)"
+proof (cases "at x within S = bot")
+  case True
+  then show ?thesis   
+    by (simp add: has_derivative_def has_vector_derivative_def)
+next
+  case False
+  then show ?thesis
   unfolding has_vector_derivative_def has_derivative_def
   using *
-  apply (cases "at x within S \<noteq> bot")
   apply (intro refl conj_cong filterlim_cong)
   apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
   done
+qed
 
 lemma vector_derivative_cong_eq:
   assumes "eventually (\<lambda>x. x \<in> A \<longrightarrow> f x = g x) (nhds x)" "x = y" "A = B" "x \<in> A"
@@ -1900,18 +1891,15 @@
 lemma vector_derivative_scaleR_at [simp]:
     "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    \<Longrightarrow> vector_derivative (\<lambda>x. f x *\<^sub>R g x) (at a) = f a *\<^sub>R vector_derivative g (at a) + vector_derivative f (at a) *\<^sub>R g a"
-apply (rule vector_derivative_at)
-apply (rule has_vector_derivative_scaleR)
-apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
-done
+  apply (intro vector_derivative_at has_vector_derivative_scaleR)
+   apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
+  done
 
 lemma vector_derivative_within_cbox:
   assumes ab: "a < b" "x \<in> cbox a b"
   assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
   shows "vector_derivative f (at x within cbox a b) = f'"
-  by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
-            vector_derivative_works[THEN iffD1] differentiableI_vector)
-     fact
+  by (metis assms box_real(2) f islimpt_Icc trivial_limit_within vector_derivative_within)
 
 lemma vector_derivative_within_closed_interval:
   fixes f::"real \<Rightarrow> 'a::euclidean_space"
@@ -2328,8 +2316,8 @@
 lemma vector_derivative_chain_at_general:
   assumes "f differentiable at x" "g field_differentiable at (f x)"
   shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
-  apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
-  using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
+  using assms field_differentiable_derivI field_vector_diff_chain_at 
+      vector_derivative_at vector_derivative_works by blast
 
 lemma deriv_chain:
   "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
@@ -2409,10 +2397,14 @@
   by (auto intro!: DERIV_imp_deriv derivative_intros)
 
 lemma deriv_compose_linear:
-  "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
-apply (rule DERIV_imp_deriv)
-  unfolding DERIV_deriv_iff_field_differentiable [symmetric]
-  by (metis (full_types) DERIV_chain2 DERIV_cmult_Id mult.commute)
+  assumes "f field_differentiable at (c * z)"
+  shows "deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
+proof -
+  have "deriv (\<lambda>a. f (c * a)) z = deriv f (c * z) * c"
+    using assms by (simp add: DERIV_chain2 DERIV_deriv_iff_field_differentiable DERIV_imp_deriv)
+  then show ?thesis
+    by simp
+qed
 
 
 lemma nonzero_deriv_nonconstant:
@@ -2624,8 +2616,7 @@
             norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
               norm ((x', y') - (x, y)))
             < e'"
-    apply eventually_elim
-  proof safe
+  proof (eventually_elim, safe)
     fix x' y'
     have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
         norm (f x' y' - f x' y - fy x' y (y' - y)) +
@@ -2727,12 +2718,10 @@
   shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
     (if x \<in> S then f' x else g' x)) (at x within u)"
   unfolding has_vector_derivative_def assms
-  using x_in
-  apply (intro has_derivative_If_within_closures[where ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
-        THEN has_derivative_eq_rhs])
-  subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
-  subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
-  by (auto simp: assms)
+  using x_in f' g'
+  by (intro has_derivative_If_within_closures[where ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+        THEN has_derivative_eq_rhs]; force simp: assms has_vector_derivative_def)
+
 
 subsection\<^marker>\<open>tag important\<close>\<open>The Inverse Function Theorem\<close>
 
@@ -3100,17 +3089,12 @@
 lemma piecewise_differentiable_on_subset:
     "f piecewise_differentiable_on S \<Longrightarrow> T \<le> S \<Longrightarrow> f piecewise_differentiable_on T"
   using continuous_on_subset
-  unfolding piecewise_differentiable_on_def
-  apply safe
-  apply (blast elim: continuous_on_subset)
-  by (meson Diff_iff differentiable_within_subset subsetCE)
+  by (smt (verit) Diff_iff differentiable_within_subset in_mono piecewise_differentiable_on_def)
 
 lemma differentiable_on_imp_piecewise_differentiable:
   fixes a:: "'a::{linorder_topology,real_normed_vector}"
   shows "f differentiable_on {a..b} \<Longrightarrow> f piecewise_differentiable_on {a..b}"
-  apply (simp add: piecewise_differentiable_on_def differentiable_imp_continuous_on)
-  apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def)
-  done
+  using differentiable_imp_continuous_on differentiable_onD piecewise_differentiable_on_def by fastforce
 
 lemma differentiable_imp_piecewise_differentiable:
     "(\<And>x. x \<in> S \<Longrightarrow> f differentiable (at x within S))
diff -r 72daee8a39ca -r 6be3459fc4c1 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Dec 30 21:27:57 2022 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Dec 30 20:59:38 2022 +0000
@@ -658,12 +658,12 @@
   assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
   assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> P \<le> lfp F \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
   shows "emeasure (M s) {x\<in>space N. lfp F x} = lfp f s"
-proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and P="Measurable.pred N", symmetric])
+proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and f=F , symmetric])
   fix C assume "incseq C" "\<And>i. Measurable.pred N (C i)"
   then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (SUP i. C i) x}) = (SUP i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
-    unfolding SUP_apply[abs_def]
+    unfolding SUP_apply
     by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
-qed (auto simp add: iter le_fun_def SUP_apply[abs_def] intro!: meas cont)
+qed (auto simp add: iter le_fun_def SUP_apply intro!: meas cont)
 
 lemma emeasure_subadditive_finite:
   "finite I \<Longrightarrow> A ` I \<subseteq> sets M \<Longrightarrow> emeasure M (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. emeasure M (A i))"
@@ -2011,14 +2011,14 @@
     apply (rule Lim_emeasure_incseq) unfolding B_def by (auto simp add: SUP_subset_mono incseq_def)
   moreover have "emeasure M (B N) \<le> ennreal (\<Sum>n. measure M (A n))" for N
   proof -
-    have *: "(\<Sum>n\<in>{..<N}. measure M (A n)) \<le> (\<Sum>n. measure M (A n))"
+    have *: "(\<Sum>n<N. measure M (A n)) \<le> (\<Sum>n. measure M (A n))"
       using assms(3) measure_nonneg sum_le_suminf by blast
 
-    have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
+    have "emeasure M (B N) \<le> (\<Sum>n<N. emeasure M (A n))"
       unfolding B_def by (rule emeasure_subadditive_finite, auto)
-    also have "\<dots> = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
+    also have "\<dots> = (\<Sum>n<N. ennreal(measure M (A n)))"
       using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
-    also have "\<dots> = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
+    also have "\<dots> = ennreal (\<Sum>n<N. measure M (A n))"
       by auto
     also have "\<dots> \<le> ennreal (\<Sum>n. measure M (A n))"
       using * by (auto simp: ennreal_leI)
@@ -2067,12 +2067,8 @@
 proof -
   have "AE x in M. x \<notin> limsup A"
     using borel_cantelli_limsup1[OF assms] unfolding eventually_ae_filter by auto
-  moreover
-  {
-    fix x assume "x \<notin> limsup A"
-    then obtain N where "x \<notin> (\<Union>n\<in>{N..}. A n)" unfolding limsup_INF_SUP by blast
-    then have "eventually (\<lambda>n. x \<notin> A n) sequentially" using eventually_sequentially by auto
-  }
+  moreover have "\<forall>\<^sub>F n in sequentially. x \<notin> A n" if "x \<notin> limsup A" for x
+    using that  by (auto simp: limsup_INF_SUP eventually_sequentially)
   ultimately show ?thesis by auto
 qed
 
@@ -2288,12 +2284,11 @@
   assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
   assumes bound: "\<And>P. f P \<le> f (\<lambda>s. emeasure (M s) (space (M s)))"
   shows "emeasure (M s) {x\<in>space N. gfp F x} = gfp f s"
-proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and
-    P="Measurable.pred N", symmetric])
+proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and P="Measurable.pred N", symmetric])
   interpret finite_measure "M s" for s by fact
   fix C assume "decseq C" "\<And>i. Measurable.pred N (C i)"
   then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (INF i. C i) x}) = (INF i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
-    unfolding INF_apply[abs_def]
+    unfolding INF_apply
     by (subst INF_emeasure_decseq) (auto simp: antimono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
 next
   show "f x \<le> (\<lambda>s. emeasure (M s) {x \<in> space N. F top x})" for x
@@ -2821,20 +2816,8 @@
     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 show ?thesis
-    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
+  with assms show ?thesis
+    by (metis Int_subset_iff emeasure_restrict_space sets.Int_space_eq2 sets_restrict_space_iff space_restrict_space)
 qed
 
 text\<^marker>\<open>tag important\<close> \<open>
@@ -2876,11 +2859,7 @@
 end
 
 proposition le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
-  apply -
-  apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
-  subgoal for X
-    by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
-  done
+  by (metis emeasure_neq_0_sets le_fun_def le_measure_iff order_class.order_eq_iff sets_eq_imp_space_eq)
 
 definition\<^marker>\<open>tag important\<close> sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
 "sup_measure' A B =
@@ -2908,7 +2887,7 @@
       then have [measurable]: "\<And>i. X i \<in> sets A" and "disjoint_family X"
         by auto
       have disjoint: "disjoint_family (\<lambda>i. X i \<inter> Y)" "disjoint_family (\<lambda>i. X i - Y)" for Y
-        by (auto intro: disjoint_family_on_bisimulation [OF \<open>disjoint_family X\<close>, simplified])
+        using "1"(2) disjoint_family_subset by fastforce+
       have "(\<Sum>i. ?S (X i)) = (SUP Y\<in>sets A. \<Sum>i. ?d (X i) Y)"
       proof (rule ennreal_suminf_SUP_eq_directed)
         fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \<in> sets A" "b \<in> sets A"
@@ -2916,13 +2895,7 @@
         proof cases
           assume "emeasure A (X i) = top \<or> emeasure B (X i) = top"
           then show ?thesis
-          proof
-            assume "emeasure A (X i) = top" then show ?thesis
-              by (intro bexI[of _ "X i"]) auto
-          next
-            assume "emeasure B (X i) = top" then show ?thesis
-              by (intro bexI[of _ "{}"]) auto
-          qed
+            by force
         next
           assume finite: "\<not> (emeasure A (X i) = top \<or> emeasure B (X i) = top)"
           then have "\<exists>Y\<in>sets A. Y \<subseteq> X i \<and> (\<forall>C\<in>sets A. C \<subseteq> Y \<longrightarrow> B C \<le> A C) \<and> (\<forall>C\<in>sets A. C \<subseteq> X i \<longrightarrow> C \<inter> Y = {} \<longrightarrow> A C \<le> B C)"
@@ -2933,7 +2906,7 @@
             by auto
 
           show ?thesis
-          proof (intro bexI[of _ Y] ballI conjI)
+          proof (intro bexI ballI conjI)
             fix a assume [measurable]: "a \<in> sets A"
             have *: "(X i \<inter> a \<inter> Y \<union> (X i \<inter> a - Y)) = X i \<inter> a" "(X i - a) \<inter> Y \<union> (X i - a - Y) = X i \<inter> - a"
               for a Y by auto
@@ -2953,36 +2926,22 @@
           and C: "\<And>a. a \<in> sets A \<Longrightarrow> ?d (X i) a \<le> ?d (X i) (C i)" for i
           by metis
         have *: "X i \<inter> (\<Union>i. C i) = X i \<inter> C i" for i
-        proof safe
-          fix x j assume "x \<in> X i" "x \<in> C j"
-          moreover have "i = j \<or> X i \<inter> X j = {}"
-            using \<open>disjoint_family X\<close> by (auto simp: disjoint_family_on_def)
-          ultimately show "x \<in> C i"
-            using \<open>C i \<subseteq> X i\<close> \<open>C j \<subseteq> X j\<close> by auto
-        qed auto
-        have **: "X i \<inter> - (\<Union>i. C i) = X i \<inter> - C i" for i
-        proof safe
-          fix x j assume "x \<in> X i" "x \<notin> C i" "x \<in> C j"
-          moreover have "i = j \<or> X i \<inter> X j = {}"
-            using \<open>disjoint_family X\<close> by (auto simp: disjoint_family_on_def)
-          ultimately show False
-            using \<open>C i \<subseteq> X i\<close> \<open>C j \<subseteq> X j\<close> by auto
-        qed auto
-        show "\<exists>c\<in>sets A. \<forall>i\<in>J. ?d (X i) a \<le> ?d (X i) c \<and> ?d (X i) b \<le> ?d (X i) c"
-          apply (intro bexI[of _ "\<Union>i. C i"])
-          unfolding * **
-          apply (intro C ballI conjI)
-          apply auto
-          done
+          using \<open>disjoint_family X\<close> \<open>\<And>i. C i \<subseteq> X i\<close>
+          by (simp add: disjoint_family_on_def disjoint_iff_not_equal set_eq_iff) (metis subsetD)
+        then have **: "X i \<inter> - (\<Union>i. C i) = X i \<inter> - C i" for i by blast
+        moreover have "(\<Union>i. C i) \<in> sets A"
+          by fastforce
+        ultimately show "\<exists>c\<in>sets A. \<forall>i\<in>J. ?d (X i) a \<le> ?d (X i) c \<and> ?d (X i) b \<le> ?d (X i) c"
+          by (metis "*" C \<open>a \<in> sets A\<close> \<open>b \<in> sets A\<close>)
       qed
       also have "\<dots> = ?S (\<Union>i. X i)"
-        apply (simp only: UN_extend_simps(4))
-        apply (rule arg_cong [of _ _ Sup])
-        apply (rule image_cong)
-         apply (fact refl)
-        using disjoint
-        apply (auto simp add: suminf_add [symmetric] Diff_eq [symmetric] image_subset_iff suminf_emeasure simp del: UN_simps)
-        done
+      proof -
+        have "\<And>Y. Y \<in> sets A \<Longrightarrow> (\<Sum>i. emeasure A (X i \<inter> Y) + emeasure B (X i \<inter> -Y)) 
+                              = emeasure A (\<Union>i. X i \<inter> Y) + emeasure B (\<Union>i. X i \<inter> -Y)"
+          using disjoint
+          by (auto simp flip: suminf_add Diff_eq simp add: image_subset_iff suminf_emeasure)
+        then show ?thesis by force
+      qed
       finally show "(\<Sum>i. ?S (X i)) = ?S (\<Union>i. X i)" .
     qed
   qed (auto dest: sets.sets_into_space simp: positive_def intro!: SUP_const)
@@ -3268,10 +3227,7 @@
         show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (\<Union>(F ` UNIV))"
         proof cases
           assume "i \<noteq> {}" with i ** show ?thesis
-            apply (intro suminf_emeasure \<open>disjoint_family F\<close>)
-            apply (subst sets_sup_measure_F[OF _ _ sets_eq])
-            apply auto
-            done
+            by (smt (verit, best) "1"(2) Measure_Space.sets_sup_measure_F assms(1) mem_Collect_eq subset_eq suminf_cong suminf_emeasure)
         qed simp
       qed
     qed
@@ -3537,33 +3493,27 @@
 
 subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Supremum of a set of \<open>\<sigma>\<close>-algebras\<close>
 
-lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
-  unfolding Sup_measure_def
-  apply (intro Sup_lexord[where P="\<lambda>x. space x = _"])
-  apply (subst space_Sup_measure'2)
-  apply auto []
-  apply (subst space_measure_of[OF UN_space_closed])
-  apply auto
-  done
+lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)" (is "?L=?R")
+proof
+  show "?L \<subseteq> ?R"
+    using Sup_lexord[where P="\<lambda>x. space x = _"]
+    apply (clarsimp simp: Sup_measure_def)
+    by (smt (verit) Sup_lexord_def UN_E mem_Collect_eq space_Sup_measure'2 space_measure_of_conv)
+qed (use Sup_upper le_measureD1 in fastforce)
+
 
 lemma sets_Sup_eq:
   assumes *: "\<And>m. m \<in> M \<Longrightarrow> space m = X" and "M \<noteq> {}"
   shows "sets (Sup M) = sigma_sets X (\<Union>x\<in>M. sets x)"
   unfolding Sup_measure_def
-  apply (rule Sup_lexord1)
-  apply fact
-  apply (simp add: assms)
+proof (rule Sup_lexord1 [OF \<open>M \<noteq> {}\<close>])
+  show "sets (Sup_lexord sets Sup_measure' (\<lambda>U. sigma (\<Union> (space ` U)) (\<Union> (sets ` U))) M)
+      = sigma_sets X (\<Union> (sets ` M))"
   apply (rule Sup_lexord)
-  subgoal premises that for a S
-    unfolding that(3) that(2)[symmetric]
-    using that(1)
-    apply (subst sets_Sup_measure'2)
-    apply (intro arg_cong2[where f=sigma_sets])
-    apply (auto simp: *)
-    done
-  apply (subst sets_measure_of[OF UN_space_closed])
-  apply (simp add:  assms)
-  done
+  apply (metis (mono_tags, lifting) "*" empty_iff mem_Collect_eq sets.sigma_sets_eq sets_Sup_measure')
+  by (metis "*" SUP_eq_const UN_space_closed assms(2) sets_measure_of)
+qed (use * in blast)
+
 
 lemma in_sets_Sup: "(\<And>m. m \<in> M \<Longrightarrow> space m = X) \<Longrightarrow> m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup M)"
   by (subst sets_Sup_eq[where X=X]) auto
@@ -3583,16 +3533,11 @@
 qed
 
 lemma sets_SUP_cong:
-  assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i\<in>I. M i) = sets (SUP i\<in>I. N i)"
+  assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" 
+  shows "sets (SUP i\<in>I. M i) = sets (SUP i\<in>I. N i)"
   unfolding Sup_measure_def
   using eq eq[THEN sets_eq_imp_space_eq]
-  apply (intro Sup_lexord_rel[where R="\<lambda>x y. sets x = sets y"])
-  apply simp
-  apply simp
-  apply (simp add: sets_Sup_measure'2)
-  apply (intro arg_cong2[where f="\<lambda>x y. sets (sigma x y)"])
-  apply auto
-  done
+  by (intro Sup_lexord_rel[where R="\<lambda>x y. sets x = sets y"], simp_all add: sets_Sup_measure'2)
 
 lemma sets_Sup_in_sets:
   assumes "M \<noteq> {}"
@@ -3626,18 +3571,15 @@
   from M obtain m where "m \<in> M" by auto
   have space_eq: "\<And>n. n \<in> M \<Longrightarrow> space n = space m"
     by (intro const_space \<open>m \<in> M\<close>)
+  have eq: "sets (sigma (\<Union> (space ` M)) (\<Union> (sets ` M))) = sets (Sup M)"
+    by (metis M SUP_eq_const UN_space_closed sets_Sup_eq sets_measure_of space_eq)
   have "f \<in> measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m))"
   proof (rule measurable_measure_of)
     show "f \<in> space N \<rightarrow> \<Union>(space ` M)"
       using measurable_space[OF f] M by auto
   qed (auto intro: measurable_sets f dest: sets.sets_into_space)
   also have "measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)) = measurable N (Sup M)"
-    apply (intro measurable_cong_sets refl)
-    apply (subst sets_Sup_eq[OF space_eq M])
-    apply simp
-    apply (subst sets_measure_of[OF UN_space_closed])
-    apply (simp add: space_eq M)
-    done
+    using eq measurable_cong_sets by blast
   finally show ?thesis .
 qed
 
@@ -3652,15 +3594,11 @@
 proof -
   { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
     then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
-     by induction (auto intro: sigma_sets.intros(2-)) }
+      by induction (auto intro: sigma_sets.intros(2-)) }
+  then have "sigma_sets \<Omega> (\<Union> (sigma_sets \<Omega> ` M)) = sigma_sets \<Omega> (\<Union> M)"
+    by (smt (verit, best) UN_iff Union_iff sigma_sets.Basic sigma_sets_eqI)
   then show "sets (SUP m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
-    apply (subst sets_Sup_eq[where X="\<Omega>"])
-    apply (auto simp add: M) []
-    apply auto []
-    apply (simp add: space_measure_of_conv M Union_least)
-    apply (rule sigma_sets_eqI)
-    apply auto
-    done
+    by (subst sets_Sup_eq) (fastforce simp add: M Union_least)+
 qed
 
 lemma Sup_sigma:
@@ -3672,9 +3610,8 @@
   show "sigma \<Omega> (\<Union>M) \<le> (SUP m\<in>M. sigma \<Omega> m)"
   proof (intro less_eq_measure.intros(3))
     show "space (sigma \<Omega> (\<Union>M)) = space (SUP m\<in>M. sigma \<Omega> m)"
-      "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m\<in>M. sigma \<Omega> m)"
-      using sets_Sup_sigma[OF assms] sets_Sup_sigma[OF assms, THEN sets_eq_imp_space_eq]
-      by auto
+         "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m\<in>M. sigma \<Omega> m)"
+      by (auto simp add: M sets_Sup_sigma sets_eq_imp_space_eq)
   qed (simp add: emeasure_sigma le_fun_def)
   fix m assume "m \<in> M" then show "sigma \<Omega> m \<le> sigma \<Omega> (\<Union>M)"
     by (subst sigma_le_iff) (auto simp add: M *)
@@ -3687,29 +3624,17 @@
 lemma sets_vimage_Sup_eq:
   assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
   shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m \<in> M. vimage_algebra X f m)"
-  (is "?IS = ?SI")
+  (is "?L = ?R")
 proof
-  show "?IS \<subseteq> ?SI"
-    apply (intro sets_image_in_sets measurable_Sup2)
-    apply (simp add: space_Sup_eq_UN *)
-    apply (simp add: *)
-    apply (intro measurable_Sup1)
-    apply (rule imageI)
-    apply assumption
-    apply (rule measurable_vimage_algebra1)
-    apply (auto simp: *)
-    done
-  show "?SI \<subseteq> ?IS"
+  have "\<And>m. m \<in> M \<Longrightarrow> f \<in> Sup (vimage_algebra X f ` M) \<rightarrow>\<^sub>M m"
+    using assms
+    by (smt (verit, del_insts) Pi_iff imageE image_eqI measurable_Sup1
+            measurable_vimage_algebra1 space_vimage_algebra)
+  then show "?L \<subseteq> ?R"
+     by (intro sets_image_in_sets measurable_Sup2) (simp_all add: space_Sup_eq_UN *)
+  show "?R \<subseteq> ?L"
     apply (intro sets_Sup_in_sets)
-    apply (auto simp: *) []
-    apply (auto simp: *) []
-    apply (elim imageE)
-    apply simp
-    apply (rule sets_image_in_sets)
-    apply simp
-    apply (simp add: measurable_def)
-    apply (simp add: * space_Sup_eq_UN sets_vimage_algebra2)
-    apply (auto intro: in_sets_Sup[OF *(3)])
+    apply (force simp add: * space_Sup_eq_UN sets_vimage_algebra2 intro: in_sets_Sup)+
     done
 qed
 
@@ -3743,13 +3668,8 @@
 
 lemma measurable_iff_sets:
   "f \<in> measurable M N \<longleftrightarrow> (f \<in> space M \<rightarrow> space N \<and> sets (vimage_algebra (space M) f N) \<subseteq> sets M)"
-proof -
-  have *: "{f -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)"
-    by auto
-  show ?thesis
     unfolding measurable_def
-    by (auto simp add: vimage_algebra_def sigma_le_sets[OF *])
-qed
+    by (smt (verit, ccfv_threshold) mem_Collect_eq sets_vimage_algebra sigma_sets_le_sets_iff subset_eq)
 
 lemma sets_vimage_algebra_space: "X \<in> sets (vimage_algebra X f M)"
   using sets.top[of "vimage_algebra X f M"] by simp
@@ -3764,7 +3684,7 @@
   moreover assume "\<forall>y\<in>sets N. f -` y \<inter> space M \<in> sets M" note this[THEN bspec, of A]
   ultimately show "f -` A \<inter> space M' \<in> sets M'"
     using assms by auto
-qed (insert N M, auto)
+qed (use N M in auto)
 
 lemma measurable_Sup_measurable:
   assumes f: "f \<in> space N \<rightarrow> A"
@@ -3780,7 +3700,7 @@
   shows "sigma_sets \<Omega>' a \<subseteq> M"
 proof
   show "x \<in> M" if x: "x \<in> sigma_sets \<Omega>' a" for x
-    using x by (induct rule: sigma_sets.induct) (insert a, auto)
+    using x by (induct rule: sigma_sets.induct) (use a in auto)
 qed
 
 lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i\<in>I. M i)"
@@ -3802,20 +3722,13 @@
   "sets M \<le> sets N \<Longrightarrow> sets (vimage_algebra X f M) \<subseteq> sets (vimage_algebra X f N)"
   using sets.top[of "sigma X {f -` A \<inter> X |A. A \<in> sets N}"]
   unfolding vimage_algebra_def
-  apply (subst (asm) space_measure_of)
-  apply auto []
-  apply (subst sigma_le_sets)
-  apply auto
-  done
+  by (smt (verit, del_insts) space_measure_of sigma_le_sets Pow_iff inf_le2 mem_Collect_eq subset_eq)
 
 lemma mono_restrict_space: "sets M \<le> sets N \<Longrightarrow> sets (restrict_space M X) \<subseteq> sets (restrict_space N X)"
   unfolding sets_restrict_space by (rule image_mono)
 
 lemma sets_eq_bot: "sets M = {{}} \<longleftrightarrow> M = bot"
-  apply safe
-  apply (intro measure_eqI)
-  apply auto
-  done
+  by (metis measure_eqI emeasure_empty sets_bot singletonD)
 
 lemma sets_eq_bot2: "{{}} = sets M \<longleftrightarrow> M = bot"
   using sets_eq_bot[of M] by blast
@@ -3825,10 +3738,8 @@
   "countable {x. measure M {x} \<noteq> 0}"
 proof cases
   assume "measure M (space M) = 0"
-  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
-    by auto
-  then show ?thesis
-    by simp
+  then show ?thesis 
+    by (metis (mono_tags, lifting) bounded_measure measure_le_0_iff Collect_empty_eq countable_empty) 
 next
   let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
   assume "?M \<noteq> 0"
@@ -3840,7 +3751,7 @@
     fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
     then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
       by (metis infinite_arbitrarily_large)
-    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
+    then have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
       by auto
     { fix x assume "x \<in> X"
       from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
diff -r 72daee8a39ca -r 6be3459fc4c1 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Dec 30 21:27:57 2022 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Dec 30 20:59:38 2022 +0000
@@ -1586,7 +1586,7 @@
 qed
 
 lemma
-  shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
+  shows space_measure_of_conv [simp]: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
   and sets_measure_of_conv:
   "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
   and emeasure_measure_of_conv: