# HG changeset patch
# User paulson
# Date 1672137514 0
# Node ID 7fd705b107f2b9c7cb87192b68d138f62c225d5f
# Parent  9e5a27486ca23defab1a0d112cedc2d30dec078c# Parent  50672d2d78db24e5f59239f3befe2d40dc140770
merged

diff -r 9e5a27486ca2 -r 7fd705b107f2 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Dec 27 10:38:34 2022 +0000
@@ -83,11 +83,8 @@
 
 lemma retraction_openin_vimage_iff:
   "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
-  if retraction: "retraction S T r" and "U \<subseteq> T"
-  using retraction apply (rule retractionE)
-  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
-  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
-  done
+  if "retraction S T r" and "U \<subseteq> T"
+  by (simp add: retraction_openin_vimage_iff that)
 
 lemma retract_of_locally_compact:
     fixes S :: "'a :: {heine_borel,real_normed_vector} set"
@@ -251,7 +248,7 @@
   then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
     using insert by auto
   with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
-    using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
+    by (metis insert_iff order.trans)+
 qed auto
 
 lemma kuhn_labelling_lemma:
@@ -1081,7 +1078,7 @@
       qed }
     with ks_f' eq \<open>a \<noteq> b.enum 0\<close> \<open>n \<noteq> 0\<close> show ?thesis
       apply (intro ex1I[of _ "b.enum ` {.. n}"])
-      apply auto []
+      apply fastforce
       apply metis
       done
   next
@@ -1111,16 +1108,11 @@
     have "{i} \<subseteq> {..n}"
       using i by auto
     { fix j assume "j \<le> n"
-      moreover have "j < i \<or> i = j \<or> i < j" by arith
-      moreover note i
-      ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
-        apply (simp only: fun_eq_iff enum_def b.enum_def flip: image_comp)
+      with i Suc_i' have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
+        unfolding fun_eq_iff enum_def b.enum_def image_comp [symmetric]
         apply (cases \<open>i = j\<close>)
-         apply simp
-         apply (metis Suc_i' \<open>i \<le> n\<close> imageI in_upd_image lessI lessThan_iff lessThan_subset_iff less_irrefl_nat transpose_apply_second transpose_commute)
-        apply (subst transpose_image_eq)
-         apply (auto simp add: i'_def)
-        done
+         apply (metis imageI in_upd_image lessI lessThan_iff lessThan_subset_iff order_less_le transpose_apply_first)
+        by (metis lessThan_iff linorder_not_less not_less_eq_eq order_less_le transpose_image_eq)
       }
     note enum_eq_benum = this
     then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
@@ -1295,7 +1287,7 @@
 
 lemma reduced_labelling_unique:
   "r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
- unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
+  by (metis linorder_less_linear linorder_not_le reduced_labelling)
 
 lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
   using reduced_labelling[of n x] by auto
@@ -1369,7 +1361,7 @@
       by (auto simp: out_eq_p)
     moreover
     { fix x assume "x \<in> s"
-      with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
+      with lab_1[rule_format, of n x] all_eq_p s_le_p[of x] 
       have "?rl x \<le> n"
         by (auto intro!: reduced_labelling_nonzero)
       then have "?rl x = reduced n (lab x)"
@@ -1532,34 +1524,9 @@
              (\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
              (\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
              (\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
-proof -
-  have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
-    by auto
-  have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
-    by auto
-  show ?thesis
-    unfolding and_forall_thm
-    apply (subst choice_iff[symmetric])+
-    apply rule
-    apply rule
-  proof -
-    fix x x'
-    let ?R = "\<lambda>y::nat.
-      (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
-      (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
-      (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
-      (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
-    have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
-      using assms(2)[rule_format,of "f x" x'] that
-      apply (drule_tac assms(1)[rule_format])
-      apply auto
-      done
-    then have "?R 0 \<or> ?R 1"
-      by auto
-    then show "\<exists>y\<le>1. ?R y"
-      by auto
-  qed
-qed
+  unfolding all_conj_distrib [symmetric] 
+  apply (subst choice_iff[symmetric])+
+  by (metis assms bot_nat_0.extremum nle_le zero_neq_one)
 
 subsection \<open>Brouwer's fixed point theorem\<close>
 
@@ -1785,11 +1752,7 @@
     using b' unfolding bij_betw_def by auto
   define r' ::'a where "r' = (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)"
   have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
-    apply (rule order_trans)
-    apply (rule rs(1)[OF b'_im,THEN conjunct2])
-    using q(1)[rule_format,OF b'_im]
-    apply (auto simp: Suc_le_eq)
-    done
+    using b'_im q(1) rs(1) by fastforce
   then have "r' \<in> cbox 0 One"
     unfolding r'_def cbox_def
     using b'_Basis
@@ -1899,9 +1862,8 @@
   have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point S) x = x"
   proof (rule_tac brouwer_ball[OF e(1)])
     show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
-      apply (rule continuous_on_compose)
-      using S compact_eq_bounded_closed continuous_on_closest_point apply blast
-      by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI)
+      by (meson assms closest_point_in_set compact_eq_bounded_closed contf continuous_on_closest_point
+          continuous_on_compose continuous_on_subset image_subsetI)
     show "(f \<circ> closest_point S) ` cball 0 e \<subseteq> cball 0 e"
       by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE)
   qed (use assms in auto)
@@ -2033,9 +1995,7 @@
     using \<open>bounded S\<close> bounded_subset_ballD by blast
   have notga: "g x \<noteq> a" for x
     unfolding g_def using fros fim \<open>a \<notin> T\<close>
-    apply (auto simp: frontier_def)
-    using fid interior_subset apply fastforce
-    by (simp add: \<open>a \<in> S\<close> closure_def)
+    by (metis Un_iff \<open>a \<in> S\<close> closure_Un_frontier fid imageI subset_eq)
   define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
   have "\<not> (frontier (cball a B) retract_of (cball a B))"
     by (metis no_retraction_cball \<open>0 < B\<close>)
@@ -2119,8 +2079,7 @@
           using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
           apply (simp add: in_segment)
           apply (rule_tac x = "dd x / k" in exI)
-          apply (simp add: field_simps that)
-          apply (simp add: vector_add_divide_simps algebra_simps)
+          apply (simp add: that vector_add_divide_simps algebra_simps)
           done
         ultimately show ?thesis
           using segsub by (auto simp: rel_frontier_def)
@@ -2163,8 +2122,7 @@
         then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
           using \<open>x \<noteq> a\<close> dd1 by fastforce
         with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
-          apply (auto simp: iff)
-          using less_eq_real_def mult_le_0_iff not_less u by fastforce
+          using less_eq_real_def mult_le_0_iff not_less u by (fastforce simp: iff)
       qed
     qed
     show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
@@ -2216,9 +2174,8 @@
   fixes S :: "'a::euclidean_space set"
   assumes "bounded S" "convex S" "a \<in> rel_interior S"
     shows "rel_frontier S retract_of (affine hull S - {a})"
-apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
-apply (auto simp: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
-done
+  by (meson assms convex_affine_hull dual_order.refl rel_frontier_affine_hull 
+      rel_frontier_deformation_retract_of_punctured_convex retract_of_def)
 
 corollary rel_boundary_retract_of_punctured_affine_hull:
   fixes S :: "'a::euclidean_space set"
@@ -2231,29 +2188,24 @@
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "bounded S" "a \<in> rel_interior S" "convex T" "rel_frontier S \<subseteq> T" "T \<subseteq> affine hull S"
   shows "(rel_frontier S) homotopy_eqv (T - {a})"
-  apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T])
-  using assms
-  apply auto
-  using deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym by blast
+  by (meson assms deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym 
+      rel_frontier_deformation_retract_of_punctured_convex[of S T])
 
 lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" "bounded S" "a \<in> rel_interior S"
     shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})"
-apply (rule homotopy_eqv_rel_frontier_punctured_convex)
-  using assms rel_frontier_affine_hull  by force+
+  by (simp add: assms homotopy_eqv_rel_frontier_punctured_convex rel_frontier_affine_hull)
 
 lemma path_connected_sphere_gen:
   assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
   shows "path_connected(rel_frontier S)"
-proof (cases "rel_interior S = {}")
-  case True
+proof -
+  have "convex (closure S)" 
+    using assms by auto
   then show ?thesis
-    by (simp add: \<open>convex S\<close> convex_imp_path_connected rel_frontier_def)
-next
-  case False
-  then show ?thesis
-    by (metis aff_dim_affine_hull affine_affine_hull affine_imp_convex all_not_in_conv assms path_connected_punctured_convex rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
+    by (metis Diff_empty aff_dim_affine_hull assms convex_affine_hull convex_imp_path_connected equals0I 
+       path_connected_punctured_convex rel_frontier_def rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
 qed
 
 lemma connected_sphere_gen:
@@ -2282,8 +2234,7 @@
   then show ?thesis
     apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
     apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
-    apply (intro conjI continuous_intros)
-    apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
+    apply (rule conjI continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
     done
 qed
 
@@ -2315,8 +2266,8 @@
       using ball_subset_cball [of a r] r by auto
     have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
                      (\<lambda>x. a + r *\<^sub>R g x)"
-      apply (rule continuous_intros)+
-      using \<open>continuous_on (s \<union> c) g\<close> ceq by blast
+      using \<open>continuous_on (s \<union> c) g\<close> ceq
+      by (intro continuous_intros) blast
     have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
             (\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
       by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
@@ -2326,10 +2277,8 @@
                   else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
       apply (subst cb_eq)
       apply (rule continuous_on_cases [OF _ _ cont1 cont2])
-        using ceq cin
-      apply (auto intro: closed_Un_complement_component
-                  simp: \<open>closed s\<close> open_Compl open_connected_component)
-      done
+      using \<open>closed s\<close> ceq cin 
+      by (force simp: closed_Diff open_Compl closed_Un_complement_component open_connected_component)+
     have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
              \<subseteq> sphere a r "
       using \<open>0 < r\<close> by (force simp: dist_norm ceq)
@@ -2384,12 +2333,7 @@
     and "x \<in> S"
     and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
   shows "\<exists>y\<in>cball a e. f y = x"
-  apply (rule brouwer_surjective)
-  apply (rule compact_cball convex_cball)+
-  unfolding cball_eq_empty
-  using assms
-  apply auto
-  done
+  by (smt (verit, best) assms brouwer_surjective cball_eq_empty compact_cball convex_cball)
 
 subsubsection \<open>Inverse function theorem\<close>
 
@@ -2510,8 +2454,7 @@
 
 lemma has_derivative_inverse_strong:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
-  assumes "open S"
-    and "x \<in> S"
+  assumes S: "open S" "x \<in> S"
     and contf: "continuous_on S f"
     and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and derf: "(f has_derivative f') (at x)"
@@ -2524,23 +2467,16 @@
     unfolding linear_conv_bounded_linear[symmetric]
     using id right_inverse_linear by blast
   moreover have "g' \<circ> f' = id"
-    using id linf ling
-    unfolding linear_conv_bounded_linear[symmetric]
-    using linear_inverse_left
-    by auto
+    using id linear_inverse_left linear_linear linf ling by blast
   moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    apply auto
-    done
+    using S derf contf id ling sussmann_open_mapping by blast
   have "continuous (at (f x)) g"
     unfolding continuous_at Lim_at
-  proof (rule, rule)
+  proof (intro strip)
     fix e :: real
     assume "e > 0"
     then have "f x \<in> interior (f ` (ball x e \<inter> S))"
-      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
-      by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
+      by (simp add: "*" S interior_open)
     then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
       unfolding mem_interior by blast
     show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
@@ -2550,16 +2486,11 @@
       then have "g y \<in> g ` f ` (ball x e \<inter> S)"
         by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
       then show "dist (g y) (g (f x)) < e"
-        using gf[OF \<open>x \<in> S\<close>]
-        by (simp add: assms(4) dist_commute image_iff)
+        using \<open>x \<in> S\<close> by (simp add: gf dist_commute image_iff)
     qed (use d in auto)
   qed
   moreover have "f x \<in> interior (f ` S)"
-    apply (rule sussmann_open_mapping)
-    apply (rule assms ling)+
-    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
-    apply auto
-    done
+    using "*" S interior_eq by blast
   moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
     by (metis gf imageE interiorE subsetD that)
   ultimately show ?thesis using assms
@@ -2576,26 +2507,20 @@
     and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and "(f has_derivative f') (at (g y))"
     and "f' \<circ> g' = id"
-    and "f (g y) = y"
+    and f: "f (g y) = y"
   shows "(g has_derivative g') (at y)"
-  using has_derivative_inverse_strong[OF assms(1-6)]
-  unfolding assms(7)
-  by simp
+  using has_derivative_inverse_strong[OF assms(1-6)] by (simp add: f)
 
 text \<open>On a region.\<close>
 
 theorem has_derivative_inverse_on:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "open S"
-    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+    and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
     and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
     and "f' x \<circ> g' x = id"
     and "x \<in> S"
   shows "(g has_derivative g'(x)) (at (f x))"
-proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
-  show "continuous_on S f"
-  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
-  using derf has_derivative_continuous by blast
-qed (use assms in auto)
+  by (meson assms continuous_on_eq_continuous_at has_derivative_continuous has_derivative_inverse_strong)
 
 end
diff -r 9e5a27486ca2 -r 7fd705b107f2 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Dec 27 10:38:34 2022 +0000
@@ -145,11 +145,8 @@
         proof cases
           assume "?R"
           with \<open>j \<in> S\<close> psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})"
-            apply (auto simp: subset_eq Ball_def)
-            apply (metis Diff_iff less_le_trans leD linear singletonD)
-            apply (metis Diff_iff less_le_trans leD linear singletonD)
-            apply (metis order_trans less_le_not_le linear)
-            done
+            apply (simp add: subset_eq Ball_def Bex_def)
+            by (metis order_le_less_trans order_less_le_trans order_less_not_sym)
           with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))"
             by (intro psubset) auto
           also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))"
@@ -162,19 +159,14 @@
             by (auto simp: not_less)
           let ?S1 = "{i \<in> S. l i < l j}"
           let ?S2 = "{i \<in> S. r i > r j}"
-
+          have *: "?S1 \<inter> ?S2 = {}"
+            using j by (fastforce simp add: disjoint_iff)
           have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))"
             using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
             by (intro sum_mono2) (auto intro: less_imp_le)
           also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) =
             (\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))"
-            using psubset(1) psubset.prems(1) j
-            apply (subst sum.union_disjoint)
-            apply simp_all
-            apply (subst sum.union_disjoint)
-            apply auto
-            apply (metis less_le_not_le)
-            done
+            using psubset(1) by (simp add: * sum.union_disjoint disjoint_iff_not_equal)
           also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u"
             using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
             apply (intro psubset.IH psubset)
@@ -202,31 +194,24 @@
     proof
       fix i
       note right_cont_F [of "r i"]
+      then have "\<exists>d>0. F (r i + d) - F (r i) < epsilon / 2 ^ (i + 2)"
+        by (simp add: continuous_at_right_real_increasing egt0)
       thus "\<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)"
-        apply -
-        apply (subst (asm) continuous_at_right_real_increasing)
-        apply (rule mono_F, assumption)
-        apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec)
-        apply (erule impE)
-        using egt0 by (auto simp add: field_simps)
+        by force
     qed
     then obtain delta where
         deltai_gt0: "\<And>i. delta i > 0" and
         deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)"
       by metis
     have "\<exists>a' > a. F a' - F a < epsilon / 2"
-      apply (insert right_cont_F [of a])
-      apply (subst (asm) continuous_at_right_real_increasing)
-      using mono_F apply force
-      apply (drule_tac x = "epsilon / 2" in spec)
-      using egt0 unfolding mult.commute [of 2] by force
+      using right_cont_F [of a]
+      by (metis continuous_at_right_real_increasing egt0 half_gt_zero less_add_same_cancel1 mono_F)
     then obtain a' where a'lea [arith]: "a' > a" and
       a_prop: "F a' - F a < epsilon / 2"
       by auto
     define S' where "S' = {i. l i < r i}"
-    obtain S :: "nat set" where
-      "S \<subseteq> S'" and finS: "finite S" and
-      Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
+    obtain S :: "nat set" where "S \<subseteq> S'" and finS: "finite S" 
+      and Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
     proof (rule compactE_image)
       show "compact {a'..b}"
         by (rule compact_Icc)
@@ -236,58 +221,34 @@
       also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
         unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans)
       also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})"
-        apply (intro UN_mono)
-        apply (auto simp: S'_def)
-        apply (cut_tac i=i in deltai_gt0)
-        apply simp
-        done
+        by (intro UN_mono; simp add: add.commute add_strict_increasing deltai_gt0 subset_iff)
       finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" .
     qed
     with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto
-    from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n"
-      by (subst finite_nat_set_iff_bounded_le [symmetric])
-    then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" ..
-    have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
-      apply (rule claim2 [rule_format])
-      using finS Sprop apply auto
-      apply (frule Sprop2)
-      apply (subgoal_tac "delta i > 0")
-      apply arith
-      by (rule deltai_gt0)
-    also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
-      apply (rule sum_mono)
-      apply simp
-      apply (rule order_trans)
-      apply (rule less_imp_le)
-      apply (rule deltai_prop)
-      by auto
-    also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
-        (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
-      by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
-    also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
-      apply (rule add_left_mono)
-      apply (rule mult_left_mono)
-      apply (rule sum_mono2)
-      using egt0 apply auto
-      by (frule Sbound, auto)
-    also have "... \<le> ?t + (epsilon / 2)"
-      apply (rule add_left_mono)
-      apply (subst geometric_sum)
-      apply auto
-      apply (rule mult_left_mono)
-      using egt0 apply auto
-      done
-    finally have aux2: "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2"
-      by simp
-
+    obtain n where Sbound: "\<And>i. i \<in> S \<Longrightarrow> i \<le> n"
+      using Max_ge finS by blast
     have "F b - F a = (F b - F a') + (F a' - F a)"
       by auto
     also have "... \<le> (F b - F a') + epsilon / 2"
       using a_prop by (intro add_left_mono) simp
     also have "... \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2"
-      apply (intro add_right_mono)
-      apply (rule aux2)
-      done
+    proof -
+      have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
+        using claim2 l_r Sprop by (simp add: deltai_gt0 finS add.commute add_strict_increasing)
+      also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
+        by (smt (verit) sum_mono deltai_prop)
+      also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
+        (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
+        by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
+      also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
+        using egt0 Sbound by (intro add_left_mono mult_left_mono sum_mono2) force+
+      also have "... \<le> ?t + (epsilon / 2)"
+        using egt0 by (simp add: geometric_sum add_left_mono mult_left_mono)
+      finally have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2"
+        by simp
+      then show ?thesis
+        by linarith
+    qed
     also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
       by auto
     also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
@@ -316,12 +277,8 @@
 
 lemma\<^marker>\<open>tag important\<close> sets_interval_measure [simp, measurable_cong]:
     "sets (interval_measure F) = sets borel"
-  apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
-  apply (rule sigma_sets_eqI)
-  apply auto
-  apply (case_tac "a \<le> ba")
-  apply (auto intro: sigma_sets.Empty)
-  done
+  apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc image_def split: prod.split)
+  by (metis greaterThanAtMost_empty nle_le)
 
 lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV"
   by (simp add: interval_measure_def space_extend_measure)
@@ -342,21 +299,16 @@
   show "((\<lambda>a. F b - F a) \<longlongrightarrow> emeasure ?F {a..b}) (at_left a)"
   proof (rule tendsto_at_left_sequentially)
     show "a - 1 < a" by simp
-    fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
-    with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
-      apply (intro Lim_emeasure_decseq)
-      apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
-      apply force
-      apply (subst (asm ) *)
-      apply (auto intro: less_le_trans less_imp_le)
-      done
+    fix X assume X: "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
+    then have "emeasure (interval_measure F) {X n<..b} \<noteq> \<infinity>" for n
+      by (smt (verit) "*" \<open>a \<le> b\<close> ennreal_neq_top infinity_ennreal_def)
+    with X have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
+      by (intro Lim_emeasure_decseq; force simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
     also have "(\<Inter>n. {X n <..b}) = {a..b}"
-      using \<open>\<And>n. X n < a\<close>
       apply auto
       apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>])
-      apply (auto intro: less_imp_le)
-      apply (auto intro: less_le_trans)
-      done
+      using less_eq_real_def apply presburger
+      using X(1) order_less_le_trans by blast
     also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))"
       using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans)
     finally show "(\<lambda>n. F b - F (X n)) \<longlonglongrightarrow> emeasure ?F {a..b}" .
@@ -426,12 +378,7 @@
   by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
 
 lemma lebesgue_on_UNIV_eq: "lebesgue_on UNIV = lebesgue"
-proof -
-  have "measure_of UNIV (sets lebesgue) (emeasure lebesgue) = lebesgue"
-    by (metis measure_of_of_measure space_borel space_completion space_lborel)
-  then show ?thesis
-    by (auto simp: restrict_space_def)
-qed
+  by (simp add: emeasure_restrict_space measure_eqI)
 
 lemma integral_restrict_Int:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -528,11 +475,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
   shows "f \<in> borel_measurable (lebesgue_on S)"
-  using assms
-  apply (simp add: in_borel_measurable_borel Ball_def)
-  apply (elim all_forward imp_forward asm_rl)
-  apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
-  done
+  using assms by (smt (verit) measurable_lebesgue_cong measurable_restrict_space1)
 
 lemma borel_measurable_if:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -557,33 +500,25 @@
 lemma borel_measurable_vimage_halfspace_component_lt:
      "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
       (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_less])
-  apply (fastforce simp add: space_restrict_space)
-  done
+  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_less])
 
 lemma borel_measurable_vimage_halfspace_component_ge:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
          (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_ge])
-  apply (fastforce simp add: space_restrict_space)
-  done
+  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_ge])
 
 lemma borel_measurable_vimage_halfspace_component_gt:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
          (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_greater])
-  apply (fastforce simp add: space_restrict_space)
-  done
+  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_greater])
 
 lemma borel_measurable_vimage_halfspace_component_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
          (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_le])
-  apply (fastforce simp add: space_restrict_space)
-  done
+  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_le])
 
 lemma
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -630,16 +565,12 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
          (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
-        (is "?lhs = ?rhs")
 proof -
-  have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
+  have eq: "{x \<in> S. f x \<in> T} = S - (S \<inter> f -` (- T))" for T
     by auto
   show ?thesis
-    apply (simp add: borel_measurable_vimage_open, safe)
-     apply (simp_all (no_asm) add: eq)
-     apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
-    apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
-    done
+    unfolding borel_measurable_vimage_open eq
+    by (metis Diff_Diff_Int closed_Compl diff_eq open_Compl sets.Diff sets_lebesgue_on_refl vimage_Compl)
 qed
 
 lemma borel_measurable_vimage_closed_interval:
@@ -689,9 +620,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
          (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
-  apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
-    apply (auto simp: in_borel_measurable_borel vimage_def)
-  done
+  by (smt (verit, best) Collect_cong UNIV_I borel_measurable_vimage_borel lebesgue_on_UNIV_eq)
 
 
 subsection \<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
@@ -699,13 +628,9 @@
 lemma continuous_imp_measurable_on_sets_lebesgue:
   assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"
   shows "f \<in> borel_measurable (lebesgue_on S)"
-proof -
-  have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)"
-    by (simp add: mono_restrict_space subsetI)
-  then show ?thesis
-    by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra 
-                  space_restrict_space)
-qed
+  by (metis borel_measurable_continuous_on_restrict borel_measurable_subalgebra f 
+      lebesgue_on_UNIV_eq mono_restrict_space sets_completionI_sets sets_lborel space_borel 
+      space_lebesgue_on space_restrict_space subsetI)
 
 lemma id_borel_measurable_lebesgue [iff]: "id \<in> borel_measurable lebesgue"
   by (simp add: measurable_completion)
@@ -741,12 +666,7 @@
   fixes l u :: real
   assumes [simp]: "l \<le> u"
   shows "emeasure lborel {l .. u} = u - l"
-proof -
-  have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}"
-    by (auto simp: space_PiM)
-  then show ?thesis
-    by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc)
-qed
+  by (simp add: emeasure_interval_measure_Icc lborel_eq_real)
 
 lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)"
   by simp
@@ -781,12 +701,7 @@
 lemma emeasure_lborel_Ioc[simp]:
   assumes [simp]: "l \<le> u"
   shows "emeasure lborel {l <.. u} = ennreal (u - l)"
-proof -
-  have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}"
-    using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
-  then show ?thesis
-    by simp
-qed
+  by (simp add: emeasure_interval_measure_Ioc lborel_eq_real)
 
 lemma emeasure_lborel_Ico[simp]:
   assumes [simp]: "l \<le> u"
@@ -830,26 +745,12 @@
   by (auto simp: emeasure_lborel_box_eq)
 
 lemma emeasure_lborel_ball_finite: "emeasure lborel (ball c r) < \<infinity>"
-proof -
-  have "bounded (ball c r)" by simp
-  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "ball c r \<subseteq> cbox (-a) a"
-    by auto
-  hence "emeasure lborel (ball c r) \<le> emeasure lborel (cbox (-a) a)"
-    by (intro emeasure_mono) auto
-  also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
-  finally show ?thesis .
-qed
+  by (metis bounded_ball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite
+      emeasure_mono order_le_less_trans sets_lborel)
 
 lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \<infinity>"
-proof -
-  have "bounded (cball c r)" by simp
-  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "cball c r \<subseteq> cbox (-a) a"
-    by auto
-  hence "emeasure lborel (cball c r) \<le> emeasure lborel (cbox (-a) a)"
-    by (intro emeasure_mono) auto
-  also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
-  finally show ?thesis .
-qed
+  by (metis bounded_cball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite 
+            emeasure_mono order_le_less_trans sets_lborel)
 
 lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel"
   and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
@@ -924,7 +825,7 @@
   also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
     by (rule emeasure_UN_eq_0) auto
   finally show ?thesis
-    by (auto simp add: )
+    by simp
 qed
 
 lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
@@ -934,30 +835,18 @@
   by (intro countable_imp_null_set_lborel countable_finite)
 
 lemma insert_null_sets_iff [simp]: "insert a N \<in> null_sets lebesgue \<longleftrightarrow> N \<in> null_sets lebesgue"     
-    (is "?lhs = ?rhs")
-proof
-  assume ?lhs then show ?rhs
-    by (meson completion.complete2 subset_insertI)
-next
-  assume ?rhs then show ?lhs
-  by (simp add: null_sets.insert_in_sets null_setsI)
-qed
+  by (meson completion.complete2 finite.simps finite_imp_null_set_lborel null_sets.insert_in_sets 
+      null_sets_completionI subset_insertI)
 
 lemma insert_null_sets_lebesgue_on_iff [simp]:
   assumes "a \<in> S" "S \<in> sets lebesgue"
   shows "insert a N \<in> null_sets (lebesgue_on S) \<longleftrightarrow> N \<in> null_sets (lebesgue_on S)"     
   by (simp add: assms null_sets_restrict_space)
 
-lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
-proof
-  assume asm: "lborel = count_space A"
-  have "space lborel = UNIV" by simp
-  hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
-  have "emeasure lborel {undefined::'a} = 1"
-      by (subst asm, subst emeasure_count_space_finite) auto
-  moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
-  ultimately show False by contradiction
-qed
+lemma lborel_neq_count_space[simp]: 
+  fixes A :: "('a::ordered_euclidean_space) set"
+  shows "lborel \<noteq> count_space A"
+  by (metis finite.simps finite_imp_null_set_lborel insert_not_empty null_sets_count_space singleton_iff)
 
 lemma mem_closed_if_AE_lebesgue_open:
   assumes "open S" "closed C"
@@ -1004,13 +893,9 @@
   let ?A = "\<lambda>n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set"
   show "range ?A \<subseteq> ?E" "(\<Union>i. ?A i) = UNIV"
     unfolding UN_box_eq_UNIV by auto
-
-  { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
-  { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
-      apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
-      apply (subst box_eq_empty(1)[THEN iffD2])
-      apply (auto intro: less_imp_le simp: not_le)
-      done }
+  show "emeasure lborel (?A i) \<noteq> \<infinity>" for i by auto 
+  show "emeasure lborel X = emeasure M X" if "X \<in> ?E" for X
+    using that box_eq_empty(1) by (fastforce simp: emeasure_eq emeasure_lborel_box_eq)
 qed
 
 lemma\<^marker>\<open>tag important\<close> lborel_affine_euclidean:
@@ -1102,7 +987,7 @@
     by (auto simp: null_sets_def)
 
   show "T \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
-    by (rule completion.measurable_completion2) (auto simp: eq measurable_completion)
+    by (simp add: completion.measurable_completion2 eq measurable_completion)
 
   have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))"
     using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
@@ -1135,7 +1020,7 @@
 
 lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
 proof cases
-  assume "x = 0"
+  assume "x = 0" 
   then have "(*\<^sub>R) x = (\<lambda>x. 0::'a)"
     by (auto simp: fun_eq_iff)
   then show ?thesis by auto
@@ -1352,8 +1237,7 @@
 lemma
   fixes a::real
   shows lmeasurable_interval [iff]: "{a..b} \<in> lmeasurable" "{a<..<b} \<in> lmeasurable"
-  apply (metis box_real(2) lmeasurable_cbox)
-  by (metis box_real(1) lmeasurable_box)
+  by (metis box_real lmeasurable_box lmeasurable_cbox)+
 
 lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
   using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
@@ -1387,14 +1271,7 @@
   by (simp add: bounded_interior lmeasurable_open)
 
 lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
-proof -
-  have "emeasure lborel (cbox a b - box a b) = 0"
-    by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
-  then have "cbox a b - box a b \<in> null_sets lborel"
-    by (auto simp: null_sets_def)
-  then show ?thesis
-    by (auto dest!: AE_not_in)
-qed
+  by (simp add: emeasure_Diff emeasure_lborel_box_eq emeasure_lborel_cbox_eq null_setsI subset_box)
 
 lemma bounded_set_imp_lmeasurable:
   assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
@@ -1423,10 +1300,8 @@
     by (simp add: sigma_sets.Empty)
 next
   case (Compl a)
-  then have "\<Omega> - a \<subseteq> \<Omega>" "a \<subseteq> \<Omega>"
-    by (auto simp: sigma_sets_into_sp [OF \<open>M \<subseteq> Pow \<Omega>\<close>])
-  then show ?case
-    by (auto simp: inj_on_image_set_diff [OF \<open>inj_on f \<Omega>\<close>] assms intro: Compl sigma_sets.Compl)
+  with assms show ?case
+    by (metis inj_on_image_set_diff sigma_sets.Compl sigma_sets_into_sp)
 next
   case (Union a) then show ?case
     by (metis image_UN sigma_sets.simps)
@@ -1475,9 +1350,8 @@
 lemma measurable_translation:
    "S \<in> lmeasurable \<Longrightarrow> ((+) a ` S) \<in> lmeasurable"
   using emeasure_lebesgue_affine [of 1 a S]
-  apply (auto intro: lebesgue_sets_translation simp add: fmeasurable_def cong: image_cong_simp)
-  apply (simp add: ac_simps)
-  done
+  by (smt (verit, best) add.commute ennreal_1 fmeasurable_def image_cong lambda_one 
+          lebesgue_sets_translation mem_Collect_eq power_one scaleR_one)
 
 lemma measurable_translation_subtract:
    "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. x - a) ` S) \<in> lmeasurable"
@@ -1508,11 +1382,10 @@
 
   let ?f = "\<lambda>n. root DIM('a) (Suc n)"
 
-  have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
-    apply safe
-    subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
-    subgoal by auto
-    done
+  have "?f n *\<^sub>R x \<in> S \<Longrightarrow> x \<in> (*\<^sub>R) (1 / ?f n) ` S" for x n
+    by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
+  then have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
+    by auto
 
   have eq: "(1 / ?f n) ^ DIM('a) = 1 / Suc n" for n
     by (simp add: field_simps)
@@ -1642,12 +1515,12 @@
                    "emeasure (completion M) A = emeasure M A'"
 proof -
   from AE_notin_null_part[OF A] obtain N where N: "N \<in> null_sets M" "null_part M A \<subseteq> N"
-    unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto
+    by (meson assms null_part)
   let ?A' = "main_part M A \<union> N"
   show ?thesis
   proof
     show "A \<subseteq> ?A'"
-      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[symmetric, OF A]) auto
+      using \<open>null_part M A \<subseteq> N\<close> assms main_part_null_part_Un by blast
     have "main_part M A \<subseteq> A"
       using assms main_part_null_part_Un by auto
     then have "?A' - A \<subseteq> N"
diff -r 9e5a27486ca2 -r 7fd705b107f2 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Library/BigO.thy	Tue Dec 27 10:38:34 2022 +0000
@@ -42,49 +42,22 @@
 lemma bigo_pos_const:
   "(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
     (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
-  apply auto
-  apply (case_tac "c = 0")
-   apply simp
-   apply (rule_tac x = "1" in exI)
-   apply simp
-  apply (rule_tac x = "\<bar>c\<bar>" in exI)
-  apply auto
-  apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
-   apply (erule_tac x = x in allE)
-   apply force
-  apply (rule mult_right_mono)
-   apply (rule abs_ge_self)
-  apply (rule abs_ge_zero)
-  done
+  by (metis (no_types, opaque_lifting) abs_ge_zero abs_not_less_zero abs_of_nonneg dual_order.trans 
+        mult_1 zero_less_abs_iff zero_less_mult_iff zero_less_one)
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
   by (auto simp add: bigo_def bigo_pos_const)
 
 lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
   apply (auto simp add: bigo_alt_def)
-  apply (rule_tac x = "ca * c" in exI)
-  apply (rule conjI)
-   apply simp
-  apply (rule allI)
-  apply (drule_tac x = "xa" in spec)+
-  apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
-   apply (erule order_trans)
-   apply (simp add: ac_simps)
-  apply (rule mult_left_mono, assumption)
-  apply (rule order_less_imp_le, assumption)
-  done
+  by (metis (no_types, opaque_lifting) mult.assoc mult_le_cancel_iff2 order.trans 
+      zero_less_mult_iff)
 
 lemma bigo_refl [intro]: "f \<in> O(f)"
-  apply (auto simp add: bigo_def)
-  apply (rule_tac x = 1 in exI)
-  apply simp
-  done
+  using bigo_def comm_monoid_mult_class.mult_1 dual_order.eq_iff by blast
 
 lemma bigo_zero: "0 \<in> O(g)"
-  apply (auto simp add: bigo_def func_zero)
-  apply (rule_tac x = 0 in exI)
-  apply auto
-  done
+  using bigo_def mult_le_cancel_left1 by fastforce
 
 lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
   by (auto simp add: bigo_def)
@@ -92,21 +65,10 @@
 lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
   apply (auto simp add: bigo_alt_def set_plus_def)
   apply (rule_tac x = "c + ca" in exI)
-  apply auto
-  apply (simp add: ring_distribs func_plus)
-  apply (rule order_trans)
-   apply (rule abs_triangle_ineq)
-  apply (rule add_mono)
-   apply force
-  apply force
-  done
+  by (smt (verit, best) abs_triangle_ineq add_mono add_pos_pos comm_semiring_class.distrib dual_order.trans)
 
 lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
-  apply (rule equalityI)
-   apply (rule bigo_plus_self_subset)
-  apply (rule set_zero_plus2)
-  apply (rule bigo_zero)
-  done
+  by (simp add: antisym bigo_plus_self_subset bigo_zero set_zero_plus2)
 
 lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
   apply (rule subsetI)
@@ -117,37 +79,22 @@
    apply (rule_tac x = "c + c" in exI)
    apply (clarsimp)
    apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
-    apply (erule_tac x = xa in allE)
-    apply (erule order_trans)
-    apply (simp)
+    apply (metis mult_2 order_trans)
    apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
-    apply (erule order_trans)
-    apply (simp add: ring_distribs)
-   apply (rule mult_left_mono)
-    apply (simp add: abs_triangle_ineq)
-   apply (simp add: order_less_le)
+    apply auto[1]
+  using abs_triangle_ineq mult_le_cancel_iff2 apply blast
+  apply (simp add: order_less_le)
   apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
   apply (rule conjI)
    apply (rule_tac x = "c + c" in exI)
    apply auto
   apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
-   apply (erule_tac x = xa in allE)
-   apply (erule order_trans)
-   apply simp
-  apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
-   apply (erule order_trans)
-   apply (simp add: ring_distribs)
-  apply (rule mult_left_mono)
-   apply (rule abs_triangle_ineq)
-  apply (simp add: order_less_le)
+   apply (metis mult_2 order.trans)
+  apply simp
   done
 
 lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
-  apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
-   apply (erule order_trans)
-   apply simp
-  apply (auto del: subsetI simp del: bigo_plus_idemp)
-  done
+  using bigo_plus_idemp set_plus_mono2 by blast
 
 lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"
   apply (rule equalityI)
@@ -157,8 +104,7 @@
   apply (rule_tac x = "max c ca" in exI)
   apply (rule conjI)
    apply (subgoal_tac "c \<le> max c ca")
-    apply (erule order_less_le_trans)
-    apply assumption
+    apply linarith
    apply (rule max.cobounded1)
   apply clarify
   apply (drule_tac x = "xa" in spec)+
@@ -167,21 +113,9 @@
    apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
     apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
      apply force
-    apply (rule add_mono)
-     apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
-      apply force
-     apply (rule mult_right_mono)
-      apply (rule max.cobounded1)
-     apply assumption
-    apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
-     apply force
-    apply (rule mult_right_mono)
-     apply (rule max.cobounded2)
-    apply assumption
-   apply (rule abs_triangle_ineq)
-  apply (rule add_nonneg_nonneg)
-   apply assumption+
-  done
+    apply (metis add_mono le_max_iff_disj max_mult_distrib_right)
+  using abs_triangle_ineq apply blast
+  using add_nonneg_nonneg by blast
 
 lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
   apply (auto simp add: bigo_def)