# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672442497 0
# Node ID 4645ca4457db53ea5b61ed32bc9074e1caea60e6
# Parent  6be3459fc4c1c26ca97071ab562ef778cf07e177
Continued proof simplifications

diff -r 6be3459fc4c1 -r 4645ca4457db src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Dec 30 20:59:38 2022 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Dec 30 23:21:37 2022 +0000
@@ -1586,7 +1586,7 @@
 qed
 
 lemma
-  shows space_measure_of_conv [simp]: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
+  shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
   and sets_measure_of_conv:
   "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
   and emeasure_measure_of_conv:
diff -r 6be3459fc4c1 -r 4645ca4457db src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Fri Dec 30 20:59:38 2022 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Dec 30 23:21:37 2022 +0000
@@ -300,15 +300,15 @@
       done
   }
   ultimately show ?l
-    unfolding division_of_def cbox_sing by auto
+    unfolding division_of_def cbox_idem by auto
 next
   assume ?l
   have "x = {a}" if  "x \<in> s" for x
-    by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
+    by (metis \<open>s division_of cbox a a\<close> cbox_idem division_ofD(2) division_ofD(3) subset_singletonD that)
   moreover have "s \<noteq> {}"
     using \<open>s division_of cbox a a\<close> by auto
   ultimately show ?r
-    unfolding cbox_sing by auto
+    unfolding cbox_idem by auto
 qed
 
 lemma elementary_empty: obtains p where "p division_of {}"
@@ -2316,7 +2316,7 @@
     "S \<subseteq> \<Union>\<D>"
 proof -
   have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
-    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
+    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_idem by fastforce+
   let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
                     cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
                          (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
diff -r 6be3459fc4c1 -r 4645ca4457db src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Dec 30 20:59:38 2022 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Dec 30 23:21:37 2022 +0000
@@ -127,12 +127,10 @@
         by (force simp: SOME_Basis dist_norm)
     next
       case False
-      have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
-        by (simp add: algebra_simps)
-      also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
+      have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
         by (simp add: algebra_simps)
       also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
-        by simp (simp add: field_simps)
+        by (simp add: divide_simps)
       finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>"
         by linarith
       from \<open>a \<noteq> a'\<close> show ?thesis
@@ -167,8 +165,7 @@
       have False if "norm (a - a') + r \<ge> r'"
       proof -
         from that have "\<bar>r' - norm (a - a')\<bar> \<le> r"
-          by (simp split: abs_split)
-            (metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
+          by (smt (verit, best) \<open>0 \<le> r\<close> \<open>?lhs\<close> ball_subset_cball cball_subset_cball_iff dist_norm order_trans)
         then show ?thesis
           using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
           apply (simp add: dist_norm)
@@ -222,8 +219,8 @@
     assume ?lhs
     then have "0 < r'"
       using False by metric
-    then have "(cball a r \<subseteq> cball a' r')"
-      by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
+    then have "cball a r \<subseteq> cball a' r'"
+      by (metis False \<open>?lhs\<close> closure_ball closure_mono not_less)
     then show ?rhs
       using False cball_subset_cball_iff by fastforce
   qed metric
@@ -233,65 +230,17 @@
 lemma ball_eq_ball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
-        (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-  proof (cases "d \<le> 0 \<or> e \<le> 0")
-    case True
-      with \<open>?lhs\<close> show ?rhs
-        by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
-  next
-    case False
-    with \<open>?lhs\<close> show ?rhs
-      apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
-      apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
-      apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
-      done
-  qed
-next
-  assume ?rhs then show ?lhs
-    by (auto simp: set_eq_subset ball_subset_ball_iff)
-qed
+  by (smt (verit, del_insts) ball_empty ball_subset_cball_iff dist_norm norm_pths(2))
 
 lemma cball_eq_cball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
-        (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-  proof (cases "d < 0 \<or> e < 0")
-    case True
-      with \<open>?lhs\<close> show ?rhs
-        by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
-  next
-    case False
-    with \<open>?lhs\<close> show ?rhs
-      apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
-      apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
-      apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
-      done
-  qed
-next
-  assume ?rhs then show ?lhs
-    by (auto simp: set_eq_subset cball_subset_cball_iff)
-qed
+  by (smt (verit, ccfv_SIG) cball_empty cball_subset_cball_iff dist_norm norm_pths(2) zero_le_dist)
 
 lemma ball_eq_cball_iff:
   fixes x :: "'a :: euclidean_space"
   shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
-    apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
-    apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
-    using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
-    done
-next
-  assume ?rhs then show ?lhs by auto
-qed
+  by (smt (verit) ball_eq_empty ball_subset_cball_iff cball_eq_empty cball_subset_ball_iff order.refl)
 
 lemma cball_eq_ball_iff:
   fixes x :: "'a :: euclidean_space"
@@ -308,9 +257,8 @@
   obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
     using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
   hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" using e1_b by auto
-  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" using \<open>e2>0\<close> \<open>e1>0\<close>
-    apply (rule_tac x="min e1 e2" in exI)
-    by auto
+  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> S \<and> (w \<noteq> p \<longrightarrow> w \<notin> X)" 
+    using \<open>e2>0\<close> \<open>e1>0\<close> by (rule_tac x="min e1 e2" in exI) auto
 qed
 
 lemma finite_cball_avoid:
@@ -391,9 +339,7 @@
   by (force simp: cbox_Pair_eq)
 
 lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
-  apply (auto simp: cbox_def Basis_complex_def)
-  apply (rule_tac x = "(Re x, Im x)" in image_eqI)
-  using complex_eq by auto
+  by (force simp: cbox_def Basis_complex_def)
 
 lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
   by (force simp: cbox_Pair_eq)
@@ -425,22 +371,14 @@
   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   then have e: "e' > 0"
     using assms by (auto)
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i
-    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] obtain a where
-    a: "\<forall>xa. a xa \<in> \<rat> \<and> a xa < x \<bullet> xa \<and> x \<bullet> xa - a xa < e'" ..
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i
-    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] obtain b where
-    b: "\<forall>xa. b xa \<in> \<rat> \<and> x \<bullet> xa < b xa \<and> b xa - x \<bullet> xa < e'" ..
+  have "\<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" for i
+    using Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e by force
+  then obtain a where
+    a: "\<And>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" by metis
+  have "\<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" for i
+    using Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e by force
+  then obtain b where
+    b: "\<And>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" by metis
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
@@ -454,10 +392,8 @@
       assume i: "i \<in> Basis"
       have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
         using * i by (auto simp: box_def)
-      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
-        using a by auto
-      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
-        using b by auto
+      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
+        using a b by auto
       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
         by auto
       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
@@ -471,7 +407,7 @@
       using \<open>0 < e\<close> by simp
     finally show "y \<in> ball x e"
       by (auto simp: ball_def)
-  qed (insert a b, auto simp: box_def)
+  qed (use a b in \<open>auto simp: box_def\<close>)
 qed
 
 lemma open_UNION_box:
@@ -527,22 +463,14 @@
   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   then have e: "e' > 0"
     using assms by auto
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i
-    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] obtain a where
-    a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" ..
-  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
-  proof
-    fix i
-    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
-    show "?th i" by auto
-  qed
-  from choice[OF this] obtain b where
-    b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" ..
+  have "\<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" for i
+    using Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e by force
+  then obtain a where
+    a: "\<forall>u. a u \<in> \<rat> \<and> a u < x \<bullet> u \<and> x \<bullet> u - a u < e'" by metis
+  have "\<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" for i
+    using Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e by force
+  then obtain b where
+    b: "\<forall>u. b u \<in> \<rat> \<and> x \<bullet> u < b u \<and> b u - x \<bullet> u < e'" by metis
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
@@ -556,10 +484,8 @@
       assume i: "i \<in> Basis"
       have "a i \<le> y\<bullet>i \<and> y\<bullet>i \<le> b i"
         using * i by (auto simp: cbox_def)
-      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
-        using a by auto
-      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
-        using b by auto
+      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
+        using a b by auto
       ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
         by auto
       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
@@ -626,54 +552,28 @@
   shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
     and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
 proof -
-  {
-    fix i x
-    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
-    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
-      unfolding mem_box by (auto simp: box_def)
-    then have "a\<bullet>i < b\<bullet>i" by auto
-    then have False using as by auto
-  }
+  have False if "i \<in> Basis" and "b\<bullet>i \<le> a\<bullet>i" and "x \<in> box a b" for i x
+    by (smt (verit, ccfv_SIG) mem_box(1) that)
   moreover
-  {
-    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
+  { assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
     let ?x = "(1/2) *\<^sub>R (a + b)"
-    {
-      fix i :: 'a
+    { fix i :: 'a
       assume i: "i \<in> Basis"
       have "a\<bullet>i < b\<bullet>i"
-        using as[THEN bspec[where x=i]] i by auto
+        using as i by fastforce
       then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
         by (auto simp: inner_add_left)
     }
     then have "box a b \<noteq> {}"
-      using mem_box(1)[of "?x" a b] by auto
+      by (metis (no_types, opaque_lifting) emptyE mem_box(1))
   }
   ultimately show ?th1 by blast
 
-  {
-    fix i x
-    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
-    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
-      unfolding mem_box by auto
-    then have "a\<bullet>i \<le> b\<bullet>i" by auto
-    then have False using as by auto
-  }
+  have False if "i\<in>Basis" and "b\<bullet>i < a\<bullet>i" and "x \<in> cbox a b" for i x
+    using mem_box(2) that by force
   moreover
-  {
-    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
-    let ?x = "(1/2) *\<^sub>R (a + b)"
-    {
-      fix i :: 'a
-      assume i:"i \<in> Basis"
-      have "a\<bullet>i \<le> b\<bullet>i"
-        using as[THEN bspec[where x=i]] i by auto
-      then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
-        by (auto simp: inner_add_left)
-    }
-    then have "cbox a b \<noteq> {}"
-      using mem_box(2)[of "?x" a b] by auto
-  }
+  have "cbox a b \<noteq> {}" if "\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
+    by (metis emptyE linorder_linear mem_box(2) order.strict_iff_not that)
   ultimately show ?th2 by blast
 qed
 
@@ -685,11 +585,9 @@
 
 lemma
   fixes a :: "'a::euclidean_space"
-  shows cbox_sing [simp]: "cbox a a = {a}"
-    and box_sing [simp]: "box a a = {}"
-  unfolding set_eq_iff mem_box eq_iff [symmetric]
-  by (auto intro!: euclidean_eqI[where 'a='a])
-     (metis all_not_in_conv nonempty_Basis)
+  shows cbox_idem [simp]: "cbox a a = {a}"
+    and box_idem [simp]: "box a a = {}"
+  unfolding set_eq_iff mem_box eq_iff [symmetric] using euclidean_eq_iff by fastforce+
 
 lemma subset_box_imp:
   fixes a :: "'a::euclidean_space"
@@ -765,11 +663,7 @@
     by auto
   then show ?rhs
     by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
-next
-  assume ?rhs
-  then show ?lhs
-    by force
-qed
+qed auto
 
 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -777,10 +671,8 @@
   assume L: ?lhs
   then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
     by auto
-  then show ?rhs
-    apply (simp add: subset_box)
-    using L box_ne_empty box_sing apply (fastforce simp add:)
-    done
+  with L subset_box show ?rhs
+    by (smt (verit) SOME_Basis box_ne_empty(1))
 qed force
 
 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
@@ -793,11 +685,7 @@
   then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
     by auto
   then show ?rhs
-    apply (simp add: subset_box)
-    using box_ne_empty(2) L
-    apply auto
-     apply (meson euclidean_eqI less_eq_real_def not_less)+
-    done
+    unfolding subset_box by (smt (verit) box_ne_empty(2) euclidean_eq_iff)+
 qed force
 
 lemma subset_box_complex:
@@ -895,27 +783,30 @@
       by (simp add: dual_order.antisym euclidean_eqI)
   }
   moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
-    unfolding True by (auto)
+    unfolding True by auto
   ultimately show ?thesis using True by (auto simp: cbox_def)
 next
   case False
   {
     fix y
     assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m > 0"
-    then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
+    then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" 
+          and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
       by (auto simp: inner_distrib)
   }
   moreover
   {
     fix y
     assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
-    then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
+    then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i"
+         and  "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
       by (auto simp: mult_left_mono_neg inner_distrib)
   }
   moreover
   {
     fix y
-    assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i" and "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
+    assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i"
+      and  "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
     then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
       unfolding image_iff Bex_def mem_box
       apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
@@ -946,11 +837,7 @@
   have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
     by auto
   then show ?thesis
-    apply (rule ssubst)
-    apply (rule continuous_on_compose)
-    apply (simp add: split_def)
-    apply (rule continuous_intros | simp add: assms)+
-    done
+    by (metis assms continuous_on_compose continuous_on_swap swap_cbox_Pair)
 qed
 
 
@@ -979,11 +866,11 @@
   unfolding is_interval_def  by simp
 
 lemma mem_is_intervalI:
-  assumes "is_interval s"
-    and "a \<in> s" "b \<in> s"
+  assumes "is_interval S"
+    and "a \<in> S" "b \<in> S"
     and "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i"
-  shows "x \<in> s"
-  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
+  shows "x \<in> S"
+  using assms is_interval_def by force
 
 lemma interval_subst:
   fixes S::"'a::euclidean_space set"
@@ -1016,11 +903,15 @@
     by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   also have "y bs \<in> S"
     using bs(1)[THEN equalityD1]
-    apply (induct bs)
-     apply (auto simp: y_def j)
-    apply (rule interval_subst[OF assms(1)])
-      apply (auto simp: s)
-    done
+  proof (induction bs)
+    case Nil
+    then show ?case
+      by (simp add: j y_def)
+  next
+    case (Cons a bs)
+    then show ?case
+      using interval_subst[OF assms(1)] s by (simp add: y_def)
+  qed
   finally show ?thesis .
 qed
 
@@ -1042,9 +933,8 @@
 next
   assume ?rhs
   have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
-    using assms unfolding is_interval_def
-    apply (clarsimp simp add: mem_box)
-    using that by blast
+    using assms that 
+    by (force simp: mem_box intro: mem_is_intervalI)
   with \<open>?rhs\<close> show ?lhs
     by blast
 qed
@@ -1091,8 +981,7 @@
     "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
        (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
   hence "- e \<in> X"
-    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
-      (auto simp: algebra_simps)
+    by (smt (verit, ccfv_threshold) assms inner_minus_left mem_is_intervalI)
   thus "e \<in> uminus ` X" by force
 qed
 
@@ -1266,7 +1155,7 @@
     shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
 proof -
   have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
-    by (force simp:)
+    by force
   then show ?thesis
     using interior_halfspace_ge [of a b] assms
     by (force simp: closure_interior)
@@ -1281,7 +1170,7 @@
     shows "interior {x. a \<bullet> x = b} = {}"
 proof -
   have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
-    by (force simp:)
+    by force
   then show ?thesis
     by (auto simp: assms)
 qed
@@ -1340,9 +1229,8 @@
   moreover have "?A \<inter> ?B = {}" by auto
   moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
   ultimately show False
-    using \<open>connected S\<close>[unfolded connected_def not_ex,
-      THEN spec[where x="?A"], THEN spec[where x="?B"]]
-    using xy b by auto
+    using \<open>connected S\<close> unfolding connected_def
+    by (smt (verit, del_insts) as b disjoint_iff empty_iff mem_Collect_eq xy)
 qed
 
 lemma connected_ivt_component: