# HG changeset patch
# User paulson
# Date 1672229725 0
# Node ID 18e719c6b6333841781af7bf09cb309e11b813d4
# Parent  04af11e6557a84cb432b8da2b5422caad34e60e9# Parent  454984e807db415f3c5b89724dab7eb44c0b8458
merged

diff -r 04af11e6557a -r 18e719c6b633 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Dec 27 22:52:28 2022 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Dec 28 12:15:25 2022 +0000
@@ -33,13 +33,13 @@
   by (simp add: sphere_def)
 
 lemma ball_trivial [simp]: "ball x 0 = {}"
-  by (simp add: ball_def)
+  by auto
 
 lemma cball_trivial [simp]: "cball x 0 = {x}"
-  by (simp add: cball_def)
+  by auto
 
 lemma sphere_trivial [simp]: "sphere x 0 = {x}"
-  by (simp add: sphere_def)
+  by auto
 
 lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
   using dist_triangle_less_add not_le by fastforce
@@ -196,9 +196,7 @@
   by (simp add: interior_open)
 
 lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
-  apply (simp add: set_eq_iff not_le)
-  apply (metis zero_le_dist dist_self order_less_le_trans)
-  done
+  by (smt (verit, best) Diff_empty ball_eq_empty cball_diff_sphere centre_in_ball centre_in_cball sphere_empty)
 
 lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
   by simp
@@ -215,8 +213,7 @@
   using ball_divide_subset one_le_numeral by blast
 
 lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
-  apply (cases "e < 0", simp add: field_split_simps)
-  by (metis div_by_1 frac_le less_numeral_extra(1) not_le order_refl subset_cball)
+  by (smt (verit, best) cball_empty div_by_1 frac_le subset_cball zero_le_divide_iff)
 
 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
   using cball_divide_subset one_le_numeral by blast
@@ -292,13 +289,7 @@
 
 lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
   for x :: "'a::metric_space"
-  apply (clarsimp simp add: islimpt_approachable)
-  apply (drule_tac x="e/2" in spec)
-  apply (auto simp: simp del: less_divide_eq_numeral1)
-  apply (drule_tac x="dist x' x" in spec)
-  apply (auto simp del: less_divide_eq_numeral1)
-  apply metric
-  done
+  by (metis islimpt_def islimpt_eq_acc_point mem_Collect_eq)
 
 lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
   using closed_limpt limpt_of_limpts by blast
@@ -308,14 +299,12 @@
   by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
 
 lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"
-  apply (simp add: islimpt_eq_acc_point, safe)
-   apply (metis Int_commute open_ball centre_in_ball)
-  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
+  unfolding islimpt_eq_acc_point
+  by (metis open_ball Int_commute Int_mono finite_subset open_contains_ball_eq subset_eq)
 
 lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"
-  apply (simp add: islimpt_eq_infinite_ball, safe)
-   apply (meson Int_mono ball_subset_cball finite_subset order_refl)
-  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
+  unfolding islimpt_eq_infinite_ball
+  by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
 
 
 subsection \<open>Perfect Metric Spaces\<close>
@@ -327,17 +316,11 @@
 lemma cball_eq_sing:
   fixes x :: "'a::{metric_space,perfect_space}"
   shows "cball x e = {x} \<longleftrightarrow> e = 0"
-proof (rule linorder_cases)
-  assume e: "0 < e"
-  obtain a where "a \<noteq> x" "dist a x < e"
-    using perfect_choose_dist [OF e] by auto
-  then have "a \<noteq> x" "dist x a \<le> e"
-    by (auto simp: dist_commute)
-  with e show ?thesis by (auto simp: set_eq_iff)
-qed auto
-
-
-subsection \<open>?\<close>
+  by (smt (verit, best) open_ball ball_eq_empty ball_subset_cball cball_empty cball_trivial 
+      not_open_singleton subset_singleton_iff)
+
+
+subsection \<open>Finite and discrete\<close>
 
 lemma finite_ball_include:
   fixes a :: "'a::metric_space"
@@ -364,19 +347,7 @@
   then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
     by blast
   show ?case
-  proof (cases "x = a")
-    case True
-    with \<open>d > 0 \<close>d show ?thesis by auto
-  next
-    case False
-    let ?d = "min d (dist a x)"
-    from False \<open>d > 0\<close> have dp: "?d > 0"
-      by auto
-    from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
-      by auto
-    with dp False show ?thesis
-      by (metis insert_iff le_less min_less_iff_conj not_less)
-  qed
+    by (smt (verit, del_insts) dist_pos_lt insert.IH insert_iff)
 qed (auto intro: zero_less_one)
 
 lemma discrete_imp_closed:
@@ -388,7 +359,7 @@
   have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   proof -
     from e have e2: "e/2 > 0" by arith
-    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
+    from C[OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
       by blast
     from e2 y(2) have mp: "min (e/2) (dist x y) > 0"
       by simp
@@ -438,9 +409,7 @@
 corollary Lim_withinI [intro?]:
   assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e"
   shows "(f \<longlongrightarrow> l) (at a within S)"
-  apply (simp add: Lim_within, clarify)
-  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
-  done
+  unfolding Lim_within by (smt (verit, ccfv_SIG) assms zero_less_dist_iff)
 
 proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
@@ -450,11 +419,7 @@
   fixes a :: "'a::metric_space" and l :: "'b::metric_space"
   shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within S); eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)\<rbrakk>
          \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
-apply (clarsimp simp: eventually_at Lim_within)
-apply (drule_tac x=e in spec, clarify)
-apply (rename_tac k)
-apply (rule_tac x="min d k" in exI, simp)
-done
+  by (simp add: eventually_at Lim_within) (smt (verit, best))
 
 text \<open>Another limit point characterization.\<close>
 
@@ -471,7 +436,7 @@
     by metis
   define f where "f \<equiv> rec_nat (y 1) (\<lambda>n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
   have [simp]: "f 0 = y 1"
-               "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
+            and fSuc: "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
     by (simp_all add: f_def)
   have f: "f n \<in> S \<and> (f n \<noteq> x) \<and> dist (f n) x < inverse(2 ^ n)" for n
   proof (induction n)
@@ -479,11 +444,10 @@
       by (simp add: y)
   next
     case (Suc n) then show ?case
-      apply (auto simp: y)
-      by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)
+      by (smt (verit, best) fSuc dist_pos_lt inverse_positive_iff_positive y zero_less_power)
   qed
   show ?rhs
-  proof (rule_tac x=f in exI, intro conjI allI)
+  proof (intro exI conjI allI)
     show "\<And>n. f n \<in> S - {x}"
       using f by blast
     have "dist (f n) x < dist (f m) x" if "m < n" for m n
@@ -497,7 +461,7 @@
       proof cases
         assume "m < n"
         have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
-          by simp
+          by (simp add: fSuc)
         also have "\<dots> < dist (f n) x"
           by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
         also have "\<dots> < dist (f m) x"
@@ -505,17 +469,16 @@
         finally show ?thesis .
       next
         assume "m = n" then show ?case
-          by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)
+          by (smt (verit, best) dist_pos_lt f fSuc y)
       qed
     qed
     then show "inj f"
       by (metis less_irrefl linorder_injI)
-    show "f \<longlonglongrightarrow> x"
-      apply (rule tendstoI)
-      apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
+    have "\<And>e n. \<lbrakk>0 < e; nat \<lceil>1 / e\<rceil> \<le> n\<rbrakk> \<Longrightarrow> dist (f n) x < e"
       apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
-      apply (simp add: field_simps)
-      by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
+      by (simp add: divide_simps order_le_less_trans)
+    then show "f \<longlonglongrightarrow> x"
+      using lim_sequentially by blast
   qed
 next
   assume ?rhs
@@ -548,70 +511,49 @@
   assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"
   shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"
   apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
-  apply (intro all_cong ex_cong, safe)
-  apply (erule_tac x="a + d" in allE, simp)
-  apply (simp add: nondecF field_simps)
-  apply (drule nondecF, simp)
-  done
+  apply (intro all_cong ex_cong)
+  by (smt (verit, best) nondecF)
 
 lemma continuous_at_left_real_increasing:
   assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
-  shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
+  shows "(continuous (at_left (a :: real)) f) \<longleftrightarrow> (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
   apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
-  apply (intro all_cong ex_cong, safe)
-  apply (erule_tac x="a - d" in allE, simp)
-  apply (simp add: nondecF field_simps)
-  apply (cut_tac x="a - d" and y=x in nondecF, simp_all)
-  done
+  apply (intro all_cong ex_cong)
+  by (smt (verit) nondecF)
 
 text\<open>Versions in terms of open balls.\<close>
 
 lemma continuous_within_ball:
-  "continuous (at x within s) f \<longleftrightarrow>
-    (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)"
+  "continuous (at x within S) f \<longleftrightarrow>
+    (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> S) \<subseteq> ball (f x) e)"
   (is "?lhs = ?rhs")
 proof
   assume ?lhs
   {
     fix e :: real
     assume "e > 0"
-    then obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
+    then obtain d where "d>0" and d: "\<forall>y\<in>S. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e"
       using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto
-    {
-      fix y
-      assume "y \<in> f ` (ball x d \<inter> s)"
-      then have "y \<in> ball (f x) e"
-        using d(2)
-        using \<open>e > 0\<close>
-        by (auto simp: dist_commute)
+    { fix y
+      assume "y \<in> f ` (ball x d \<inter> S)" then have "y \<in> ball (f x) e"
+        using d \<open>e > 0\<close> by (auto simp: dist_commute)
     }
-    then have "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e"
-      using \<open>d > 0\<close>
-      unfolding subset_eq ball_def by (auto simp: dist_commute)
+    then have "\<exists>d>0. f ` (ball x d \<inter> S) \<subseteq> ball (f x) e"
+      using \<open>d > 0\<close> by blast
   }
   then show ?rhs by auto
 next
   assume ?rhs
   then show ?lhs
-    unfolding continuous_within Lim_within ball_def subset_eq
-    apply (auto simp: dist_commute)
-    apply (erule_tac x=e in allE, auto)
-    done
+    apply (simp add: continuous_within Lim_within ball_def subset_eq)
+    by (metis (mono_tags, lifting) Int_iff dist_commute mem_Collect_eq)
 qed
 
 lemma continuous_at_ball:
-  "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
-    by (metis dist_commute dist_pos_lt dist_self)
-next
-  assume ?rhs
-  then show ?lhs
-    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
-    by (metis dist_commute)
-qed
+  "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)"
+  apply (simp add: continuous_at Lim_at subset_eq Ball_def Bex_def image_iff)
+  by (smt (verit, ccfv_threshold) dist_commute dist_self)
+
 
 text\<open>Define setwise continuity in terms of limits within the set.\<close>
 
@@ -622,16 +564,14 @@
   by (metis dist_pos_lt dist_self)
 
 lemma continuous_within_E:
-  assumes "continuous (at x within s) f" "e>0"
-  obtains d where "d>0"  "\<And>x'. \<lbrakk>x'\<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
-  using assms apply (simp add: continuous_within_eps_delta)
-  apply (drule spec [of _ e], clarify)
-  apply (rule_tac d="d/2" in that, auto)
-  done
+  assumes "continuous (at x within S) f" "e>0"
+  obtains d where "d>0"  "\<And>x'. \<lbrakk>x'\<in> S; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+  using assms unfolding continuous_within_eps_delta
+  by (metis dense order_le_less_trans)
 
 lemma continuous_onI [intro?]:
-  assumes "\<And>x e. \<lbrakk>e > 0; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
-  shows "continuous_on s f"
+  assumes "\<And>x e. \<lbrakk>e > 0; x \<in> S\<rbrakk> \<Longrightarrow> \<exists>d>0. \<forall>x'\<in>S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
+  shows "continuous_on S f"
 apply (simp add: continuous_on_iff, clarify)
 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
 done
@@ -642,10 +582,7 @@
     assumes "continuous_on s f" "x\<in>s" "e>0"
     obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
   using assms
-  apply (simp add: continuous_on_iff)
-  apply (elim ballE allE)
-  apply (auto intro: that [where d="d/2" for d])
-  done
+  unfolding continuous_on_iff by (metis dense order_le_less_trans)
 
 text\<open>The usual transformation theorems.\<close>
 
@@ -657,8 +594,7 @@
     and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
   shows "continuous (at x within s) g"
   using assms
-  unfolding continuous_within
-  by (force intro: Lim_transform_within)
+  unfolding continuous_within by (force intro: Lim_transform_within)
 
 
 subsection \<open>Closure and Limit Characterization\<close>
@@ -666,9 +602,7 @@
 lemma closure_approachable:
   fixes S :: "'a::metric_space set"
   shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
-  apply (auto simp: closure_def islimpt_approachable)
-  apply (metis dist_self)
-  done
+  using dist_self by (force simp: closure_def islimpt_approachable)
 
 lemma closure_approachable_le:
   fixes S :: "'a::metric_space set"
@@ -693,14 +627,13 @@
 proof -
   have *: "\<forall>x\<in>S. Inf S \<le> x"
     using cInf_lower[of _ S] assms by metis
-  {
-    fix e :: real
+  { fix e :: real
     assume "e > 0"
     then have "Inf S < Inf S + e" by simp
     with assms obtain x where "x \<in> S" "x < Inf S + e"
-      by (subst (asm) cInf_less_iff) auto
+      using cInf_lessD by blast
     with * have "\<exists>x\<in>S. dist x (Inf S) < e"
-      by (intro bexI[of _ x]) (auto simp: dist_real_def)
+      using dist_real_def by force
   }
   then show ?thesis unfolding closure_approachable by auto
 qed
@@ -717,9 +650,9 @@
     assume "e > 0"
     then have "Sup S - e < Sup S" by simp
     with assms obtain x where "x \<in> S" "Sup S - e < x"
-      by (subst (asm) less_cSup_iff) auto
+      using less_cSupE by blast
     with * have "\<exists>x\<in>S. dist x (Sup S) < e"
-      by (intro bexI[of _ x]) (auto simp: dist_real_def)
+      using dist_real_def by force
   }
   then show ?thesis unfolding closure_approachable by auto
 qed
@@ -730,8 +663,7 @@
 proof
   show ?rhs if ?lhs
   proof -
-    {
-      fix e :: real
+    { fix e :: real
       assume "e > 0"
       then obtain y where "y \<in> S - {x}" and "dist y x < e"
         using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
@@ -744,8 +676,7 @@
   qed
   show ?lhs if ?rhs
   proof -
-    {
-      fix e :: real
+    { fix e :: real
       assume "e > 0"
       then obtain y where "y \<in> S \<inter> ball x e - {x}"
         using \<open>?rhs\<close> by blast
@@ -804,8 +735,7 @@
 proof -
   from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a"
     unfolding bounded_def by auto
-  {
-    fix y
+  { fix y
     assume "y \<in> closure S"
     then obtain f where f: "\<forall>n. f n \<in> S"  "(f \<longlongrightarrow> y) sequentially"
       unfolding closure_sequential by auto
@@ -1299,10 +1229,7 @@
     and xy: "\<forall>u\<in>S. \<forall>v\<in>S. dist u v \<le> dist x y"
     using compact_sup_maxdistance[OF assms] by auto
   then have "diameter S \<le> dist x y"
-    unfolding diameter_def
-    apply clarsimp
-    apply (rule cSUP_least, fast+)
-    done
+    unfolding diameter_def by (force intro!: cSUP_least)
   then show ?thesis
     by (metis b diameter_bounded_bound order_antisym xys)
 qed
@@ -1332,12 +1259,12 @@
   assumes "bounded S"
   shows "diameter(closure S) = diameter S"
 proof (rule order_antisym)
-  have "False" if "diameter S < diameter (closure S)"
+  have "False" if d_less_d: "diameter S < diameter (closure S)"
   proof -
     define d where "d = diameter(closure S) - diameter(S)"
     have "d > 0"
       using that by (simp add: d_def)
-    then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
+    then have dle: "diameter(closure(S)) - d / 2 < diameter(closure(S))"
       by simp
     have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
       by (simp add: d_def field_split_simps)
@@ -1346,14 +1273,13 @@
     moreover have "0 \<le> diameter S"
       using assms diameter_ge_0 by blast
     ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
-      using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
+      by (smt (verit) dle d_less_d d_def dd diameter_lower_bounded)
     then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"
-      using closure_approachable
-      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
+      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral closure_approachable)
     then have "dist x' y' \<le> diameter S"
       using assms diameter_bounded_bound by blast
     with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"
-      by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
+      by (meson add_mono dist_triangle dist_triangle3 less_eq_real_def order_trans)
     then show ?thesis
       using xy d_def by linarith
   qed
@@ -1421,8 +1347,7 @@
       then have "T \<subseteq> ball y \<delta>"
         using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
       then show ?thesis
-        apply (rule_tac x=C in bexI)
-        using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
+        by (meson \<open>C \<in> \<C>\<close> \<open>ball y \<delta> \<subseteq> C\<close> subset_eq)
     qed
   qed
 qed
@@ -1490,8 +1415,7 @@
   obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
     unfolding comp_def by (metis seq_monosub)
   then have "Bseq (f \<circ> r)"
-    unfolding Bseq_eq_bounded using f
-    by (metis BseqI' bounded_iff comp_apply rangeI)
+    unfolding Bseq_eq_bounded by (metis f BseqI' bounded_iff comp_apply rangeI)
   with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
     using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
@@ -1525,32 +1449,31 @@
       using k
       by (rule bounded_proj)
     obtain l1::"'a" and r1 where r1: "strict_mono r1"
-      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
-      using insert(3) using insert(4) by auto
+      and lr1: "\<forall>e > 0. \<forall>\<^sub>F n in sequentially. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e"
+      using insert by auto
     have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
       by simp
     have "bounded (range (\<lambda>i. f (r1 i) proj k))"
       by (metis (lifting) bounded_subset f' image_subsetI s')
-    then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
+    then obtain l2 r2 where r2: "strict_mono r2" and lr2: "(\<lambda>i. f (r1 (r2 i)) proj k) \<longlonglongrightarrow> l2"
       using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
       by (auto simp: o_def)
     define r where "r = r1 \<circ> r2"
-    have r:"strict_mono r"
+    have r: "strict_mono r"
       using r1 and r2 unfolding r_def o_def strict_mono_def by auto
     moreover
     define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"
-    {
-      fix e::real
+    { fix e::real
       assume "e > 0"
-      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
+      from lr1 \<open>e > 0\<close> have N1: "\<forall>\<^sub>F n in sequentially. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e"
         by blast
-      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
+      from lr2 \<open>e > 0\<close> have N2: "\<forall>\<^sub>F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < e"
         by (rule tendstoD)
-      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
+      from r2 N1 have N1': "\<forall>\<^sub>F n in sequentially. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e"
         by (rule eventually_subseq)
-      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
+      have "\<forall>\<^sub>F n in sequentially. \<forall>i\<in>insert k d. dist (f (r n) proj i) (l proj i) < e"
         using N1' N2
-        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
+        by eventually_elim (use insert.prems in \<open>auto simp: l_def r_def o_def proj_unproj\<close>)
     }
     ultimately show ?case by auto
   qed
@@ -1576,7 +1499,7 @@
     using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
     by (auto simp: image_comp intro: bounded_snd bounded_subset)
-  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
+  obtain l2 r2 where r2: "strict_mono r2" and l2: "(\<lambda>n. snd (f (r1 (r2 n)))) \<longlonglongrightarrow> l2"
     using bounded_imp_convergent_subsequence [OF s2]
     unfolding o_def by fast
   have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
@@ -1619,13 +1542,9 @@
       fix e :: real
       assume "e > 0"
       from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2"
-        unfolding cauchy_def
-        using \<open>e > 0\<close>
-        apply (erule_tac x="e/2" in allE, auto)
-        done
-      from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]
-      obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
-        using \<open>e > 0\<close> by auto
+        unfolding cauchy_def using \<open>e > 0\<close> by (meson half_gt_zero)
+      then obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
+        by (metis dist_self lim_sequentially lr(3))
       {
         fix n :: nat
         assume n: "n \<ge> max N M"
@@ -1756,58 +1675,28 @@
 instance heine_borel < complete_space
 proof
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
-  then have "bounded (range f)"
-    by (rule cauchy_imp_bounded)
-  then have "compact (closure (range f))"
-    unfolding compact_eq_bounded_closed by auto
-  then have "complete (closure (range f))"
-    by (rule compact_imp_complete)
-  moreover have "\<forall>n. f n \<in> closure (range f)"
-    using closure_subset [of "range f"] by auto
-  ultimately have "\<exists>l\<in>closure (range f). (f \<longlongrightarrow> l) sequentially"
-    using \<open>Cauchy f\<close> unfolding complete_def by auto
   then show "convergent f"
-    unfolding convergent_def by auto
+    unfolding convergent_def
+    using Cauchy_converges_subseq cauchy_imp_bounded bounded_imp_convergent_subsequence by blast
 qed
 
 lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"
 proof (rule completeI)
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
-  then have "convergent f" by (rule Cauchy_convergent)
-  then show "\<exists>l\<in>UNIV. f \<longlonglongrightarrow> l" unfolding convergent_def by simp
+  then show "\<exists>l\<in>UNIV. f \<longlonglongrightarrow> l" 
+    using Cauchy_convergent convergent_def by blast
 qed
 
 lemma complete_imp_closed:
   fixes S :: "'a::metric_space set"
-  assumes "complete S"
-  shows "closed S"
-proof (unfold closed_sequential_limits, clarify)
-  fix f x assume "\<forall>n. f n \<in> S" and "f \<longlonglongrightarrow> x"
-  from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"
-    by (rule LIMSEQ_imp_Cauchy)
-  with \<open>complete S\<close> and \<open>\<forall>n. f n \<in> S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
-    by (rule completeE)
-  from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"
-    by (rule LIMSEQ_unique)
-  with \<open>l \<in> S\<close> show "x \<in> S"
-    by simp
-qed
+  shows "complete S \<Longrightarrow> closed S"
+  by (metis LIMSEQ_imp_Cauchy LIMSEQ_unique closed_sequential_limits completeE)
 
 lemma complete_Int_closed:
   fixes S :: "'a::metric_space set"
   assumes "complete S" and "closed t"
   shows "complete (S \<inter> t)"
-proof (rule completeI)
-  fix f assume "\<forall>n. f n \<in> S \<inter> t" and "Cauchy f"
-  then have "\<forall>n. f n \<in> S" and "\<forall>n. f n \<in> t"
-    by simp_all
-  from \<open>complete S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
-    using \<open>\<forall>n. f n \<in> S\<close> and \<open>Cauchy f\<close> by (rule completeE)
-  from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"
-    by (rule closed_sequentially)
-  with \<open>l \<in> S\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>S \<inter> t. f \<longlonglongrightarrow> l"
-    by fast
-qed
+  by (metis Int_iff assms closed_sequentially completeE completeI)
 
 lemma complete_closed_subset:
   fixes S :: "'a::metric_space set"
@@ -1845,8 +1734,7 @@
 lemma continuous_closed_imp_Cauchy_continuous:
   fixes S :: "('a::complete_space) set"
   shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
-  apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
-  by (meson LIMSEQ_imp_Cauchy complete_def)
+  by (meson LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially)
 
 lemma banach_fix_type:
   fixes f::"'a::complete_space\<Rightarrow>'a"
@@ -1866,15 +1754,13 @@
   assumes "closed S"
       and T: "T \<in> \<F>" "bounded T"
       and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
-      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
+      and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
     shows "S \<inter> \<Inter>\<F> \<noteq> {}"
 proof -
   have "compact (S \<inter> T)"
     using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast
   then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"
-    apply (rule compact_imp_fip)
-     apply (simp add: clof)
-    by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
+    by (smt (verit, best) Inf_insert Int_assoc assms compact_imp_fip finite_insert insert_subset)
   then show ?thesis by blast
 qed
 
@@ -1884,33 +1770,27 @@
    "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
      \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
         \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
-by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
+  by (metis closed_imp_fip compact_eq_bounded_closed equals0I finite.emptyI order.refl)
 
 lemma closed_fip_Heine_Borel:
   fixes \<F> :: "'a::heine_borel set set"
-  assumes "closed S" "T \<in> \<F>" "bounded T"
+  assumes "T \<in> \<F>" "bounded T"
       and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
       and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
     shows "\<Inter>\<F> \<noteq> {}"
-proof -
-  have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"
-    using assms closed_imp_fip [OF closed_UNIV] by auto
-  then show ?thesis by simp
-qed
+  using closed_imp_fip [OF closed_UNIV] assms by auto
 
 lemma compact_fip_Heine_Borel:
   fixes \<F> :: "'a::heine_borel set set"
   assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
       and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
     shows "\<Inter>\<F> \<noteq> {}"
-by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
+  by (metis InterI clof closed_fip_Heine_Borel compact_eq_bounded_closed equals0D none)
 
 lemma compact_sequence_with_limit:
   fixes f :: "nat \<Rightarrow> 'a::heine_borel"
-  shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"
-apply (simp add: compact_eq_bounded_closed, auto)
-apply (simp add: convergent_imp_bounded)
-by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
+  shows "f \<longlonglongrightarrow> l \<Longrightarrow> compact (insert l (range f))"
+  by (simp add: closed_limpt compact_eq_bounded_closed convergent_imp_bounded islimpt_insert sequence_unique_limpt)
 
 
 subsection \<open>Properties of Balls and Spheres\<close>
@@ -1918,21 +1798,18 @@
 lemma compact_cball[simp]:
   fixes x :: "'a::heine_borel"
   shows "compact (cball x e)"
-  using compact_eq_bounded_closed bounded_cball closed_cball
-  by blast
+  using compact_eq_bounded_closed bounded_cball closed_cball by blast
 
 lemma compact_frontier_bounded[intro]:
   fixes S :: "'a::heine_borel set"
   shows "bounded S \<Longrightarrow> compact (frontier S)"
   unfolding frontier_def
-  using compact_eq_bounded_closed
-  by blast
+  using compact_eq_bounded_closed by blast
 
 lemma compact_frontier[intro]:
   fixes S :: "'a::heine_borel set"
   shows "compact S \<Longrightarrow> compact (frontier S)"
-  using compact_eq_bounded_closed compact_frontier_bounded
-  by blast
+  using compact_eq_bounded_closed compact_frontier_bounded by blast
 
 
 subsection \<open>Distance from a Set\<close>
@@ -2054,9 +1931,7 @@
     with infdist_nonneg[of x A] have "infdist x A > 0"
       by auto
     then have "ball x (infdist x A) \<inter> closure A = {}"
-      apply auto
-      apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
-      done
+      by (smt (verit, best) \<open>x \<in> closure A\<close> closure_approachableD infdist_le)
     then have "x \<notin> closure A"
       by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
     then show False using \<open>x \<in> closure A\<close> by simp
@@ -2065,18 +1940,15 @@
   assume x: "infdist x A = 0"
   then obtain a where "a \<in> A"
     by atomize_elim (metis all_not_in_conv assms)
-  show "x \<in> closure A"
-    unfolding closure_approachable
-    apply safe
-  proof (rule ccontr)
-    fix e :: real
-    assume "e > 0"
-    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
-    then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
-      unfolding infdist_def
+  have False if "e > 0" "\<not> (\<exists>y\<in>A. dist y x < e)" for e
+  proof -
+    have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
+      unfolding infdist_def using that
       by (force simp: dist_commute intro: cINF_greatest)
     with x \<open>e > 0\<close> show False by auto
   qed
+  then show "x \<in> closure A"
+    using closure_approachable by blast
 qed
 
 lemma in_closed_iff_infdist_zero:
@@ -2084,14 +1956,14 @@
   shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
 proof -
   have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
-    by (rule in_closure_iff_infdist_zero) fact
+    by (simp add: \<open>A \<noteq> {}\<close> in_closure_iff_infdist_zero)
   with assms show ?thesis by simp
 qed
 
 lemma infdist_pos_not_in_closed:
   assumes "closed S" "S \<noteq> {}" "x \<notin> S"
   shows "infdist x S > 0"
-using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
+  by (smt (verit, best) assms in_closed_iff_infdist_zero infdist_nonneg)
 
 lemma
   infdist_attains_inf:
@@ -2103,10 +1975,9 @@
   have "bdd_below (dist y ` X)"
     by auto
   from distance_attains_inf[OF assms, of y]
-  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
-  have "infdist y X = dist y x"
-    by (auto simp: infdist_def assms
-      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+  obtain x where "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+  then have "infdist y X = dist y x"
+    by (metis antisym assms(2) cINF_greatest infdist_def infdist_le)
   with \<open>x \<in> X\<close> show ?thesis ..
 qed
 
@@ -2119,13 +1990,9 @@
   consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
   then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
   proof (cases)
-    case 1
-    show ?thesis
-      apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
+    case 1 then show ?thesis by blast
   next
-    case 2
-    show ?thesis
-      apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
+    case 2 then show ?thesis by blast
   next
     case 3
     define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
@@ -2154,7 +2021,7 @@
     then have E: "U \<inter> V = {}"
       unfolding U_def V_def by auto
     show ?thesis
-      apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
+      using A B C D E by blast
   qed
 qed
 
@@ -2218,57 +2085,42 @@
 subsection \<open>Separation between Points and Sets\<close>
 
 proposition separate_point_closed:
-  fixes s :: "'a::heine_borel set"
-  assumes "closed s" and "a \<notin> s"
-  shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
-proof (cases "s = {}")
-  case True
-  then show ?thesis by(auto intro!: exI[where x=1])
-next
-  case False
-  from assms obtain x where "x\<in>s" "\<forall>y\<in>s. dist a x \<le> dist a y"
-    using \<open>s \<noteq> {}\<close> by (blast intro: distance_attains_inf [of s a])
-  with \<open>x\<in>s\<close> show ?thesis using dist_pos_lt[of a x] and\<open>a \<notin> s\<close>
-    by blast
-qed
+  fixes S :: "'a::heine_borel set"
+  assumes "closed S" and "a \<notin> S"
+  shows "\<exists>d>0. \<forall>x\<in>S. d \<le> dist a x"
+  by (metis assms distance_attains_inf empty_iff gt_ex zero_less_dist_iff)
 
 proposition separate_compact_closed:
-  fixes s t :: "'a::heine_borel set"
-  assumes "compact s"
-    and t: "closed t" "s \<inter> t = {}"
-  shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
+  fixes S T :: "'a::heine_borel set"
+  assumes "compact S"
+    and T: "closed T" "S \<inter> T = {}"
+  shows "\<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>T. d \<le> dist x y"
 proof cases
-  assume "s \<noteq> {} \<and> t \<noteq> {}"
-  then have "s \<noteq> {}" "t \<noteq> {}" by auto
-  let ?inf = "\<lambda>x. infdist x t"
-  have "continuous_on s ?inf"
+  assume "S \<noteq> {} \<and> T \<noteq> {}"
+  then have "S \<noteq> {}" "T \<noteq> {}" by auto
+  let ?inf = "\<lambda>x. infdist x T"
+  have "continuous_on S ?inf"
     by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
-  then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
-    using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto
+  then obtain x where x: "x \<in> S" "\<forall>y\<in>S. ?inf x \<le> ?inf y"
+    using continuous_attains_inf[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close>] by auto
   then have "0 < ?inf x"
-    using t \<open>t \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
-  moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y"
+    using T \<open>T \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
+  moreover have "\<forall>x'\<in>S. \<forall>y\<in>T. ?inf x \<le> dist x' y"
     using x by (auto intro: order_trans infdist_le)
   ultimately show ?thesis by auto
 qed (auto intro!: exI[of _ 1])
 
 proposition separate_closed_compact:
-  fixes s t :: "'a::heine_borel set"
-  assumes "closed s"
-    and "compact t"
-    and "s \<inter> t = {}"
-  shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof -
-  have *: "t \<inter> s = {}"
-    using assms(3) by auto
-  show ?thesis
-    using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
-qed
+  fixes S T :: "'a::heine_borel set"
+  assumes S: "closed S"
+    and T: "compact T"
+    and dis: "S \<inter> T = {}"
+  shows "\<exists>d>0. \<forall>x\<in>S. \<forall>y\<in>T. d \<le> dist x y"
+  by (metis separate_compact_closed[OF T S] dis dist_commute inf_commute)
 
 proposition compact_in_open_separated:
   fixes A::"'a::heine_borel set"
-  assumes "A \<noteq> {}"
-  assumes "compact A"
+  assumes A: "A \<noteq> {}" "compact A"
   assumes "open B"
   assumes "A \<subseteq> B"
   obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
@@ -2287,13 +2139,8 @@
     assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
     with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
       by auto
-    from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
-    from infdist_attains_inf[OF this]
-    obtain y where y: "y \<in> A" "infdist x A = dist x y"
-      by auto
-    have "dist x y \<le> d" using x y by simp
-    also have "\<dots> < dist x y" using y d x by auto
-    finally show False by simp
+    then show False
+      by (metis A compact_eq_bounded_closed infdist_attains_inf x d linorder_not_less)
   qed
 qed
 
@@ -2303,8 +2150,8 @@
 lemma uniformly_continuous_onE:
   assumes "uniformly_continuous_on s f" "0 < e"
   obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
-using assms
-by (auto simp: uniformly_continuous_on_def)
+  using assms
+  by (auto simp: uniformly_continuous_on_def)
 
 lemma uniformly_continuous_on_sequentially:
   "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
@@ -2320,20 +2167,11 @@
       fix e :: real
       assume "e > 0"
       then obtain d where "d > 0" and d: "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
-        using \<open>?lhs\<close>[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
+        by (metis \<open>?lhs\<close> uniformly_continuous_onE)
       obtain N where N: "\<forall>n\<ge>N. dist (x n) (y n) < d"
         using xy[unfolded lim_sequentially dist_norm] and \<open>d>0\<close> by auto
-      {
-        fix n
-        assume "n\<ge>N"
-        then have "dist (f (x n)) (f (y n)) < e"
-          using N[THEN spec[where x=n]]
-          using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]]
-          using x and y
-          by (simp add: dist_commute)
-      }
       then have "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
-        by auto
+        using d x y by blast
     }
     then have "((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially"
       unfolding lim_sequentially and dist_real_def by auto
@@ -2348,8 +2186,7 @@
     then obtain fa where fa:
       "\<forall>x. 0 < x \<longrightarrow> fst (fa x) \<in> s \<and> snd (fa x) \<in> s \<and> dist (fst (fa x)) (snd (fa x)) < x \<and> \<not> dist (f (fst (fa x))) (f (snd (fa x))) < e"
       using choice[of "\<lambda>d x. d>0 \<longrightarrow> fst x \<in> s \<and> snd x \<in> s \<and> dist (snd x) (fst x) < d \<and> \<not> dist (f (snd x)) (f (fst x)) < e"]
-      unfolding Bex_def
-      by (auto simp: dist_commute)
+      by (auto simp: Bex_def dist_commute)
     define x where "x n = fst (fa (inverse (real n + 1)))" for n
     define y where "y n = snd (fa (inverse (real n + 1)))" for n
     have xyn: "\<forall>n. x n \<in> s \<and> y n \<in> s"
@@ -2362,17 +2199,8 @@
       assume "e > 0"
       then obtain N :: nat where "N \<noteq> 0" and N: "0 < inverse (real N) \<and> inverse (real N) < e"
         unfolding real_arch_inverse[of e] by auto
-      {
-        fix n :: nat
-        assume "n \<ge> N"
-        then have "inverse (real n + 1) < inverse (real N)"
-          using of_nat_0_le_iff and \<open>N\<noteq>0\<close> by auto
-        also have "\<dots> < e" using N by auto
-        finally have "inverse (real n + 1) < e" by auto
-        then have "dist (x n) (y n) < e"
-          using xy0[THEN spec[where x=n]] by auto
-      }
-      then have "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto
+      then have "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e"
+        by (smt (verit, ccfv_SIG) inverse_le_imp_le nat_le_real_less of_nat_le_0_iff xy0) 
     }
     then have "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
       using \<open>?rhs\<close>[THEN spec[where x=x], THEN spec[where x=y]] and xyn
@@ -2415,8 +2243,7 @@
     then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))"
       by simp
     also have "... \<le> 1 / real (Suc (max N1 N2))"
-      apply (simp add: field_split_simps del: max.bounded_iff)
-      using \<open>strict_mono r\<close> seq_suble by blast
+      by (meson Suc_le_mono \<open>strict_mono r\<close> inverse_of_nat_le nat.discI seq_suble)
     also have "... \<le> 1 / real (Suc N2)"
       by (simp add: field_simps)
     also have "... < e/2"
@@ -2447,7 +2274,7 @@
     using cont by metis
   let ?\<G> = "((\<lambda>x. ball x (d x (e/2))) ` S)"
   have Ssub: "S \<subseteq> \<Union> ?\<G>"
-    by clarsimp (metis d_pos \<open>0 < e\<close> dist_self half_gt_zero_iff)
+    using \<open>0 < e\<close> d_pos by auto
   then obtain k where "0 < k" and k: "\<And>x. x \<in> S \<Longrightarrow> \<exists>G \<in> ?\<G>. ball x k \<subseteq> G"
     by (rule Heine_Borel_lemma [OF \<open>compact S\<close>]) auto
   moreover have "dist (f v) (f u) < e" if "f \<in> \<F>" "u \<in> S" "v \<in> S" "dist v u < k" for f u v
@@ -2637,10 +2464,7 @@
   from uc have cont_f: "continuous_on X f"
     by (simp add: uniformly_continuous_imp_continuous)
   obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
-    apply atomize_elim
-    apply (rule choice)
-    using uniformly_continuous_on_extension_at_closure[OF assms]
-    by metis
+    using uniformly_continuous_on_extension_at_closure[OF assms] by meson
   let ?g = "\<lambda>x. if x \<in> X then f x else y x"
 
   have "uniformly_continuous_on (closure X) ?g"
@@ -2733,14 +2557,11 @@
 proof
   assume ?lhs
   then show ?rhs
-    apply (simp add: openin_open)
-    apply (metis Int_commute Int_mono inf.cobounded2 open_contains_ball order_refl subsetCE)
-    done
+    by (metis IntD2 Int_commute Int_lower1 Int_mono inf.idem openE openin_open)
 next
   assume ?rhs
   then show ?lhs
-    apply (simp add: openin_euclidean_subtopology_iff)
-    by (metis (no_types) Int_iff dist_commute inf.absorb_iff2 mem_ball)
+    by (smt (verit) open_ball Int_commute Int_iff centre_in_ball in_mono openin_open_Int openin_subopen)
 qed
 
 lemma openin_contains_cball:
@@ -2804,11 +2625,8 @@
           "\<And>e. e>0 \<Longrightarrow> \<exists>n. \<forall>x\<in>S n. \<forall>y\<in>S n. dist x y < e"
   obtains a where "\<And>n. a \<in> S n"
 proof -
-  have "\<forall>n. \<exists>x. x \<in> S n"
-    using assms(2) by auto
-  then have "\<exists>t. \<forall>n. t n \<in> S n"
-    using choice[of "\<lambda>n x. x \<in> S n"] by auto
-  then obtain t where t: "\<forall>n. t n \<in> S n" by auto
+  obtain t where t: "\<forall>n. t n \<in> S n"
+    by (meson assms(2) equals0I)
   {
     fix e :: real
     assume "e > 0"
@@ -3012,15 +2830,7 @@
 lemma continuous_at_real_range:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
   shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
-  unfolding continuous_at
-  unfolding Lim_at
-  unfolding dist_norm
-  apply auto
-  apply (erule_tac x=e in allE, auto)
-  apply (rule_tac x=d in exI, auto)
-  apply (erule_tac x=x' in allE, auto)
-  apply (erule_tac x=e in allE, auto)
-  done
+  by (metis (mono_tags, opaque_lifting) LIM_eq continuous_within norm_eq_zero real_norm_def right_minus_eq)
 
 lemma continuous_on_real_range:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real"
@@ -3091,12 +2901,7 @@
 lemma le_setdist_iff:
         "d \<le> setdist S T \<longleftrightarrow>
         (\<forall>x \<in> S. \<forall>y \<in> T. d \<le> dist x y) \<and> (S = {} \<or> T = {} \<longrightarrow> d \<le> 0)"
-  apply (cases "S = {} \<or> T = {}")
-  apply (force simp add: setdist_def)
-  apply (intro iffI conjI)
-  using setdist_le_dist apply fastforce
-  apply (auto simp: intro: le_setdistI)
-  done
+  by (smt (verit) le_setdistI setdist_def setdist_le_dist)
 
 lemma setdist_ltE:
   assumes "setdist S T < b" "S \<noteq> {}" "T \<noteq> {}"
@@ -3105,11 +2910,7 @@
 by (auto simp: not_le [symmetric] le_setdist_iff)
 
 lemma setdist_refl: "setdist S S = 0"
-  apply (cases "S = {}")
-  apply (force simp add: setdist_def)
-  apply (rule antisym [OF _ setdist_pos_le])
-  apply (metis all_not_in_conv dist_self setdist_le_dist)
-  done
+  by (metis dist_eq_0_iff ex_in_conv order_antisym setdist_def setdist_le_dist setdist_pos_le)
 
 lemma setdist_sym: "setdist S T = setdist T S"
   by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
@@ -3121,10 +2922,8 @@
 next
   case False
   then have "\<And>x. x \<in> S \<Longrightarrow> setdist S T - dist x a \<le> setdist {a} T"
-    apply (intro le_setdistI)
-    apply (simp_all add: algebra_simps)
-    apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
-    done
+    using  dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff
+    by (smt (verit, best) dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff)
   then have "setdist S T - setdist {a} T \<le> setdist S {a}"
     using False by (fastforce intro: le_setdistI)
   then show ?thesis
@@ -3148,9 +2947,7 @@
   by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
 
 lemma setdist_subset_right: "\<lbrakk>T \<noteq> {}; T \<subseteq> u\<rbrakk> \<Longrightarrow> setdist S u \<le> setdist S T"
-  apply (cases "S = {} \<or> u = {}", force)
-  apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
-  done
+  by (smt (verit, best) in_mono le_setdist_iff)
 
 lemma setdist_subset_left: "\<lbrakk>S \<noteq> {}; S \<subseteq> T\<rbrakk> \<Longrightarrow> setdist T u \<le> setdist S u"
   by (metis setdist_subset_right setdist_sym)
@@ -3166,12 +2963,9 @@
       by (auto simp: continuous_intros dist_norm)
     then have *: "\<And>x. x \<in> closure S \<Longrightarrow> setdist S T \<le> dist x y"
       by (fast intro: setdist_le_dist \<open>y \<in> T\<close> continuous_ge_on_closure)
-  } note * = this
+  } then
   show ?thesis
-    apply (rule antisym)
-     using False closure_subset apply (blast intro: setdist_subset_left)
-    using False * apply (force intro!: le_setdistI)
-    done
+    by (metis False antisym closure_eq_empty closure_subset le_setdist_iff setdist_subset_left)
 qed
 
 lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S"
@@ -3199,14 +2993,13 @@
     have "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> Inf (dist x ` B)"
       if  "b \<in> B" "a \<in> A" "x \<in> A" for x 
     proof -
-      have *: "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"
+      have "\<And>b'. b' \<in> B \<Longrightarrow> Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> dist x b'"
         by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))
-      show ?thesis
-        using that by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: *)+
+      then show ?thesis
+        by (smt (verit) cINF_greatest ex_in_conv \<open>b \<in> B\<close>)
     qed
     then show "Inf {dist x y |x y. x \<in> A \<and> y \<in> B} \<le> (INF x\<in>A. Inf (dist x ` B))"
-      using that
-      by (subst conditionally_complete_lattice_class.le_cInf_iff) (auto simp: bdd_below_def)
+      by (metis (mono_tags, lifting) cINF_greatest emptyE that)
   next
     have *: "\<And>x y. \<lbrakk>b \<in> B; a \<in> A; x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>a\<in>A. Inf (dist a ` B) \<le> dist x y"
       by (meson bdd_below_image_dist cINF_lower)
@@ -3225,8 +3018,7 @@
   shows "infdist x B \<le> infdist x A"
   by (simp add: assms infdist_eq_setdist setdist_subset_right)
 
-lemma infdist_singleton [simp]:
-  "infdist x {y} = dist x y"
+lemma infdist_singleton [simp]: "infdist x {y} = dist x y"
   by (simp add: infdist_eq_setdist)
 
 proposition setdist_attains_inf:
@@ -3247,12 +3039,7 @@
     also have "\<dots> = infdist y A"
     proof (rule order_antisym)
       show "(INF y\<in>B. infdist y A) \<le> infdist y A"
-      proof (rule cInf_lower)
-        show "infdist y A \<in> (\<lambda>y. infdist y A) ` B"
-          using \<open>y \<in> B\<close> by blast
-        show "bdd_below ((\<lambda>y. infdist y A) ` B)"
-          by (meson bdd_belowI2 infdist_nonneg)
-      qed
+        by (meson \<open>y \<in> B\<close> bdd_belowI2 cInf_lower image_eqI infdist_nonneg)
     next
       show "infdist y A \<le> (INF y\<in>B. infdist y A)"
         by (simp add: \<open>B \<noteq> {}\<close> cINF_greatest min)
diff -r 04af11e6557a -r 18e719c6b633 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Dec 27 22:52:28 2022 +0100
+++ b/src/HOL/Library/Float.thy	Wed Dec 28 12:15:25 2022 +0000
@@ -100,22 +100,11 @@
 qed
 
 lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
-  apply (auto simp: float_def)
-  apply hypsubst_thin
-  apply (rename_tac m e)
-  apply (rule_tac x="-m" in exI)
-  apply (rule_tac x="e" in exI)
-  apply (simp add: field_simps)
-  done
+  by (simp add: float_def) (metis mult_minus_left of_int_minus)
 
 lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
-  apply (auto simp: float_def)
-  apply hypsubst_thin
-  apply (rename_tac mx my ex ey)
-  apply (rule_tac x="mx * my" in exI)
-  apply (rule_tac x="ex + ey" in exI)
-  apply (simp add: powr_add)
-  done
+  apply (clarsimp simp: float_def)
+  by (metis (no_types, opaque_lifting) of_int_add powr_add mult.assoc mult.left_commute of_int_mult)
 
 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
   using plus_float [of x "- y"] by simp
@@ -126,23 +115,11 @@
 lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
   by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)
 
-lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
-  apply (auto simp add: float_def)
-  apply hypsubst_thin
-  apply (rename_tac m e)
-  apply (rule_tac x="m" in exI)
-  apply (rule_tac x="e - d" in exI)
-  apply (simp flip: powr_realpow powr_add add: field_simps)
-  done
+lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float" 
+  by (simp add: float_def) (metis of_int_diff of_int_of_nat_eq powr_diff powr_realpow zero_less_numeral times_divide_eq_right)
 
 lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
-  apply (auto simp add: float_def)
-  apply hypsubst_thin
-  apply (rename_tac m e)
-  apply (rule_tac x="m" in exI)
-  apply (rule_tac x="e - d" in exI)
-  apply (simp flip: powr_realpow powr_add add: field_simps)
-  done
+  by simp
 
 lemma div_numeral_Bit0_float[simp]:
   assumes "x / numeral n \<in> float"
@@ -158,13 +135,7 @@
 lemma div_neg_numeral_Bit0_float[simp]:
   assumes "x / numeral n \<in> float"
   shows "x / (- numeral (Num.Bit0 n)) \<in> float"
-proof -
-  have "- (x / numeral (Num.Bit0 n)) \<in> float"
-    using assms by simp
-  also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
-    by simp
-  finally show ?thesis .
-qed
+  using assms by force
 
 lemma power_float[simp]:
   assumes "a \<in> float"
@@ -251,15 +222,9 @@
 proof
   fix a b :: float
   show "\<exists>c. a < c"
-    apply (intro exI[of _ "a + 1"])
-    apply transfer
-    apply simp
-    done
+    by (metis Float.real_of_float less_float.rep_eq reals_Archimedean2)
   show "\<exists>c. c < a"
-    apply (intro exI[of _ "a - 1"])
-    apply transfer
-    apply simp
-    done
+    by (metis add_0 add_strict_right_mono neg_less_0_iff_less zero_less_one)
   show "\<exists>c. a < c \<and> c < b" if "a < b"
     apply (rule exI[of _ "(a + b) * Float 1 (- 1)"])
     using that
@@ -283,11 +248,10 @@
 end
 
 lemma float_numeral[simp]: "real_of_float (numeral x :: float) = numeral x"
-  apply (induct x)
-  apply simp
-  apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq float_of_inverse
-          plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
-  done
+proof (induct x)
+  case One
+  then show ?case by simp
+qed (metis of_int_numeral real_of_float_of_int_eq)+
 
 lemma transfer_numeral [transfer_rule]:
   "rel_fun (=) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
@@ -837,11 +801,11 @@
   finally show ?thesis
     using \<open>p + e < 0\<close>
     apply transfer
-    apply (simp add: round_down_def field_simps flip: floor_divide_of_int_eq)
+    apply (simp add: round_down_def field_simps flip: floor_divide_of_int_eq powr_add)
     apply (metis (no_types, opaque_lifting) Float.rep_eq
       add.inverse_inverse compute_real_of_float diff_minus_eq_add
       floor_divide_of_int_eq int_of_reals(1) linorder_not_le
-      minus_add_distrib of_int_eq_numeral_power_cancel_iff powr_add)
+      minus_add_distrib of_int_eq_numeral_power_cancel_iff )
     done
 next
   case False
@@ -885,10 +849,7 @@
     have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
       by simp
     moreover have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<noteq> real_of_int a / real_of_int b"
-      apply (subst (2) real_of_int_div_aux)
-      unfolding floor_divide_of_int_eq
-      using ne \<open>b \<noteq> 0\<close> apply auto
-      done
+      by (smt (verit) floor_divide_of_int_eq ne real_of_int_div_aux)
     ultimately show "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> < real_of_int a / real_of_int b" by arith
   qed
   then show ?thesis
@@ -1254,12 +1215,7 @@
   by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)
 
 lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
-  apply (cases "0 \<le> x")
-  apply (rule truncate_down_nonneg_mono, assumption+)
-  apply (simp add: truncate_down_eq_truncate_up)
-  apply (cases "0 \<le> y")
-  apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
-  done
+  by (smt (verit) truncate_down_nonneg_mono truncate_up_nonneg_mono truncate_up_uminus_eq)
 
 lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
   by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
@@ -1271,22 +1227,7 @@
   by (meson less_le_trans that truncate_up)
 
 lemma truncate_up_less_zero_iff[simp]: "truncate_up p x < 0 \<longleftrightarrow> x < 0"
-proof -
-  have f1: "\<forall>n r. truncate_up n r + truncate_down n (- 1 * r) = 0"
-    by (simp add: truncate_down_uminus_eq)
-  have f2: "(\<forall>v0 v1. truncate_up v0 v1 + truncate_down v0 (- 1 * v1) = 0) = (\<forall>v0 v1. truncate_up v0 v1 = - 1 * truncate_down v0 (- 1 * v1))"
-    by (auto simp: truncate_up_eq_truncate_down)
-  have f3: "\<forall>x1. ((0::real) < x1) = (\<not> x1 \<le> 0)"
-    by fastforce
-  have "(- 1 * x \<le> 0) = (0 \<le> x)"
-    by force
-  then have "0 \<le> x \<or> \<not> truncate_down p (- 1 * x) \<le> 0"
-    using f3 by (meson truncate_down_pos)
-  then have "(0 \<le> truncate_up p x) \<noteq> (\<not> 0 \<le> x)"
-    using f2 f1 truncate_up_nonneg by force
-  then show ?thesis
-    by linarith
-qed
+  by (smt (verit) truncate_down_pos truncate_down_uminus_eq truncate_up_nonneg)
 
 lemma truncate_up_nonneg_iff[simp]: "truncate_up p x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
   using truncate_up_less_zero_iff[of p x] truncate_up_nonneg[of x]
@@ -1913,7 +1854,6 @@
   by (meson dual_order.trans mult_left_mono_neg mult_right_mono_neg that)
 
 lemma mult_float_mono1:
-  notes mono_rules = plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
   shows "a \<le> b \<Longrightarrow> ab \<le> bb \<Longrightarrow>
        aa \<le> a \<Longrightarrow>
        b \<le> ba \<Longrightarrow>
@@ -1927,20 +1867,10 @@
            (plus_down prec (nprt b * nprt bb)
              (plus_down prec (pprt a * pprt ab)
                (pprt b * nprt ab)))"
-  apply (rule order_trans)
-   apply (rule mono_rules | assumption)+
-    apply (rule mult_mono_nonpos_nonneg)
-       apply (rule mono_rules | assumption)+
-    apply (rule mult_mono_nonpos_nonpos)
-       apply (rule mono_rules | assumption)+
-    apply (rule mult_mono)
-       apply (rule mono_rules | assumption)+
-   apply (rule mult_mono_nonneg_nonpos)
-      apply (rule mono_rules | assumption)+
-  by (rule order_refl)+
+  by (smt (verit, del_insts) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt 
+pprt_mono mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
 
 lemma mult_float_mono2:
-  notes mono_rules = plus_up_mono add_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
   shows "a \<le> b \<Longrightarrow>
        ab \<le> bb \<Longrightarrow>
        aa \<le> a \<Longrightarrow>
@@ -1955,17 +1885,8 @@
            (plus_up prec (pprt aa * nprt bc)
              (plus_up prec (nprt ba * pprt ac)
                (nprt aa * nprt ac)))"
-  apply (rule order_trans)
-   apply (rule mono_rules | assumption)+
-    apply (rule mult_mono)
-       apply (rule mono_rules | assumption)+
-    apply (rule mult_mono_nonneg_nonpos)
-       apply (rule mono_rules | assumption)+
-    apply (rule mult_mono_nonpos_nonneg)
-       apply (rule mono_rules | assumption)+
-   apply (rule mult_mono_nonpos_nonpos)
-      apply (rule mono_rules | assumption)+
-  by (rule order_refl)+
+  by (smt (verit, del_insts) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono 
+      mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
 
 
 subsection \<open>Approximate Power\<close>
@@ -2132,24 +2053,21 @@
       assume [simp]: "odd j"
       have "power_down prec 0 (Suc (j div 2)) \<le> - power_down prec b (Suc (j div 2))"
         if "b < 0" "even (j div 2)"
-        apply (rule order_trans[where y=0])
-        using IH that by (auto simp: div2_less_self)
+        by (metis even_Suc le_minus_iff Suc_neq_Zero neg_equal_zero power_down_eq_zero_iff
+              power_down_nonpos_iff that)
       then have "truncate_down (Suc prec) ((power_down prec a (Suc (j div 2)))\<^sup>2)
         \<le> truncate_down (Suc prec) ((power_down prec b (Suc (j div 2)))\<^sup>2)"
-        using IH
-        by (auto intro!: truncate_down_mono intro: order_trans[where y=0]
-            simp: abs_le_square_iff[symmetric] abs_real_def
-            div2_less_self)
+        by (smt (verit) IH Suc_less_eq \<open>odd j\<close> div2_less_self mult_mono_nonpos_nonpos 
+            Suc_neq_Zero power2_eq_square power_down_neg_iff power_down_nonpos_iff power_mono truncate_down_mono)
       then show ?thesis
-        unfolding j
-        by (simp add: power_down_simp)
+        unfolding j by (simp add: power_down_simp)
     qed
   qed simp
 qed
 
 lemma power_up_even_nonneg: "even n \<Longrightarrow> 0 \<le> power_up p x n"
   by (induct p x n rule: power_up.induct)
-    (auto simp: power_up.simps simp del: odd_Suc_div_two intro!: )
+    (auto simp: power_up.simps simp del: odd_Suc_div_two)
 
 lemma power_up_eq_zero_iff[simp]: "power_up prec b n = 0 \<longleftrightarrow> b = 0 \<and> n \<noteq> 0"
 proof (induction n arbitrary: b rule: less_induct)
@@ -2253,18 +2171,7 @@
   fixes a b :: int
   assumes "b > 0"
   shows "a \<ge> b * (a div b)"
-proof -
-  from minus_div_mult_eq_mod [symmetric, of a b] have "a = b * (a div b) + a mod b"
-    by simp
-  also have "\<dots> \<ge> b * (a div b) + 0"
-    apply (rule add_left_mono)
-    apply (rule pos_mod_sign)
-    using assms
-    apply simp
-    done
-  finally show ?thesis
-    by simp
-qed
+  by (smt (verit, ccfv_threshold) assms minus_div_mult_eq_mod mod_int_pos_iff mult.commute)
 
 lemma lapprox_rat_nonneg:
   assumes "0 \<le> x" and "0 \<le> y"
@@ -2393,9 +2300,8 @@
 qualified lemma compute_int_floor_fl[code]:
   "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   apply transfer
-  apply (simp add: powr_int floor_divide_of_int_eq)
-  apply (metis (no_types, opaque_lifting)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
-  done
+  by (smt (verit, ccfv_threshold) Float.rep_eq compute_real_of_float floor_divide_of_int_eq 
+      floor_of_int of_int_1 of_int_add of_int_mult of_int_power)
 
 lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real_of_int \<lfloor>x\<rfloor>"
   by simp
@@ -2404,8 +2310,7 @@
   "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   apply transfer
   apply (simp add: powr_int floor_divide_of_int_eq)
-  apply (metis (no_types, opaque_lifting)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
-  done
+  by (smt (z3) floor_divide_of_int_eq of_int_1 of_int_add of_int_power)
 
 end