# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1690495525 -3600
# Node ID cc1058b831245aa699e2c2aaf871b939e166fe2e
# Parent  67bf692cf1ab2e02bb03bc22c1b8f83d88852a0e
Cosmetic polishing of proofs

diff -r 67bf692cf1ab -r cc1058b83124 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Wed Jul 26 20:28:35 2023 +0200
+++ b/src/HOL/Analysis/Homotopy.thy	Thu Jul 27 23:05:25 2023 +0100
@@ -712,7 +712,7 @@
 
 proposition homotopic_loops_subset:
    "\<lbrakk>homotopic_loops S p q; S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
-  by (fastforce simp add: homotopic_loops)
+  by (fastforce simp: homotopic_loops)
 
 proposition homotopic_loops_eq:
    "\<lbrakk>path p; path_image p \<subseteq> S; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
@@ -1040,17 +1040,15 @@
   have "homotopic_paths S (subpath u w g +++ subpath w v g) 
                           ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
     by (simp add: hom homotopic_paths_join homotopic_paths_sym wvg)
-  also have "homotopic_paths S ((subpath u v g +++ subpath v w g) +++ subpath w v g) 
-                               (subpath u v g +++ subpath v w g +++ subpath w v g)"
+  also have "homotopic_paths S \<dots>  (subpath u v g +++ subpath v w g +++ subpath w v g)"
     using wvg vug \<open>path g\<close>
     by (metis homotopic_paths_assoc homotopic_paths_sym path_image_subpath_commute path_subpath
         pathfinish_subpath pathstart_subpath u v w)
-  also have "homotopic_paths S (subpath u v g +++ subpath v w g +++ subpath w v g)
-                               (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
+  also have "homotopic_paths S \<dots> (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
     using wvg vug \<open>path g\<close>
     by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl path_image_subpath_commute
         path_subpath pathfinish_subpath pathstart_join pathstart_subpath reversepath_subpath u v)
-  also have "homotopic_paths S (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
+  also have "homotopic_paths S \<dots> (subpath u v g)"
     using vug \<open>path g\<close> by (metis homotopic_paths_rid path_image_subpath_commute path_subpath u v)
   finally have "homotopic_paths S (subpath u w g +++ subpath w v g) (subpath u v g)" .
   then show ?thesis
@@ -1077,11 +1075,11 @@
 qed
 
 lemma homotopic_loops_imp_path_component_value:
-   "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> path_component S (p t) (q t)"
-apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
-apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
-apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
-done
+  "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> path_component S (p t) (q t)"
+  apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
+  apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
+  apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
+  done
 
 lemma homotopic_points_eq_path_component:
    "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow> path_component S a b"
@@ -1109,12 +1107,12 @@
 lemma simply_connected_imp_path_connected:
   fixes S :: "_::real_normed_vector set"
   shows "simply_connected S \<Longrightarrow> path_connected S"
-by (simp add: simply_connected_def path_connected_eq_homotopic_points)
+  by (simp add: simply_connected_def path_connected_eq_homotopic_points)
 
 lemma simply_connected_imp_connected:
   fixes S :: "_::real_normed_vector set"
   shows "simply_connected S \<Longrightarrow> connected S"
-by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
+  by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
 
 lemma simply_connected_eq_contractible_loop_any:
   fixes S :: "_::real_normed_vector set"
@@ -1123,13 +1121,10 @@
                   \<longrightarrow> homotopic_loops S p (linepath a a))"
         (is "?lhs = ?rhs")
 proof
-  assume ?lhs then show ?rhs
-    unfolding simply_connected_def by force
-next
   assume ?rhs then show ?lhs
     unfolding simply_connected_def
     by (metis pathfinish_in_path_image subsetD  homotopic_loops_trans homotopic_loops_sym)
-qed
+qed (force simp: simply_connected_def)
 
 lemma simply_connected_eq_contractible_loop_some:
   fixes S :: "_::real_normed_vector set"
@@ -1154,15 +1149,7 @@
          S = {} \<or>
          (\<exists>a \<in> S. \<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
                 \<longrightarrow> homotopic_loops S p (linepath a a))"
-        (is "?lhs = ?rhs")
-proof (cases "S = {}")
-  case True then show ?thesis by force
-next
-  case False
-  then obtain a where "a \<in> S" by blast
-  then show ?thesis
-    by (meson False homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
-qed
+  by (meson ex_in_conv homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
 
 lemma simply_connected_eq_contractible_path:
   fixes S :: "_::real_normed_vector set"
@@ -1207,14 +1194,12 @@
       using that
       by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym 
           homotopic_paths_trans pathstart_linepath)
-    also have "homotopic_paths S (p +++ reversepath q +++ q)
-                                 ((p +++ reversepath q) +++ q)"
+    also have "homotopic_paths S \<dots> ((p +++ reversepath q) +++ q)"
       by (simp add: that homotopic_paths_assoc)
-    also have "homotopic_paths S ((p +++ reversepath q) +++ q)
-                                 (linepath (pathstart q) (pathstart q) +++ q)"
+    also have "homotopic_paths S \<dots> (linepath (pathstart q) (pathstart q) +++ q)"
       using * [of "p +++ reversepath q"] that
       by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
-    also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
+    also have "homotopic_paths S \<dots> q"
       using that homotopic_paths_lid by blast
     finally show ?thesis .
   qed
@@ -1238,7 +1223,7 @@
     have "path (fst \<circ> p)"
       by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF \<open>path p\<close>])
     moreover have "path_image (fst \<circ> p) \<subseteq> S"
-      using that by (force simp add: path_image_def)
+      using that by (force simp: path_image_def)
     ultimately have p1: "homotopic_loops S (fst \<circ> p) (linepath a a)"
       using S that
       by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
@@ -1291,12 +1276,12 @@
 corollary contractible_imp_connected:
   fixes S :: "_::real_normed_vector set"
   shows "contractible S \<Longrightarrow> connected S"
-by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)
+  by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)
 
 lemma contractible_imp_path_connected:
   fixes S :: "_::real_normed_vector set"
   shows "contractible S \<Longrightarrow> path_connected S"
-by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)
+  by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)
 
 lemma nullhomotopic_through_contractible:
   fixes S :: "_::topological_space set"
@@ -1351,7 +1336,7 @@
     with \<open>path_connected U\<close> show ?thesis by blast
   qed
   then have "homotopic_with_canon (\<lambda>h. True) S U (\<lambda>x. c2) (\<lambda>x. c1)"
-    by (auto simp add: path_component homotopic_constant_maps)
+    by (auto simp: path_component homotopic_constant_maps)
   then show ?thesis
     using c1 c2 homotopic_with_symD homotopic_with_trans by blast
 qed
@@ -1419,7 +1404,7 @@
     using \<open>a \<in> S\<close>
     unfolding homotopic_with_def
     apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
-    apply (force simp add: P intro: continuous_intros)
+    apply (force simp: P intro: continuous_intros)
     done
   then show ?thesis
     using that by blast
@@ -1516,18 +1501,17 @@
 where
  "locally P S \<equiv>
         \<forall>w x. openin (top_of_set S) w \<and> x \<in> w
-              \<longrightarrow> (\<exists>u v. openin (top_of_set S) u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
+              \<longrightarrow> (\<exists>U V. openin (top_of_set S) U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> w)"
 
 lemma locallyI:
   assumes "\<And>w x. \<lbrakk>openin (top_of_set S) w; x \<in> w\<rbrakk>
-                  \<Longrightarrow> \<exists>u v. openin (top_of_set S) u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w"
+                  \<Longrightarrow> \<exists>U V. openin (top_of_set S) U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> w"
     shows "locally P S"
 using assms by (force simp: locally_def)
 
 lemma locallyE:
   assumes "locally P S" "openin (top_of_set S) w" "x \<in> w"
-  obtains u v where "openin (top_of_set S) u"
-                    "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> w"
+  obtains U V where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> w"
   using assms unfolding locally_def by meson
 
 lemma locally_mono:
@@ -1636,28 +1620,26 @@
     using \<open>f ` S = T\<close> f \<open>V \<subseteq> S\<close> by auto
   have contvf: "continuous_on V f"
     using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
-  have "f ` V \<subseteq> W"
-    using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
-  then have contvg: "continuous_on (f ` V) g"
-    using \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
-  have "V \<subseteq> g ` f ` V"
-    by (metis \<open>V \<subseteq> S\<close> hom homeomorphism_def homeomorphism_of_subsets order_refl)
-  then have homv: "homeomorphism V (f ` V) f g"
-    using \<open>V \<subseteq> S\<close> f by (auto simp: homeomorphism_def contvf contvg)
   have "openin (top_of_set (g ` T)) U"
     using \<open>g ` T = S\<close> by (simp add: osu)
   then have "openin (top_of_set T) (T \<inter> g -` U)"
     using \<open>continuous_on T g\<close> continuous_on_open [THEN iffD1] by blast
   moreover have "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
   proof (intro exI conjI)
+    show "f ` V \<subseteq> W"
+      using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
+    then have contvg: "continuous_on (f ` V) g"
+      using \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
+    have "V \<subseteq> g ` f ` V"
+      by (metis \<open>V \<subseteq> S\<close> hom homeomorphism_def homeomorphism_of_subsets order_refl)
+    then have homv: "homeomorphism V (f ` V) f g"
+      using \<open>V \<subseteq> S\<close> f by (auto simp: homeomorphism_def contvf contvg)
     show "Q (f ` V)"
       using Q homv \<open>P V\<close> by blast
     show "y \<in> T \<inter> g -` U"
       using T(2) \<open>y \<in> W\<close> \<open>g y \<in> U\<close> by blast
     show "T \<inter> g -` U \<subseteq> f ` V"
       using g(1) image_iff uv(3) by fastforce
-    show "f ` V \<subseteq> W"
-      using \<open>f ` V \<subseteq> W\<close> by blast
   qed
   ultimately show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
     by meson
@@ -1692,8 +1674,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "linear f" "inj f" and iff: "\<And>S. P (f ` S) \<longleftrightarrow> Q S"
   shows "locally P (f ` S) \<longleftrightarrow> locally Q S"
-  using homeomorphism_locally [of "f`S" _ _ f] linear_homeomorphism_image [OF f]
-  by (metis (no_types, lifting) homeomorphism_image2 iff)
+  by (smt (verit) f homeomorphism_image2 homeomorphism_locally iff linear_homeomorphism_image)
 
 lemma locally_open_map_image:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1782,8 +1763,8 @@
     shows "R a b"
 proof -
   have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
-    apply (rule connected_induction_simple [OF \<open>connected S\<close>], simp_all)
-    by (meson local.sym local.trans opI openin_imp_subset subsetCE)
+    by (smt (verit, ccfv_threshold) connected_induction_simple [OF \<open>connected S\<close>] 
+            assms openin_imp_subset subset_eq)
   then show ?thesis by (metis etc opI)
 qed
 
@@ -1833,13 +1814,13 @@
               compact v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<inter> T"
           if "open T" "x \<in> S" "x \<in> T" for x T
   proof -
-    obtain u v where uv: "x \<in> u" "u \<subseteq> v" "v \<subseteq> S" "compact v" "openin (top_of_set S) u"
+    obtain U V where uv: "x \<in> U" "U \<subseteq> V" "V \<subseteq> S" "compact V" "openin (top_of_set S) U"
       using r [OF \<open>x \<in> S\<close>] by auto
     obtain e where "e>0" and e: "cball x e \<subseteq> T"
       using open_contains_cball \<open>open T\<close> \<open>x \<in> T\<close> by blast
     show ?thesis
-      apply (rule_tac x="(S \<inter> ball x e) \<inter> u" in exI)
-      apply (rule_tac x="cball x e \<inter> v" in exI)
+      apply (rule_tac x="(S \<inter> ball x e) \<inter> U" in exI)
+      apply (rule_tac x="cball x e \<inter> V" in exI)
       using that \<open>e > 0\<close> e uv
       apply auto
       done
@@ -1860,16 +1841,8 @@
   shows "locally compact S \<longleftrightarrow>
          (\<forall>x \<in> S. \<exists>U. x \<in> U \<and>
                     openin (top_of_set S) U \<and> compact(closure U) \<and> closure U \<subseteq> S)"
-        (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    by (meson bounded_subset closure_minimal compact_closure compact_imp_bounded 
-              compact_imp_closed dual_order.trans locally_compactE)
-next
-  assume ?rhs then show ?lhs
-    by (meson closure_subset locally_compact)
-qed
+  by (smt (verit, ccfv_threshold) bounded_subset closure_closed closure_mono closure_subset 
+      compact_closure compact_imp_closed order.trans locally_compact)
 
 lemma locally_compact_Int_cball:
   fixes S :: "'a :: heine_borel set"
@@ -2008,8 +1981,9 @@
   then show ?rhs
     unfolding locally_def
     apply (elim all_forward imp_forward asm_rl exE)
-    apply (rule_tac x = "u \<inter> ball x 1" in exI)
-    apply (rule_tac x = "v \<inter> cball x 1" in exI)
+    apply (rename_tac U V)
+    apply (rule_tac x = "U \<inter> ball x 1" in exI)
+    apply (rule_tac x = "V \<inter> cball x 1" in exI)
     apply (force intro: openin_trans)
     done
 next
@@ -2019,7 +1993,7 @@
 
 lemma locally_compact_openin_Un:
   fixes S :: "'a::euclidean_space set"
-  assumes LCS: "locally compact S" and LCT:"locally compact T"
+  assumes LCS: "locally compact S" and LCT: "locally compact T"
       and opS: "openin (top_of_set (S \<union> T)) S"
       and opT: "openin (top_of_set (S \<union> T)) T"
     shows "locally compact (S \<union> T)"
@@ -2453,7 +2427,7 @@
     "\<And>v x. \<lbrakk>openin (top_of_set S) v; x \<in> v\<rbrakk>
               \<Longrightarrow> \<exists>u. openin (top_of_set S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
    shows "locally path_connected S"
-  by (force simp add: locally_def dest: assms)
+  by (force simp: locally_def dest: assms)
 
 lemma locally_path_connected_2:
   assumes "locally path_connected S"
@@ -2525,7 +2499,7 @@
 proof
   assume ?lhs
   then show ?rhs
-    by (fastforce simp add: locally_connected)
+    by (fastforce simp: locally_connected)
 next
   assume ?rhs
   have *: "\<exists>T. openin (top_of_set S) T \<and> x \<in> T \<and> T \<subseteq> c"
@@ -3577,7 +3551,7 @@
   show thesis
     using homotopic_with_compose_continuous_map_right
            [OF homotopic_with_compose_continuous_map_left [OF b g] f]
-    by (force simp add: that)
+    by (force simp: that)
 qed
 
 lemma nullhomotopic_into_contractible_space:
@@ -3901,7 +3875,7 @@
     by (rule homotopic_with_compose_continuous_left [where Y=T])
        (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
   ultimately show ?thesis
-    using that homotopic_with_trans by (fastforce simp add: o_def)
+    using that homotopic_with_trans by (fastforce simp: o_def)
 qed
 
 lemma homotopy_eqv_cohomotopic_triviality_null:
@@ -3942,7 +3916,7 @@
     by (rule homotopic_with_compose_continuous_right [where X=T])
        (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
   ultimately show ?thesis
-    using homotopic_with_trans by (fastforce simp add: o_def)
+    using homotopic_with_trans by (fastforce simp: o_def)
 qed
 
 lemma homotopy_eqv_homotopic_triviality_null:
@@ -5002,7 +4976,7 @@
       using \<gamma> by (auto simp: pairwise_def bij_betw_def inj_on_def)
   qed (use affine_hull_open assms that in auto)
   then show ?thesis
-    using \<gamma> \<open>P \<subseteq> U\<close> bij_betwE by (fastforce simp add: intro!: that)
+    using \<gamma> \<open>P \<subseteq> U\<close> bij_betwE by (fastforce simp: intro!: that)
 next
   case False
   with DIM_positive have "DIM('a) = 1"
@@ -5089,7 +5063,7 @@
       using \<gamma> by (auto simp: pairwise_def bij_betw_def inj_on_def)
   qed
   then show ?thesis
-    using \<gamma> \<open>P \<subseteq> U\<close> bij_betwE by (fastforce simp add: intro!: that)
+    using \<gamma> \<open>P \<subseteq> U\<close> bij_betwE by (fastforce simp: intro!: that)
 next
   case False
   with aff_dim_geq [of S] consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S = 1" by linarith
@@ -5173,9 +5147,9 @@
             using \<open>T \<subseteq> affine hull S\<close> h by auto
         qed
         show "\<And>x. x \<in> T \<Longrightarrow> g' (f' x) = x"
-          using h j hom homeomorphism_apply1 by (fastforce simp add: f'_def g'_def)
+          using h j hom homeomorphism_apply1 by (fastforce simp: f'_def g'_def)
         show "\<And>y. y \<in> T \<Longrightarrow> f' (g' y) = y"
-          using h j hom homeomorphism_apply2 by (fastforce simp add: f'_def g'_def)
+          using h j hom homeomorphism_apply2 by (fastforce simp: f'_def g'_def)
       qed
     next
       have \<section>: "\<And>x y. \<lbrakk>x \<in> affine hull S; h x = h y; y \<in> S\<rbrakk> \<Longrightarrow> x \<in> S"
@@ -5241,7 +5215,7 @@
            and d: "\<And>x'. \<lbrakk>dist x' a \<le> r; x' \<noteq> a; dist x' x < d\<rbrakk> \<Longrightarrow>
                                  dist (g x') (g x) < e"
           using contg False x \<open>e>0\<close>
-          unfolding continuous_on_iff by (fastforce simp add: dist_commute intro: that)
+          unfolding continuous_on_iff by (fastforce simp: dist_commute intro: that)
         show ?thesis
           using \<open>d > 0\<close> \<open>x \<noteq> a\<close>
           by (rule_tac x="min d (norm(x - a))" in exI)
@@ -5287,7 +5261,7 @@
   next
     assume ?rhs
     then show ?lhs
-      using equal continuous_on_const by (force simp add: homotopic_with)
+      using equal continuous_on_const by (force simp: homotopic_with)
   qed
 next
   case greater
diff -r 67bf692cf1ab -r cc1058b83124 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Wed Jul 26 20:28:35 2023 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Thu Jul 27 23:05:25 2023 +0100
@@ -1355,7 +1355,7 @@
               case False
               have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
                 by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
-              also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
+              also have "\<dots> = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
                 using \<open>ux \<noteq> 0\<close> equx apply (auto simp: field_split_simps)
                 by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
               finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
@@ -1501,7 +1501,7 @@
 proof
   have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
     using Krein_Milman_Minkowski assms by blast
-  also have "... \<subseteq> ?rhs"
+  also have "\<dots> \<subseteq> ?rhs"
   proof (rule hull_mono)
     show "{x. x extreme_point_of S} \<subseteq> frontier S"
       using closure_subset
@@ -1511,7 +1511,7 @@
 next
   have "?rhs \<subseteq> convex hull S"
     by (metis Diff_subset \<open>compact S\<close> closure_closed compact_eq_bounded_closed frontier_def hull_mono)
-  also have "... \<subseteq> ?lhs"
+  also have "\<dots> \<subseteq> ?lhs"
     by (simp add: \<open>convex S\<close> hull_same)
   finally show "?rhs \<subseteq> ?lhs" .
 qed
@@ -1626,12 +1626,11 @@
   done
 
 lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
-  unfolding polyhedron_def
-  by (rule_tac x="{}" in exI) auto
+  using polyhedron_def by auto
 
 lemma polyhedron_Inter [intro,simp]:
-   "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
-by (induction F rule: finite_induct) auto
+  "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
+  by (induction F rule: finite_induct) auto
 
 
 lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
@@ -1640,10 +1639,7 @@
   have "\<exists>a. a \<noteq> 0 \<and> (\<exists>b. {x. i \<bullet> x \<le> -1} = {x. a \<bullet> x \<le> b})"
     by (rule_tac x="i" in exI) (force simp: i_def SOME_Basis nonzero_Basis)
   moreover have "\<exists>a b. a \<noteq> 0 \<and> {x. -i \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b}"
-      apply (rule_tac x="-i" in exI)
-      apply (rule_tac x="-1" in exI)
-      apply (simp add: i_def SOME_Basis nonzero_Basis)
-      done
+    by (metis Basis_zero SOME_Basis i_def neg_0_equal_iff_equal)
   ultimately show ?thesis
     unfolding polyhedron_def
     by (rule_tac x="{{x. i \<bullet> x \<le> -1}, {x. -i \<bullet> x \<le> -1}}" in exI) force
@@ -1664,7 +1660,7 @@
 lemma polyhedron_halfspace_ge:
   fixes a :: "'a :: euclidean_space"
   shows "polyhedron {x. a \<bullet> x \<ge> b}"
-using polyhedron_halfspace_le [of "-a" "-b"] by simp
+  using polyhedron_halfspace_le [of "-a" "-b"] by simp
 
 lemma polyhedron_hyperplane:
   fixes a :: "'a :: euclidean_space"
@@ -1679,7 +1675,7 @@
 lemma affine_imp_polyhedron:
   fixes S :: "'a :: euclidean_space set"
   shows "affine S \<Longrightarrow> polyhedron S"
-by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
+  by (metis affine_hull_finite_intersection_hyperplanes hull_same polyhedron_Inter polyhedron_hyperplane)
 
 lemma polyhedron_imp_closed:
   fixes S :: "'a :: euclidean_space set"
@@ -1694,7 +1690,7 @@
 lemma polyhedron_affine_hull:
   fixes S :: "'a :: euclidean_space set"
   shows "polyhedron(affine hull S)"
-by (simp add: affine_imp_polyhedron)
+  by (simp add: affine_imp_polyhedron)
 
 
 subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
@@ -1704,14 +1700,7 @@
   shows "polyhedron S \<longleftrightarrow>
            (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
                 (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
-        (is "?lhs = ?rhs")
-proof
-  assume ?lhs then show ?rhs
-    using hull_subset polyhedron_def by fastforce
-next
-  assume ?rhs then show ?lhs
-    by (metis polyhedron_Int polyhedron_Inter polyhedron_affine_hull polyhedron_halfspace_le)
-qed
+  by (metis hull_subset inf.absorb_iff2 polyhedron_Int polyhedron_affine_hull polyhedron_def)
 
 proposition rel_interior_polyhedron_explicit:
   assumes "finite F"
@@ -1744,13 +1733,13 @@
     define \<xi> where "\<xi> = min (1/2) (e / 2 / norm(z - x))"
     have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
       by (simp add: \<xi>_def algebra_simps norm_mult)
-    also have "... = \<xi> * norm (x - z)"
+    also have "\<dots> = \<xi> * norm (x - z)"
       using \<open>e > 0\<close> by (simp add: \<xi>_def)
-    also have "... < e"
+    also have "\<dots> < e"
       using \<open>z \<noteq> x\<close> \<open>e > 0\<close> by (simp add: \<xi>_def min_def field_split_simps norm_minus_commute)
     finally have lte: "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) < e" .
     have \<xi>_aff: "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> affine hull S"
-      by (metis \<open>x \<in> S\<close> add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff)
+      by (simp add: \<open>x \<in> S\<close> hull_inc mem_affine zaff)
     have "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> S"
       using ins [OF _ \<xi>_aff] by (simp add: algebra_simps lte)
     then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \<in> S"
@@ -1809,7 +1798,7 @@
       have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
         using \<open>h \<in> F\<close> ab by auto
       then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
-        by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
+        by (metis affine_hull_eq_empty inf.absorb_iff1 inf_assoc inf_bot_left seq that(2))
       moreover have "\<not> (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
         using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
       ultimately show ?thesis
@@ -1822,14 +1811,14 @@
                   affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
                   (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
       by metis
-    have seq2: "S = affine hull S \<inter> (\<Inter>h\<in>{h \<in> F. \<not> affine hull S \<subseteq> h}. {x. a h \<bullet> x \<le> b h})"
-      by (subst seq) (auto simp: ab INT_extend_simps)
+    let ?F = "(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h \<in> F. \<not> affine hull S \<subseteq> h}"
     show ?thesis
-      apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> \<not>(affine hull S \<subseteq> h)}" in exI)
-      apply (intro conjI seq2)
-        using \<open>finite F\<close> apply force
-       using ab apply blast
-       done
+    proof (intro exI conjI)
+      show "finite ?F"
+        using \<open>finite F\<close> by force
+      show "S = affine hull S \<inter> \<Inter> ?F"
+        by (subst seq) (auto simp: ab INT_extend_simps)
+    qed (use ab in blast)
   qed
 next
   assume ?rhs then show ?lhs
@@ -1887,12 +1876,7 @@
          (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}) \<and>
               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'))"
-     (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    by (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward)
-qed (auto simp: polyhedron_Int_affine elim!: ex_forward)
+  by (metis polyhedron_Int_affine polyhedron_Int_affine_parallel_minimal)
 
 proposition facet_of_polyhedron_explicit:
   assumes "finite F"
@@ -1928,7 +1912,7 @@
     have "x \<in> h" using that xint by auto
     then have able: "a h \<bullet> x \<le> b h"
       using faceq that by blast
-    also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
+    also have "\<dots> < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
     finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
     define l where "l = (b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
     define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z"
@@ -1942,14 +1926,15 @@
       moreover have "l * (a i \<bullet> z) \<le> l * b i"
       proof (rule mult_left_mono)
         show "a i \<bullet> z \<le> b i"
-          by (metis Diff_insert_absorb Inter_iff Set.set_insert \<open>h \<in> F\<close> faceq insertE mem_Collect_eq that zint)
+          by (metis DiffI Inter_iff empty_iff faceq insertE mem_Collect_eq that zint)
       qed (use \<open>0 < l\<close> in auto)
       ultimately show ?thesis by (simp add: w_def algebra_simps)
     qed
     have weq: "a h \<bullet> w = b h"
       using xltz unfolding w_def l_def
       by (simp add: algebra_simps) (simp add: field_simps)
-    have faceS: "S \<inter> {x. a h \<bullet> x = b h} face_of S"
+    let ?F = "{x. a h \<bullet> x = b h}"
+    have faceS: "S \<inter> ?F face_of S"
     proof (rule face_of_Int_supporting_hyperplane_le)
       show "\<And>x. x \<in> S \<Longrightarrow> a h \<bullet> x \<le> b h"
         using faceq seq that by fastforce
@@ -1960,15 +1945,18 @@
       using \<open>a h \<bullet> w = b h\<close> awlt faceq less_eq_real_def by blast
     ultimately have "w \<in> S"
       using seq by blast
-    with weq have ne: "S \<inter> {x. a h \<bullet> x = b h} \<noteq> {}" by blast
-    moreover have "affine hull (S \<inter> {x. a h \<bullet> x = b h}) = (affine hull S) \<inter> {x. a h \<bullet> x = b h}"
+    with weq have ne: "S \<inter> ?F \<noteq> {}" by blast
+    moreover have "affine hull (S \<inter> ?F) = (affine hull S) \<inter> ?F"
     proof
-      show "affine hull (S \<inter> {x. a h \<bullet> x = b h}) \<subseteq> affine hull S \<inter> {x. a h \<bullet> x = b h}"
-        apply (intro Int_greatest hull_mono Int_lower1)
-        apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2)
-        done
+      show "affine hull (S \<inter> ?F) \<subseteq> affine hull S \<inter> ?F"
+      proof -
+        have "affine hull (S \<inter> ?F) \<subseteq> affine hull S"
+          by (simp add: hull_mono)
+        then show ?thesis
+          by (simp add: affine_hyperplane subset_hull)
+      qed
     next
-      show "affine hull S \<inter> {x. a h \<bullet> x = b h} \<subseteq> affine hull (S \<inter> {x. a h \<bullet> x = b h})"
+      show "affine hull S \<inter> ?F \<subseteq> affine hull (S \<inter> ?F)"
       proof
         fix y
         assume yaff: "y \<in> affine hull S \<inter> {y. a h \<bullet> y = b h}"
@@ -2014,7 +2002,7 @@
             case False
             with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
               by (simp add: mult_le_0_iff)
-            also have "... < b j - a j \<bullet> w"
+            also have "\<dots> < b j - a j \<bullet> w"
               by (simp add: awlt that)
             finally show ?thesis by simp
           qed
@@ -2050,7 +2038,7 @@
           by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff])
       qed
     qed
-    ultimately have "aff_dim (affine hull (S \<inter> {x. a h \<bullet> x = b h})) = aff_dim S - 1"
+    ultimately have "aff_dim (affine hull (S \<inter> ?F)) = aff_dim S - 1"
       using \<open>b h < a h \<bullet> z\<close> zaff by (force simp: aff_dim_affine_Int_hyperplane)
     then show ?thesis
       by (simp add: ne faceS facet_of_def)
@@ -2755,7 +2743,7 @@
       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + x"
       using \<open>a>0\<close> by (simp add: distrib_right floor_divide_lower)
-    also have "... < y"
+    also have "\<dots> < y"
       by (rule 1)
     finally have "?n * a < y" .
     with x show ?thesis
@@ -2767,7 +2755,7 @@
       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + y"
       using \<open>a>0\<close> by (simp add: distrib_right floor_divide_lower)
-    also have "... < x"
+    also have "\<dots> < x"
       by (rule 2)
     finally have "?n * a < x" .
     then show ?thesis
@@ -2891,7 +2879,7 @@
             using B \<open>X \<in> \<F>'\<close> eq that by blast+
           have "norm (x - y) \<le> (\<Sum>b\<in>Basis. \<bar>(x-y) \<bullet> b\<bar>)"
             by (rule norm_le_l1)
-          also have "... \<le> of_nat (DIM('a)) * (e / 2 / DIM('a))"
+          also have "\<dots> \<le> of_nat (DIM('a)) * (e / 2 / DIM('a))"
           proof (rule sum_bounded_above)
             fix i::'a
             assume "i \<in> Basis"
@@ -2930,12 +2918,12 @@
                 using  I' [OF \<open>n \<in> C\<close> refl] n  by auto
             qed
           qed
-          also have "... = e / 2"
+          also have "\<dots> = e / 2"
             by simp
           finally show ?thesis .
         qed
       qed (use \<open>0 < e\<close> in force)
-      also have "... < e"
+      also have "\<dots> < e"
         by (simp add: \<open>0 < e\<close>)
       finally show ?thesis .
     qed
@@ -3240,7 +3228,7 @@
           using \<open>K \<in> \<U>\<close> C\<U> by blast
         have "K \<le> rel_frontier C"
           by (simp add: \<open>K \<subseteq> rel_frontier C\<close>)
-        also have "... \<le> C"
+        also have "\<dots> \<le> C"
           by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
         finally have "K \<subseteq> C" .
         have "L \<inter> C face_of C"
@@ -3292,7 +3280,7 @@
               by (auto simp: \<open>\<not> affine_dependent I\<close> aff_independent_finite finite_imp_compact)
             moreover have "F face_of convex hull insert ?z I"
               by (metis S \<open>F face_of S\<close> \<open>K = convex hull I\<close> convex_hull_eq_empty convex_hull_insert_segments hull_hull)
-            ultimately obtain J where "J \<subseteq> insert ?z I" "F = convex hull J"
+            ultimately obtain J where J: "J \<subseteq> insert ?z I" "F = convex hull J"
               using face_of_convex_hull_subset [of "insert ?z I" F] by auto
             show ?thesis
             proof (cases "?z \<in> J")
@@ -3320,7 +3308,7 @@
               case False
               then have "F \<in> \<U>"
                 using face_of_convex_hull_affine_independent [OF \<open>\<not> affine_dependent I\<close>]
-                by (metis Int_absorb2 Int_insert_right_if0 \<open>F = convex hull J\<close> \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> face\<U> inf_le2 \<open>K \<in> \<U>\<close>)
+                by (metis J \<open>K = convex hull I\<close> face\<U> subset_insert \<open>K \<in> \<U>\<close>)
               then show "F \<in> \<U> \<union> ?\<T>"
                 by blast
             qed
@@ -3366,7 +3354,7 @@
             using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
           have "X \<inter> K face_of K"
             by (simp add: XY(1) \<open>K \<in> \<U>\<close> faceI\<U> inf_commute)
-          also have "... face_of convex hull insert ?z K"
+          also have "\<dots> face_of convex hull insert ?z K"
             by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
           finally have "X \<inter> K face_of convex hull insert ?z K" .
           then show ?thesis
@@ -3413,7 +3401,7 @@
                 using \<open>L \<subseteq> rel_frontier D\<close> by auto
               have "convex hull insert (SOME z. z \<in> rel_interior C) (K \<inter> L) face_of
                     convex hull insert (SOME z. z \<in> rel_interior C) K"
-                by (metis face_of_polytope_insert2 "*" IntI \<open>C \<in> \<N>\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_def z \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close>)
+                by (metis IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<in> \<U>\<close> ahK_C_disjoint empty_iff faceI\<U> face_of_polytope_insert2 simpl\<U> simplex_imp_polytope z)
               then show ?thesis
                 using True X Y \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close> convex_hull_insert_Int_eq z by force
             next
@@ -3442,7 +3430,7 @@
               qed
               finally have CD: "C \<inter> (rel_interior D) = {}" .
               have zKC: "(convex hull insert ?z K) \<subseteq> C"
-                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
+                by (metis \<open>K \<subseteq> C\<close> \<open>convex C\<close> in_mono insert_subsetI rel_interior_subset subset_hull z)
               have "disjnt (convex hull insert (SOME z. z \<in> rel_interior C) K) (rel_interior D)"
                 using zKC CD by (force simp: disjnt_def)
               then have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
@@ -3454,7 +3442,7 @@
                 by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
               have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
                 by blast
-              also have "... = convex hull K \<inter> L"
+              also have "\<dots> = convex hull K \<inter> L"
               proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
                 have "(C \<inter> D) \<inter> rel_interior C = {}"
                 proof (rule face_of_disjoint_rel_interior)
@@ -3482,26 +3470,26 @@
               finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
               have "convex hull insert ?z K \<inter> convex hull L face_of K"
                 by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
-              also have "... face_of convex hull insert ?z K"
+              also have "\<dots> face_of convex hull insert ?z K"
               proof -
                 obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
                   using * [OF \<open>K \<in> \<U>\<close>] by auto
                 then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
                   using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
                 then show ?thesis
-                  by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
+                  by (metis I \<open>convex K\<close> aff_independent_finite face_of_convex_hull_insert_eq face_of_refl hull_insert z)
               qed
               finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
               have "convex hull insert ?z K \<inter> convex hull L face_of L"
                 by (metis \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> chKL ch_id faceI\<U> inf_commute)
-              also have "... face_of convex hull insert ?w L"
+              also have "\<dots> face_of convex hull insert ?w L"
               proof -
                 obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
                   using * [OF \<open>L \<in> \<U>\<close>] by auto
                 then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
                   using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
                 then show ?thesis
-                  by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
+                  by (metis I \<open>convex L\<close> aff_independent_finite face_of_convex_hull_insert face_of_refl hull_insert w)
               qed
               finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
               show ?thesis
@@ -3767,18 +3755,13 @@
           if "T \<in> {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}" for T
           using that dense_complement_convex_closed \<open>closed U\<close> \<open>convex U\<close> by auto
       qed
-      also have "... \<subseteq> closure ?lhs"
+      also have "\<dots> \<subseteq> closure ?lhs"
       proof -
         obtain C where "C \<in> \<S>" "aff_dim C < aff_dim U"
           by (metis False Sup_upper aff_dim_subset eq eq_iff not_le)
-        have "\<exists>X. X \<in> \<S> \<and> aff_dim X = aff_dim U \<and> x \<in> X"
+        then have "\<exists>X. X \<in> \<S> \<and> aff_dim X = aff_dim U \<and> x \<in> X"
           if "\<And>V. (\<exists>C. V = U - C \<and> C \<in> \<S> \<and> aff_dim C < aff_dim U) \<Longrightarrow> x \<in> V" for x
-        proof -
-          have "x \<in> U \<and> x \<in> \<Union>\<S>"
-            using \<open>C \<in> \<S>\<close> \<open>aff_dim C < aff_dim U\<close> eq that by blast
-          then show ?thesis
-            by (metis Diff_iff Sup_upper Union_iff aff_dim_subset dual_order.order_iff_strict eq that)
-        qed
+          by (metis Diff_iff Sup_upper UnionE aff_dim_subset eq order_less_le that)
         then show ?thesis
           by (auto intro!: closure_mono)
       qed
diff -r 67bf692cf1ab -r cc1058b83124 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Wed Jul 26 20:28:35 2023 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Jul 27 23:05:25 2023 +0100
@@ -14,99 +14,56 @@
     and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
   shows "(\<Sum>i\<in>S. sum (x i) (T i)) = (\<Sum>(i, j)\<in>Sigma S T. x i j)"
   using assms
-proof induct
-  case empty
-  then show ?case
-    by simp
-next
-  case (insert a S)
-  show ?case
-    by (simp add: insert.hyps(1) insert.prems sum.Sigma)
-qed
+  by induction (auto simp: sum.Sigma)
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
 
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Sundries\<close>
-
-
-text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
-lemma wf_finite_segments:
-  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
-  shows "wf (r)"
-  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
-  using acyclic_def assms irrefl_def trans_Restr by fastforce
-
-text\<open>For creating values between \<^term>\<open>u\<close> and \<^term>\<open>v\<close>.\<close>
-lemma scaling_mono:
-  fixes u::"'a::linordered_field"
-  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
-    shows "u + r * (v - u) / s \<le> v"
-proof -
-  have "r/s \<le> 1" using assms
-    using divide_le_eq_1 by fastforce
-  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
-    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
-  then show ?thesis
-    by (simp add: field_simps)
-qed
-
 subsection \<open>Some useful lemmas about intervals\<close>
 
 lemma interior_subset_union_intervals:
-  assumes "i = cbox a b"
-    and "j = cbox c d"
-    and "interior j \<noteq> {}"
+  fixes a b c d
+  defines "i \<equiv> cbox a b"
+  defines "j \<equiv> cbox c d"
+  assumes "interior j \<noteq> {}"
     and "i \<subseteq> j \<union> S"
     and "interior i \<inter> interior j = {}"
   shows "interior i \<subseteq> interior S"
-proof -
-  have "box a b \<inter> cbox c d = {}"
-     using Int_interval_mixed_eq_empty[of c d a b] assms
-     unfolding interior_cbox by auto
-  moreover
-  have "box a b \<subseteq> cbox c d \<union> S"
-    apply (rule order_trans,rule box_subset_cbox)
-    using assms by auto
-  ultimately
-  show ?thesis
-    unfolding assms interior_cbox
-      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
-qed
+  by (smt (verit, del_insts) IntI Int_interval_mixed_eq_empty UnE assms empty_iff interior_cbox interior_maximal interior_subset open_interior subset_eq)
 
 lemma interior_Union_subset_cbox:
-  assumes "finite f"
-  assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t"
-    and t: "closed t"
-  shows "interior (\<Union>f) \<subseteq> t"
+  assumes "finite \<F>"
+  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a b. S = cbox a b" "\<And>S. S \<in> \<F> \<Longrightarrow> interior S \<subseteq> T"
+    and T: "closed T"
+  shows "interior (\<Union>\<F>) \<subseteq> T"
 proof -
-  have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
-    using f by auto
-  define E where "E = {s\<in>f. interior s = {}}"
-  then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
-    using \<open>finite f\<close> by auto
-  then have "interior (\<Union>f) = interior (\<Union>(f - E))"
+  have clo[simp]: "S \<in> \<F> \<Longrightarrow> closed S" for S
+    using \<F> by auto
+  define E where "E = {s\<in>\<F>. interior s = {}}"
+  then have "finite E" "E \<subseteq> {s\<in>\<F>. interior s = {}}"
+    using \<open>finite \<F>\<close> by auto
+  then have "interior (\<Union>\<F>) = interior (\<Union>(\<F> - E))"
   proof (induction E rule: finite_subset_induct')
     case (insert s f')
-    have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
-      using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
-    also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
+    have "interior (\<Union>(\<F> - insert s f') \<union> s) = interior (\<Union>(\<F> - insert s f'))"
+      using insert.hyps \<open>finite \<F>\<close> by (intro interior_closed_Un_empty_interior) auto
+    also have "\<Union>(\<F> - insert s f') \<union> s = \<Union>(\<F> - f')"
       using insert.hyps by auto
     finally show ?case
       by (simp add: insert.IH)
   qed simp
-  also have "\<dots> \<subseteq> \<Union>(f - E)"
+  also have "\<dots> \<subseteq> \<Union>(\<F> - E)"
     by (rule interior_subset)
-  also have "\<dots> \<subseteq> t"
+  also have "\<dots> \<subseteq> T"
   proof (rule Union_least)
-    fix s assume "s \<in> f - E"
-    with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
+    fix s assume "s \<in> \<F> - E"
+    with \<F>[of s] obtain a b where s: "s \<in> \<F>" "s = cbox a b" "box a b \<noteq> {}"
       by (fastforce simp: E_def)
-    have "closure (interior s) \<subseteq> closure t"
-      by (intro closure_mono f \<open>s \<in> f\<close>)
-    with s \<open>closed t\<close> show "s \<subseteq> t"
+    have "closure (interior s) \<subseteq> closure T"
+      by (intro closure_mono \<F> \<open>s \<in> \<F>\<close>)
+    with s \<open>closed T\<close> show "s \<subseteq> T"
       by simp
   qed
   finally show ?thesis .
@@ -195,14 +152,12 @@
 definition\<^marker>\<open>tag important\<close> "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
 
 lemma gaugeI:
-  assumes "\<And>x. x \<in> \<gamma> x"
-    and "\<And>x. open (\<gamma> x)"
+  assumes "\<And>x. x \<in> \<gamma> x" and "\<And>x. open (\<gamma> x)"
   shows "gauge \<gamma>"
   using assms unfolding gauge_def by auto
 
 lemma gaugeD[dest]:
-  assumes "gauge \<gamma>"
-  shows "x \<in> \<gamma> x"
+  assumes "gauge \<gamma>" shows "x \<in> \<gamma> x"
     and "open (\<gamma> x)"
   using assms unfolding gauge_def by auto
 
@@ -213,7 +168,7 @@
   unfolding gauge_def by auto
 
 lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
-  by (rule gauge_ball) auto
+  by auto
 
 lemma gauge_Int[intro]: "gauge \<gamma>1 \<Longrightarrow> gauge \<gamma>2 \<Longrightarrow> gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
   unfolding gauge_def by auto
@@ -221,8 +176,7 @@
 lemma gauge_reflect:
   fixes \<gamma> :: "'a::euclidean_space \<Rightarrow> 'a set"
   shows "gauge \<gamma> \<Longrightarrow> gauge (\<lambda>x. uminus ` \<gamma> (- x))"
-  using equation_minus_iff
-  by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
+  by (metis (mono_tags, lifting) gauge_def imageI open_negations minus_minus)
 
 lemma gauge_Inter:
   assumes "finite S"
@@ -233,7 +187,7 @@
     by auto
   show ?thesis
     unfolding gauge_def unfolding *
-    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
+    by (simp add: assms gaugeD open_INT)
 qed
 
 lemma gauge_existence_lemma:
@@ -290,18 +244,6 @@
   "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
   (is "?l = ?r")
 proof
-  assume ?r
-  moreover
-  { fix K
-    assume "s = {{a}}" "K\<in>s"
-    then have "\<exists>x y. K = cbox x y"
-      apply (rule_tac x=a in exI)+
-      apply force
-      done
-  }
-  ultimately show ?l
-    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_idem division_ofD(2) division_ofD(3) subset_singletonD that)
@@ -309,10 +251,10 @@
     using \<open>s division_of cbox a a\<close> by auto
   ultimately show ?r
     unfolding cbox_idem by auto
-qed
+qed (use cbox_idem in blast)
 
 lemma elementary_empty: obtains p where "p division_of {}"
-  unfolding division_of_trivial by auto
+  by simp
 
 lemma elementary_interval: obtains p where "p division_of (cbox a b)"
   by (metis division_of_trivial division_of_self)
@@ -334,31 +276,24 @@
     and "q \<subseteq> p"
   shows "q division_of (\<Union>q)"
 proof (rule division_ofI)
-  note * = division_ofD[OF assms(1)]
   show "finite q"
-    using "*"(1) assms(2) infinite_super by auto
-  {
-    fix k
-    assume "k \<in> q"
-    then have kp: "k \<in> p"
-      using assms(2) by auto
-    show "k \<subseteq> \<Union>q"
-      using \<open>k \<in> q\<close> by auto
-    show "\<exists>a b. k = cbox a b"
-      using *(4)[OF kp] by auto
-    show "k \<noteq> {}"
-      using *(3)[OF kp] by auto
-  }
+    using assms finite_subset by blast
+next
+  fix k
+  assume "k \<in> q"
+  show "k \<subseteq> \<Union>q"
+    using \<open>k \<in> q\<close> by auto
+  show "\<exists>a b. k = cbox a b" "k \<noteq> {}"
+    using assms \<open>k \<in> q\<close> by blast+
+next
   fix k1 k2
   assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
-  then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
-    using assms(2) by auto
-  show "interior k1 \<inter> interior k2 = {}"
-    using *(5)[OF **] by auto
+  then show "interior k1 \<inter> interior k2 = {}"
+    using assms by blast
 qed auto
 
 lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
-  unfolding division_of_def by auto
+  by blast
 
 lemma division_inter:
   fixes s1 s2 :: "'a::euclidean_space set"
@@ -379,25 +314,20 @@
     ultimately show "finite ?A" by auto
     have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
       by auto
-    show "\<Union>?A = s1 \<inter> s2"
+    show UA: "\<Union>?A = s1 \<inter> s2"
       unfolding * 
       using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
     {
       fix k
-      assume "k \<in> ?A"
+      assume kA: "k \<in> ?A"
       then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
         by auto
       then show "k \<noteq> {}"
         by auto
       show "k \<subseteq> s1 \<inter> s2"
-        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
-        unfolding k by auto
-      obtain a1 b1 where k1: "k1 = cbox a1 b1"
-        using division_ofD(4)[OF assms(1) k(2)] by blast
-      obtain a2 b2 where k2: "k2 = cbox a2 b2"
-        using division_ofD(4)[OF assms(2) k(3)] by blast
+        using UA kA by blast
       show "\<exists>a b. k = cbox a b"
-        unfolding k k1 k2 unfolding Int_interval by auto
+        using k by (metis (no_types, lifting) Int_interval assms division_ofD(4))
     }
     fix k1 k2
     assume "k1 \<in> ?A"
@@ -407,17 +337,9 @@
     then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
       by auto
     assume "k1 \<noteq> k2"
-    then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
-      unfolding k1 k2 by auto
-    have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
-      interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
-      interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
-      interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
-    show "interior k1 \<inter> interior k2 = {}"
+    then show "interior k1 \<inter> interior k2 = {}"
       unfolding k1 k2
-      apply (rule *)
-      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
-      done
+      using assms division_ofD(5) k1 k2 by auto
   qed
 qed
 
@@ -439,33 +361,20 @@
 
 lemma elementary_Int:
   fixes s t :: "'a::euclidean_space set"
-  assumes "p1 division_of s"
-    and "p2 division_of t"
+  assumes "p1 division_of s" and "p2 division_of t"
   shows "\<exists>p. p division_of (s \<inter> t)"
 using assms division_inter by blast
 
 lemma elementary_Inter:
-  assumes "finite f"
-    and "f \<noteq> {}"
-    and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
-  shows "\<exists>p. p division_of (\<Inter>f)"
+  assumes "finite \<F>"
+    and "\<F> \<noteq> {}"
+    and "\<forall>s\<in>\<F>. \<exists>p. p division_of (s::('a::euclidean_space) set)"
+  shows "\<exists>p. p division_of (\<Inter>\<F>)"
   using assms
-proof (induct f rule: finite_induct)
-  case (insert x f)
-  show ?case
-  proof (cases "f = {}")
-    case True
-    then show ?thesis
-      unfolding True using insert by auto
-  next
-    case False
-    obtain p where "p division_of \<Inter>f"
-      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
-    moreover obtain px where "px division_of x"
-      using insert(5)[rule_format,OF insertI1] ..
-    ultimately show ?thesis
-      by (simp add: elementary_Int Inter_insert)
-  qed
+proof (induct \<F> rule: finite_induct)
+  case (insert x \<F>)
+  then show ?case
+    by (metis cInf_singleton complete_lattice_class.Inf_insert elementary_Int insert_iff)
 qed auto
 
 lemma division_disjoint_union:
@@ -476,40 +385,11 @@
 proof (rule division_ofI)
   note d1 = division_ofD[OF assms(1)]
   note d2 = division_ofD[OF assms(2)]
-  show "finite (p1 \<union> p2)"
-    using d1(1) d2(1) by auto
-  show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
-    using d1(6) d2(6) by auto
-  {
-    fix k1 k2
-    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
-    moreover
-    let ?g="interior k1 \<inter> interior k2 = {}"
-    {
-      assume as: "k1\<in>p1" "k2\<in>p2"
-      have ?g
-        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
-        using assms(3) by blast
-    }
-    moreover
-    {
-      assume as: "k1\<in>p2" "k2\<in>p1"
-      have ?g
-        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
-        using assms(3) by blast
-    }
-    ultimately show ?g
-      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
-  }
-  fix k
-  assume k: "k \<in> p1 \<union> p2"
-  show "k \<subseteq> s1 \<union> s2"
-    using k d1(2) d2(2) by auto
-  show "k \<noteq> {}"
-    using k d1(3) d2(3) by auto
-  show "\<exists>a b. k = cbox a b"
-    using k d1(4) d2(4) by auto
-qed
+  fix k1 k2
+  assume "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
+  with assms show "interior k1 \<inter> interior k2 = {}"
+    by (smt (verit, best) IntE Un_iff disjoint_iff_not_equal division_ofD(2) division_ofD(5) inf.orderE interior_Int)
+qed (use division_ofD assms in auto)
 
 lemma partial_division_extend_1:
   fixes a b c d :: "'a::euclidean_space"
@@ -533,71 +413,59 @@
     show "finite p"
       unfolding p_def by (auto intro!: finite_PiE)
     {
-      fix k
-      assume "k \<in> p"
-      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
+      fix K
+      assume "K \<in> p"
+      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "K = ?B f"
         by (auto simp: p_def)
-      then show "\<exists>a b. k = cbox a b"
-        by auto
-      have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
-      proof (simp add: k box_eq_empty subset_box not_less, safe)
-        fix i :: 'a
-        assume i: "i \<in> Basis"
-        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
-          by (auto simp: PiE_iff)
-        with i ord[of i]
-        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
-          by auto
-      qed
-      then show "k \<noteq> {}" "k \<subseteq> cbox a b"
+      then show "\<exists>a b. K = cbox a b"
         by auto
       {
         fix l
         assume "l \<in> p"
         then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
           by (auto simp: p_def)
-        assume "l \<noteq> k"
+        assume "l \<noteq> K"
         have "\<exists>i\<in>Basis. f i \<noteq> g i"
-        proof (rule ccontr)
-          assume "\<not> ?thesis"
-          with f g have "f = g"
-            by (auto simp: PiE_iff extensional_def fun_eq_iff)
-          with \<open>l \<noteq> k\<close> show False
-            by (simp add: l k)
-        qed
+          using \<open>l \<noteq> K\<close> l k f g by auto
         then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
         then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
-                  "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
+          "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
           using f g by (auto simp: PiE_iff)
-        with * ord[of i] show "interior l \<inter> interior k = {}"
+        with * ord[of i] show "interior l \<inter> interior K = {}"
           by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
       }
-      note \<open>k \<subseteq> cbox a b\<close>
+      have "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
+        if "i \<in> Basis" for i
+      proof -
+        have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
+          using that f by (auto simp: PiE_iff)
+        with that ord[of i]
+        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
+          by auto
+      qed
+      then show "K \<noteq> {}" "K \<subseteq> cbox a b"
+        by (auto simp add: k box_eq_empty subset_box not_less)      
     }
     moreover
-    {
-      fix x assume x: "x \<in> cbox a b"
-      have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
-      proof
-        fix i :: 'a
-        assume "i \<in> Basis"
-        with x ord[of i]
+    have "\<exists>k\<in>p. x \<in> k" if x: "x \<in> cbox a b" for x
+    proof -
+      have "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}" if "i \<in> Basis" for i
+      proof -
         have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
             (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
+          using that x ord[of i]
           by (auto simp: cbox_def)
         then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
           by auto
       qed
       then obtain f where
         f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
-        unfolding bchoice_iff ..
-      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
-        by auto
-      moreover from f have "x \<in> ?B (restrict f Basis)"
+        by metis 
+      moreover from f have "x \<in> ?B (restrict f Basis)" "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a,c), (c,d), (d,b)}"
         by (auto simp: mem_box)
-      ultimately have "\<exists>k\<in>p. x \<in> k"
+      ultimately show ?thesis
         unfolding p_def by blast
-    }
+    qed
     ultimately show "\<Union>p = cbox a b"
       by auto
   qed
@@ -608,14 +476,12 @@
   obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
 proof (cases "p = {}")
   case True
-  obtain q where "q division_of (cbox a b)"
-    by (rule elementary_interval)
   then show ?thesis
-    using True that by blast
+    using elementary_interval that by auto
 next
   case False
   note p = division_ofD[OF assms(1)]
-  have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
+  have "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
   proof
     fix k
     assume kp: "k \<in> p"
@@ -629,64 +495,55 @@
     then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
       unfolding k by auto
   qed
-  obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
-    using bchoice[OF div_cbox] by blast
+  then obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
+    by metis
   have "q x division_of \<Union>(q x)" if x: "x \<in> p" for x
-    apply (rule division_ofI)
-    using division_ofD[OF q(1)[OF x]] by auto
+    using q(1) x by blast
   then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
     by (meson Diff_subset division_of_subset)
-  have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
-    apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
-    apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
-    done
-  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
+  have "\<forall>s\<in>(\<lambda>i. \<Union> (q i - {i})) ` p. \<exists>d. d division_of s"
+    using di by blast
+  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
+    by (meson False elementary_Inter finite_imageI image_is_empty p(1))
   have "d \<union> p division_of cbox a b"
   proof -
     have te: "\<And>S f T. S \<noteq> {} \<Longrightarrow> \<forall>i\<in>S. f i \<union> i = T \<Longrightarrow> T = \<Inter>(f ` S) \<union> \<Union>S" by auto
     have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
     proof (rule te[OF False], clarify)
       fix i
-      assume i: "i \<in> p"
-      show "\<Union>(q i - {i}) \<union> i = cbox a b"
-        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
+      assume "i \<in> p"
+      then show "\<Union>(q i - {i}) \<union> i = cbox a b"
+        by (metis Un_commute complete_lattice_class.Sup_insert division_ofD(6) insert_Diff q)
     qed
-    { fix K
-      assume K: "K \<in> p"
-      note qk=division_ofD[OF q(1)[OF K]]
-      have *: "\<And>u T S. T \<inter> S = {} \<Longrightarrow> u \<subseteq> S \<Longrightarrow> u \<inter> T = {}"
+      have [simp]: "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior K = {}" if K: "K \<in> p" for K
+      proof -
+      note qk = division_ofD[OF q(1)[OF K]]
+      have *: "\<And>U T S. T \<inter> S = {} \<Longrightarrow> U \<subseteq> S \<Longrightarrow> U \<inter> T = {}"
         by auto
-      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior K = {}"
+      show ?thesis
       proof (rule *[OF Int_interior_Union_intervals])
         show "\<And>T. T\<in>q K - {K} \<Longrightarrow> interior K \<inter> interior T = {}"
-          using qk(5) using q(2)[OF K] by auto
+          using K q(2) qk(5) by auto
         show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q K - {K}))"
-          apply (rule interior_mono)+
-          using K by auto
-      qed (use qk in auto)} note [simp] = this
+          by (meson INF_lower K interior_mono)
+      qed (use qk in auto)
+    qed
     show "d \<union> p division_of (cbox a b)"
-      unfolding cbox_eq
-      apply (rule division_disjoint_union[OF d assms(1)])
-      apply (rule Int_interior_Union_intervals)
-      apply (rule p open_interior ballI)+
-      apply simp_all
-      done
+      by (simp add: Int_interior_Union_intervals assms(1) cbox_eq d division_disjoint_union p(1) p(4))
   qed
   then show ?thesis
     by (meson Un_upper2 that)
 qed
 
 lemma elementary_bounded[dest]:
-  fixes S :: "'a::euclidean_space set"
   shows "p division_of S \<Longrightarrow> bounded S"
   unfolding division_of_def by (metis bounded_Union bounded_cbox)
 
 lemma elementary_subset_cbox:
-  "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a (b::'a::euclidean_space)"
+  "p division_of S \<Longrightarrow> \<exists>a b. S \<subseteq> cbox a b"
   by (meson bounded_subset_cbox_symmetric elementary_bounded)
 
 proposition division_union_intervals_exists:
-  fixes a b :: "'a::euclidean_space"
   assumes "cbox a b \<noteq> {}"
   obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
 proof (cases "cbox c d = {}")
@@ -707,26 +564,19 @@
     obtain p where pd: "p division_of cbox c d" and "cbox u v \<in> p"
       by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
     note p = this division_ofD[OF pd]
-    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
-      apply (rule arg_cong[of _ _ interior])
-      using p(8) uv by auto
+    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v) \<inter> interior (\<Union>(p - {cbox u v}))"
+      by (metis Diff_subset Int_absorb1 Int_assoc Sup_subset_mono interior_Int p(8) uv)
     also have "\<dots> = {}"
-      unfolding interior_Int
-      apply (rule Int_interior_Union_intervals)
       using p(6) p(7)[OF p(2)] \<open>finite p\<close>
-      apply auto
-      done
-    finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
+      by (intro Int_interior_Union_intervals) auto
+    finally have disj: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" 
+      by simp
     have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
       using p(8) unfolding uv[symmetric] by auto
     have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
-    proof -
-      have "{cbox a b} division_of cbox a b"
-        by (simp add: assms division_of_self)
-      then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
-        by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
-    qed
-    with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
+      by (metis Diff_subset assms disj division_disjoint_union division_of_self division_of_subset insert_is_Un p(8) pd)
+    with that[of "p - {cbox u v}"] show ?thesis 
+      by (simp add: cbe)
   qed
 qed
 
@@ -735,7 +585,7 @@
     and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
     and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
   shows "\<Union>f division_of \<Union>(\<Union>f)"
-  using assms  by (auto intro!: division_ofI)
+  using assms by (auto intro!: division_ofI)
 
 lemma elementary_union_interval:
   fixes a b :: "'a::euclidean_space"
@@ -756,21 +606,13 @@
   proof (cases "interior (cbox a b) = {}")
     case True
     show ?thesis
-      apply (rule that [of "insert (cbox a b) p", OF division_ofI])
-      using pdiv(1-4) True False apply auto
-       apply (metis IntI equals0D pdiv(5))
-      by (metis disjoint_iff_not_equal pdiv(5))
+      by (metis True assms division_disjoint_union elementary_interval inf_bot_left that)
   next
-    case False  
+    case nonempty: False  
     have "\<forall>K\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> K)"
-    proof
-      fix K
-      assume kp: "K \<in> p"
-      from pdiv(4)[OF kp] obtain c d where "K = cbox c d" by blast
-      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> K)"
-        by (meson \<open>cbox a b \<noteq> {}\<close> division_union_intervals_exists)
-    qed
-    from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
+      by (metis \<open>cbox a b \<noteq> {}\<close> division_union_intervals_exists pdiv(4))
+    then obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" 
+      by metis
     note q = division_ofD[OF this[rule_format]]
     let ?D = "\<Union>{insert (cbox a b) (q K) | K. K \<in> p}"
     show thesis
@@ -814,11 +656,11 @@
           by (metis \<open>interior (cbox a b) \<noteq> {}\<close> K q(2) x interior_subset_union_intervals)
         moreover
         obtain c d where c_d: "K' = cbox c d"
-          using q(4)[OF x'(2,1)] by blast
+          using q(4) x'(1) x'(2) by presburger
         have "interior K' \<inter> interior (cbox a b) = {}"
           using as'(2) q(5) x' by blast
         then have "interior K' \<subseteq> interior x'"
-          by (metis \<open>interior (cbox a b) \<noteq> {}\<close> c_d interior_subset_union_intervals q(2) x'(1) x'(2))
+          by (metis nonempty c_d interior_subset_union_intervals q(2) x')
         moreover have "interior x \<inter> interior x' = {}"
           by (meson False assms division_ofD(5) x'(2) x(2))
         ultimately show ?thesis
@@ -831,39 +673,34 @@
 
 
 lemma elementary_unions_intervals:
-  assumes fin: "finite f"
-    and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
-  obtains p where "p division_of (\<Union>f)"
+  assumes fin: "finite \<F>"
+    and "\<And>s. s \<in> \<F> \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
+  obtains p where "p division_of (\<Union>\<F>)"
 proof -
-  have "\<exists>p. p division_of (\<Union>f)"
-  proof (induct_tac f rule:finite_subset_induct)
+  have "\<exists>p. p division_of (\<Union>\<F>)"
+  proof (induct_tac \<F> rule:finite_subset_induct)
     show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
   next
     fix x F
-    assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
-    from this(3) obtain p where p: "p division_of \<Union>F" ..
-    from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
-    have *: "\<Union>F = \<Union>p"
-      using division_ofD[OF p] by auto
-    show "\<exists>p. p division_of \<Union>(insert x F)"
-      using elementary_union_interval[OF p[unfolded *], of a b]
-      unfolding Union_insert x * by metis
-  qed (insert assms, auto)
+    assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>\<F>"
+    then obtain a b where x: "x = cbox a b"
+      by (meson assms(2)) 
+    then show "\<exists>p. p division_of \<Union>(insert x F)"
+      using elementary_union_interval by (metis Union_insert as(3) division_ofD(6))
+  qed (use assms in auto)
   then show ?thesis
     using that by auto
 qed
 
 lemma elementary_union:
-  fixes S T :: "'a::euclidean_space set"
   assumes "ps division_of S" "pt division_of T"
   obtains p where "p division_of (S \<union> T)"
 proof -
-  have *: "S \<union> T = \<Union>ps \<union> \<Union>pt"
+  have "S \<union> T = \<Union>ps \<union> \<Union>pt"
     using assms unfolding division_of_def by auto
+  with elementary_unions_intervals[of "ps \<union> pt"] assms 
   show ?thesis
-    apply (rule elementary_unions_intervals[of "ps \<union> pt"])
-    using assms apply auto
-    by (simp add: * that)
+    by (metis Un_iff Union_Un_distrib division_of_def finite_Un that)
 qed
 
 lemma partial_division_extend:
@@ -881,10 +718,7 @@
     by (metis ab dual_order.trans partial_division_extend_interval divp(6))
   note r1 = this division_ofD[OF this(2)]
   obtain p' where "p' division_of \<Union>(r1 - p)"
-    apply (rule elementary_unions_intervals[of "r1 - p"])
-    using r1(3,6)
-      apply auto
-    done
+    by (metis Diff_subset division_of_subset r1(2) r1(8))
   then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
     by (metis assms(2) divq(6) elementary_Int)
   {
@@ -894,11 +728,7 @@
       unfolding r1 using ab
       by (meson division_contains r1(2) subsetCE)
     moreover have "R \<notin> p"
-    proof
-      assume "R \<in> p"
-      then have "x \<in> S" using divp(2) r by auto
-      then show False using x by auto
-    qed
+      using divp(6) r(2) x(2) by blast
     ultimately have "x\<in>\<Union>(r1 - p)" by auto
   }
   then have Teq: "T = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
@@ -923,14 +753,11 @@
   then have div: "p \<union> r2 division_of \<Union>p \<union> \<Union>(r1 - p) \<inter> \<Union>q"
     by (simp add: assms(1) division_disjoint_union divp(6) r2)
   show ?thesis
-    apply (rule that[of "p \<union> r2"])
-     apply (auto simp: div Teq)
-    done
+    by (metis Teq div sup_ge1 that)
 qed
 
 
 lemma division_split:
-  fixes a :: "'a::euclidean_space"
   assumes "p division_of (cbox a b)"
     and k: "k\<in>Basis"
   shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of(cbox a b \<inter> {x. x\<bullet>k \<le> c})"
@@ -954,11 +781,10 @@
       using l p(2) uv by force
     show  "K \<noteq> {}"
       by (simp add: l)
-    show  "\<exists>a b. K = cbox a b"
-      apply (simp add: l uv p(2-3)[OF l(2)])
-      apply (subst interval_split[OF k])
-      apply (auto intro: order.trans)
-      done
+    have "\<exists>a b. cbox u v \<inter> {x. x \<bullet> k \<le> c} = cbox a b"
+      unfolding interval_split[OF k] by (auto intro: order.trans)
+    then show  "\<exists>a b. K = cbox a b"
+      by (simp add: l(1) uv)
     fix K'
     assume "K' \<in> ?p1"
     then obtain l' where l': "K' = l' \<inter> {x. x \<bullet> k \<le> c}" "l' \<in> p" "l' \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
@@ -978,11 +804,10 @@
       using l p(2) uv by force
     show  "K \<noteq> {}"
       by (simp add: l)
-    show  "\<exists>a b. K = cbox a b"
-      apply (simp add: l uv p(2-3)[OF l(2)])
-      apply (subst interval_split[OF k])
-      apply (auto intro: order.trans)
-      done
+    have "\<exists>a b. cbox u v \<inter> {x. c \<le> x \<bullet> k} = cbox a b"
+      unfolding interval_split[OF k] by (auto intro: order.trans)
+    then show  "\<exists>a b. K = cbox a b"
+      by (simp add: l(1) uv)
     fix K'
     assume "K' \<in> ?p2"
     then obtain l' where l': "K' = l' \<inter> {x. c \<le> x \<bullet> k}" "l' \<in> p" "l' \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
@@ -1037,9 +862,9 @@
     and "(\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
   shows "s tagged_division_of i"
   unfolding tagged_division_of
-  using assms  by fastforce
+  using assms by fastforce
 
-lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
+lemma tagged_division_ofD[dest]: 
   assumes "s tagged_division_of i"
   shows "finite s"
     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> x \<in> K"
@@ -1057,18 +882,14 @@
   note assm = tagged_division_ofD[OF assms]
   show "\<Union>(snd ` s) = i" "finite (snd ` s)"
     using assm by auto
-  fix k
-  assume k: "k \<in> snd ` s"
-  then obtain xk where xk: "(xk, k) \<in> s"
-    by auto
-  then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
+  fix K
+  assume k: "K \<in> snd ` s"
+  then show "K \<subseteq> i" "K \<noteq> {}" "\<exists>a b. K = cbox a b"
     using assm by fastforce+
-  fix k'
-  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
-  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
-    by auto
-  then show "interior k \<inter> interior k' = {}"
-    using assm(5) k'(2) xk by blast
+  fix K'
+  assume k': "K' \<in> snd ` s" "K \<noteq> K'"
+  then show "interior K \<inter> interior K' = {}"
+    by (metis (no_types, lifting) assms imageE k prod.collapse tagged_division_ofD(5))
 qed
 
 lemma partial_division_of_tagged_division:
@@ -1078,23 +899,18 @@
   note assm = tagged_partial_division_ofD[OF assms]
   show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
     using assm by auto
-  fix k
-  assume k: "k \<in> snd ` s"
-  then obtain xk where xk: "(xk, k) \<in> s"
-    by auto
-  then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
-    using assm by auto
-  fix k'
-  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
-  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
-    by auto
-  then show "interior k \<inter> interior k' = {}"
-    using assm(5) k'(2) xk by auto
+  fix K
+  assume K: "K \<in> snd ` s"
+  then show "K \<noteq> {}" "\<exists>a b. K = cbox a b" "K \<subseteq> \<Union>(snd ` s)"
+    using assm by fastforce+
+  fix K'
+  assume "K' \<in> snd ` s" "K \<noteq> K'"
+  then show "interior K \<inter> interior K' = {}"
+    using assm(5) K by force
 qed
 
 lemma tagged_partial_division_subset:
-  assumes "s tagged_partial_division_of i"
-    and "t \<subseteq> s"
+  assumes "s tagged_partial_division_of i" and "t \<subseteq> s"
   shows "t tagged_partial_division_of i"
   using assms finite_subset[OF assms(2)]
   unfolding tagged_partial_division_of_def
@@ -1116,8 +932,7 @@
   by (rule tagged_division_ofI) auto
 
 lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
-  unfolding box_real[symmetric]
-  by (rule tagged_division_of_self)
+  by (metis box_real(2) tagged_division_of_self)
 
 lemma tagged_division_Un:
   assumes "p1 tagged_division_of s1"
@@ -1131,20 +946,16 @@
     using p1(1) p2(1) by auto
   show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
     using p1(6) p2(6) by blast
-  fix x k
-  assume xk: "(x, k) \<in> p1 \<union> p2"
-  show "x \<in> k" "\<exists>a b. k = cbox a b"
-    using xk p1(2,4) p2(2,4) by auto
-  show "k \<subseteq> s1 \<union> s2"
-    using xk p1(3) p2(3) by blast
-  fix x' k'
-  assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
+  fix x K
+  assume xK: "(x, K) \<in> p1 \<union> p2"
+  show "x \<in> K" "\<exists>a b. K = cbox a b" "K \<subseteq> s1 \<union> s2"
+    using xK p1 p2 by auto
+  fix x' K'
+  assume xk': "(x', K') \<in> p1 \<union> p2" "(x, K) \<noteq> (x', K')"
   have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
     using assms(3) interior_mono by blast
-  show "interior k \<inter> interior k' = {}"
-    apply (cases "(x, k) \<in> p1")
-    apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
-    by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
+  with assms show "interior K \<inter> interior K' = {}"
+    by (metis Un_iff inf_commute p1(3) p2(3) tagged_division_ofD(5) xK xk')
 qed
 
 lemma tagged_division_Union:
@@ -1186,21 +997,16 @@
 lemma tagged_partial_division_of_Union_self:
   assumes "p tagged_partial_division_of s"
   shows "p tagged_division_of (\<Union>(snd ` p))"
-  apply (rule tagged_division_ofI)
   using tagged_partial_division_ofD[OF assms]
-  apply auto
-  done
+  by (intro tagged_division_ofI) auto
 
 lemma tagged_division_of_union_self:
   assumes "p tagged_division_of s"
   shows "p tagged_division_of (\<Union>(snd ` p))"
-  apply (rule tagged_division_ofI)
   using tagged_division_ofD[OF assms]
-  apply auto
-  done
+  by (intro tagged_division_ofI) auto
 
 lemma tagged_division_Un_interval:
-  fixes a :: "'a::euclidean_space"
   assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
     and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
     and k: "k \<in> Basis"
@@ -1208,13 +1014,10 @@
 proof -
   have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
     by auto
-  show ?thesis
-    apply (subst *)
-    apply (rule tagged_division_Un[OF assms(1-2)])
-    unfolding interval_split[OF k] interior_cbox
-    using k
-    apply (auto simp add: box_def elim!: ballE[where x=k])
-    done
+  have "interior (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<inter> interior (cbox a b \<inter> {x. c \<le> x \<bullet> k}) = {}"
+    using k by (force simp: interval_split[OF k] box_def)
+  with assms show ?thesis
+    by (metis "*" tagged_division_Un)
 qed
 
 lemma tagged_division_Un_interval_real:
@@ -1223,35 +1026,23 @@
     and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
     and k: "k \<in> Basis"
   shows "(p1 \<union> p2) tagged_division_of {a .. b}"
-  using assms
-  unfolding box_real[symmetric]
-  by (rule tagged_division_Un_interval)
+  using assms by (metis box_real(2) tagged_division_Un_interval)
 
 lemma tagged_division_split_left_inj:
   assumes d: "d tagged_division_of i"
-  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
-  and "K1 \<noteq> K2"
-  and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
-    shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-proof -
-  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
-    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
-  then show ?thesis
-    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
+    and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+    and "K1 \<noteq> K2"
+    and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
+  shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+  by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)
 
 lemma tagged_division_split_right_inj:
   assumes d: "d tagged_division_of i"
-  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
-  and "K1 \<noteq> K2"
-  and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
-    shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-proof -
-  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
-    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
-  then show ?thesis
-    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
+    and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+    and "K1 \<noteq> K2"
+    and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+  shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+  by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)
 
 lemma (in comm_monoid_set) over_tagged_division_lemma:
   assumes "p tagged_division_of i"
@@ -1272,14 +1063,10 @@
       using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
     have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
       using \<open>x \<in> p\<close> \<open>x \<noteq> y\<close> \<open>snd x = snd y\<close> [symmetric] by auto
-    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
-      by (intro assm(5)[of "fst x" _ "fst y"]) auto
-    then have "box a b = {}"
-      unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
-    then have "d (cbox a b) = \<^bold>1"
-      using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
+    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "box a b = {}"
+      by (metis \<open>snd x = snd y\<close> ab assm(5) inf.idem interior_cbox prod.collapse)
     then show "d (snd x) = \<^bold>1"
-      unfolding ab by auto
+      by (simp add: ab assms(2))
   qed
 qed
 
@@ -1311,11 +1098,8 @@
     by standard (auto simp: lift_option_def ac_simps split: bind_split)
 qed
 
-lemma comm_monoid_and: "comm_monoid HOL.conj True"
-  by standard auto
-
 lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
-  by (rule comm_monoid_set.intro) (fact comm_monoid_and)
+  by (simp add: comm_monoid_set.intro conj.comm_monoid_axioms)
 
 
 paragraph \<open>Misc\<close>
@@ -1323,9 +1107,7 @@
 lemma interval_real_split:
   "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
   "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
-  apply (metis Int_atLeastAtMostL1 atMost_def)
-  apply (metis Int_atLeastAtMostL2 atLeast_def)
-  done
+  by auto
 
 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
   by (meson zero_less_one)
@@ -1375,16 +1157,11 @@
   proof -
     obtain u v where l: "l = cbox u v"
       using \<open>l \<in> d\<close> assms(1) by blast
-    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
-      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+    have "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
       using l using that(6) unfolding box_ne_empty[symmetric] by auto
-    show ?thesis
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using that(1-3,5) \<open>x \<in> Basis\<close>
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
-      apply (auto split: if_split_asm)
-      done
+    then show ?thesis
+      using that \<open>x \<in> Basis\<close> unfolding l interval_split[OF k] 
+      by (force split: if_split_asm)
   qed
   moreover have "\<And>x y. \<lbrakk>y < (if x = k then c else b \<bullet> x)\<rbrakk> \<Longrightarrow> y < b \<bullet> x"
     using \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
@@ -1403,16 +1180,11 @@
   proof -
     obtain u v where l: "l = cbox u v"
       using \<open>l \<in> d\<close> assm(4) by blast
-    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
-      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+    have "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
       using l using that(6) unfolding box_ne_empty[symmetric] by auto
-    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using that(1-3,5) \<open>x \<in> Basis\<close>
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
-      apply (auto split: if_split_asm)
-      done
+    then show "\<exists>i\<in>d. interval_lowerbound i \<bullet> x = y \<or> interval_upperbound i \<bullet> x = y"
+      using that \<open>x \<in> Basis\<close> unfolding l interval_split[OF k] 
+      by (force split: if_split_asm)
   qed
   ultimately show ?t2
     unfolding division_points_def interval_split[OF k, of a b]
@@ -1520,8 +1292,6 @@
   shows "(\<lambda>l. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e}) ` {l\<in>p. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
          division_of  (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
 proof -
-  have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
-    by auto
   have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
     by auto
   note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
@@ -1533,7 +1303,8 @@
       apply (rule equalityI)
       apply blast
       apply clarsimp
-      apply (rule_tac x="xa \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
+      apply (rename_tac S)
+      apply (rule_tac x="S \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
       apply auto
       done
     by (simp add: interval_split k interval_doublesplit)
@@ -1547,16 +1318,8 @@
     and Basis_imp: "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
 begin
 
-lemma empty [simp]:
-  "g {} = \<^bold>1"
-proof -
-  have *: "cbox One (-One) = ({}::'b set)"
-    by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
-  moreover have "box One (-One) = ({}::'b set)"
-    using box_subset_cbox[of One "-One"] by (auto simp: *)
-  ultimately show ?thesis
-    using box_empty_imp [of One "-One"] by simp
-qed
+lemma empty [simp]: "g {} = \<^bold>1"
+  by (metis box_empty_imp box_subset_cbox empty_as_interval subset_empty)
        
 lemma division:
   "F g d = g (cbox a b)" if "d division_of (cbox a b)"
@@ -1566,21 +1329,22 @@
   using that proof (induction C arbitrary: a b d rule: less_induct)
     case (less a b d)
     show ?case
-    proof cases
-      assume "box a b = {}"
+    proof (cases "box a b = {}")
+      case True
       { fix k assume "k\<in>d"
         then obtain a' b' where k: "k = cbox a' b'"
           using division_ofD(4)[OF less.prems] by blast
-        with \<open>k\<in>d\<close> division_ofD(2)[OF less.prems] have "cbox a' b' \<subseteq> cbox a b"
-          by auto
+        then have "cbox a' b' \<subseteq> cbox a b"
+          using \<open>k \<in> d\<close> less.prems by blast
         then have "box a' b' \<subseteq> box a b"
           unfolding subset_box by auto
         then have "g k = \<^bold>1"
-          using box_empty_imp [of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
-      then show "box a b = {} \<Longrightarrow> F g d = g (cbox a b)"
+          using box_empty_imp [of a' b'] k by (simp add: True)
+      }
+      with True show "F g d = g (cbox a b)"
         by (auto intro!: neutral simp: box_empty_imp)
     next
-      assume "box a b \<noteq> {}"
+      case False
       then have ab: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" and ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
         by (auto simp: box_ne_empty)
       show "F g d = g (cbox a b)"
@@ -1600,11 +1364,10 @@
           note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
           moreover
           have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
-            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
-            apply (metis j subset_box(1) uv(1))
-            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
+            by (meson as division_ofD(2) j less.prems subset_box(1) uv(1))+
           ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
-            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
+            using uv(2) by force
+        }
         then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
           (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
           unfolding forall_in_division[OF less.prems] by blast
@@ -1624,9 +1387,9 @@
           proof safe
             fix j :: 'b
             assume j: "j \<in> Basis"
-            note i(2)[unfolded uv mem_box,rule_format,of j]
+            note i(2)[unfolded uv mem_box]
             then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
-              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
+              by (smt (verit) False box_midpoint j mem_box(1) uv(2))+
           qed
           then have "i = cbox a b" using uv by auto
           then show ?thesis using i by auto
@@ -1650,17 +1413,11 @@
             unfolding euclidean_eq_iff[where 'a='b] by auto
           then have "u\<bullet>j = v\<bullet>j"
             using uv(2)[rule_format,OF j] by auto
-          then have "box u v = {}"
-            using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
           then show "g x = \<^bold>1"
-            unfolding uv(1) by (rule box_empty_imp)
+            by (smt (verit) box_empty_imp box_eq_empty(1) j uv(1))
         qed
         then show "F g d = g (cbox a b)"
-          using division_ofD[OF less.prems]
-          apply (subst deq)
-          apply (subst insert)
-          apply auto
-          done
+          by (metis deq division_of_finite insert_Diff_single insert_remove less.prems right_neutral)
       next
         case False
         then have "\<exists>x. x \<in> division_points (cbox a b) d"
@@ -1748,12 +1505,7 @@
 proposition tagged_division:
   assumes "d tagged_division_of (cbox a b)"
   shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
-proof -
-  have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
-    using assms box_empty_imp by (rule over_tagged_division_lemma)
-  then show ?thesis
-    unfolding assms [THEN division_of_tagged_division, THEN division] .
-  qed
+  by (metis assms box_empty_imp division division_of_tagged_division over_tagged_division_lemma)
 
 end
 
@@ -1778,14 +1530,14 @@
       from that have [simp]: "k = 1"
         by simp
       from neutral [of 0 1] neutral [of a a for a] coalesce_less
-  have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
-    "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
-    by auto
+      have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
+        "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+        by auto
       have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
-    by (auto simp: min_def max_def le_less)
+        by (auto simp: min_def max_def le_less)
       then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
         by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
-qed
+    qed
   qed
   show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
     and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
@@ -1795,17 +1547,7 @@
 
 lemma coalesce_less_eq:
   "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
-  proof (cases "c = a \<or> c = b")
-    case False
-  with that have "a < c" "c < b"
-    by auto
-    then show ?thesis
-    by (rule coalesce_less)
-  next
-    case True
-  with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
-    by safe simp_all
-    qed
+  by (metis coalesce_less commute left_neutral less_eq_real_def neutral that)
 
 end
 
@@ -1819,22 +1561,22 @@
     show "g {a..b} = z" if "b \<le> a" for a b
       using that box_empty_imp by simp
     show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
-      using that
-    using Basis_imp [of 1 a b c]
+      using that Basis_imp [of 1 a b c]
       by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
-qed
+  qed
 qed
 
 
 subsection \<open>Special case of additivity we need for the FTC\<close>
 (*fix add explanation here *)
+
 lemma additive_tagged_division_1:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
     and "p tagged_division_of {a..b}"
-  shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
+  shows "sum (\<lambda>(x,K). f(Sup K) - f(Inf K)) p = f b - f a"
 proof -
-  let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
+  let ?f = "(\<lambda>K::real set. if K = {} then 0 else f(interval_upperbound K) - f(interval_lowerbound K))"
   interpret operative_real plus 0 ?f
     rewrites "comm_monoid_set.F (+) 0 = sum"
     by standard[1] (auto simp add: sum_def)
@@ -1843,12 +1585,7 @@
   have **: "cbox a b \<noteq> {}"
     using assms(1) by auto
   then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
-    proof -
-      have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
-        using assms by auto
-      then show ?thesis
-        using p_td assms by (simp add: tagged_division) 
-    qed 
+    using assms(2) tagged_division by force
   then show ?thesis
     using assms by (auto intro!: sum.cong)
 qed
@@ -1897,12 +1634,16 @@
   obtain pfn where pfn:
     "\<And>x. x \<in> I \<Longrightarrow> pfn x tagged_division_of x"
     "\<And>x. x \<in> I \<Longrightarrow> d fine pfn x"
-    using bchoice[OF assms(2)] by auto
+    using assms by metis
   show thesis
-    apply (rule_tac p="\<Union>(pfn ` I)" in that)
-    using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
-    by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
+  proof
+    show "\<Union> (pfn ` I) tagged_division_of i"
+      using assms pfn(1) tagged_division_Union by force
+    show "d fine \<Union> (pfn ` I)"
+      by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
+  qed
 qed
+
 (* FIXME structure here, do not have one lemma in each subsection *)
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>The set we're concerned with must be closed\<close>
@@ -1910,9 +1651,11 @@
 lemma division_of_closed:
   fixes i :: "'n::euclidean_space set"
   shows "s division_of i \<Longrightarrow> closed i"
-  unfolding division_of_def by fastforce
+  by blast
 (* FIXME structure here, do not have one lemma in each subsection *)
+
 subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
+
 (* FIXME  move? *)
 lemma interval_bisection_step:
   fixes type :: "'a::euclidean_space"
@@ -1952,11 +1695,10 @@
       assume "x \<in> ?A"
       then obtain c d
         where x:  "x = cbox c d"
-          "\<And>i. i \<in> Basis \<Longrightarrow>
-                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
+          "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
         by blast
       have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
-           "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
+        "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
         using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
       then show "x \<in> ?B"
         unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
@@ -1968,7 +1710,7 @@
     assume "S \<in> ?A"
     then obtain c d
       where s: "S = cbox c d"
-               "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
+        "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
       by blast
     show "P S"
       unfolding s using ab s(2) by (fastforce intro!: that)
@@ -1986,8 +1728,7 @@
     then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
       unfolding euclidean_eq_iff[where 'a='a] by auto
     then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
-      using s(2) t(2) apply fastforce
-      using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
+      using s(2) t(2) by fastforce+
     have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
       by auto
     show "interior S \<inter> interior T = {}"
@@ -1995,10 +1736,10 @@
     proof (rule *)
       fix x
       assume "x \<in> box c d" "x \<in> box e f"
-      then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
-        unfolding mem_box using i'  by force+
-      show False  using s(2)[OF i'] t(2)[OF i'] and i x  
-        by auto
+      then have "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
+        unfolding mem_box using i' by force+
+      with i i' show False
+        using s(2) t(2) by fastforce
     qed
   qed
   also have "\<Union>?A = cbox a b"
@@ -2024,7 +1765,7 @@
       by (force simp add: mem_box)
   qed
   finally show thesis
-      by (metis (no_types, lifting) assms(3) that)
+    by (metis (no_types, lifting) assms(3) that)
 qed
 
 lemma interval_bisection:
@@ -2066,9 +1807,10 @@
             snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
             2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)" by metis
   define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
-  have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
-    (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
-    2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
+  have [simp]: "A 0 = a" "B 0 = b" 
+    and ABRAW: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
+                  (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
+                  2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
   proof -
     show "A 0 = a" "B 0 = b"
       unfolding ab_def by auto
@@ -2080,13 +1822,9 @@
         unfolding S using \<open>\<not> P (cbox a b)\<close> f by auto
     next
       case (Suc n)
-      show ?case
+      then show ?case
         unfolding S
-        apply (rule f[rule_format])
-        using Suc
-        unfolding S
-        apply auto
-        done
+        by (force intro!: f[rule_format])
     qed
   qed
   then have AB: "A(n)\<bullet>i \<le> A(Suc n)\<bullet>i" "A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i" 
@@ -2109,10 +1847,9 @@
       also have "\<dots> \<le> sum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
       proof (rule sum_mono)
         fix i :: 'a
-        assume i: "i \<in> Basis"
-        show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
-          using xy[unfolded mem_box,THEN bspec, OF i]
-          by (auto simp: inner_diff_left)
+        assume "i \<in> Basis"
+        with xy show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
+          by (smt (verit, best) inner_diff_left mem_box(2))
       qed
       also have "\<dots> \<le> sum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
         unfolding sum_divide_distrib
@@ -2136,23 +1873,21 @@
       finally show "dist x y < e" .
     qed
   qed
-  {
-    fix n m :: nat
-    assume "m \<le> n" then have "cbox (A n) (B n) \<subseteq> cbox (A m) (B m)"
-    proof (induction rule: inc_induct)
-      case (step i)
-      show ?case
-        using AB by (intro order_trans[OF step.IH] subset_box_imp) auto
-    qed simp
-  } note ABsubset = this
+  have ABsubset: "cbox (A n) (B n) \<subseteq> cbox (A m) (B m)" if "m \<le> n" for m n
+    using that
+  proof (induction rule: inc_induct)
+    case (step i) show ?case
+      by (smt (verit, ccfv_SIG) ABRAW in_mono mem_box(2) step.IH subsetI)
+  qed simp
   have "\<And>n. cbox (A n) (B n) \<noteq> {}"
     by (meson AB dual_order.trans interval_not_empty)
   then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
     using decreasing_closed_nest [OF closed_cbox] ABsubset interv by blast
   show thesis
-  proof (rule that[rule_format, of x0])
-    show "x0\<in>cbox a b"
+  proof (intro that strip)
+    show "x0 \<in> cbox a b"
       using \<open>A 0 = a\<close> \<open>B 0 = b\<close> x0 by blast
+  next
     fix e :: real
     assume "e > 0"
     from interv[OF this] obtain n
@@ -2170,17 +1905,14 @@
     moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
       using ABsubset \<open>A 0 = a\<close> \<open>B 0 = b\<close> by blast
     ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
-      apply (rule_tac x="A n" in exI)
-      apply (rule_tac x="B n" in exI)
-      apply (auto simp: x0)
-      done
+      by (meson x0)
   qed
 qed
 
 
 subsection \<open>Cousin's lemma\<close>
 
-lemma fine_division_exists: (*FIXME rename(?) *)
+lemma fine_division_exists: 
   fixes a b :: "'a::euclidean_space"
   assumes "gauge g"
   obtains p where "p tagged_division_of (cbox a b)" "g fine p"
@@ -2199,23 +1931,21 @@
           cbox c d \<subseteq> ball x e \<and>
           cbox c d \<subseteq> (cbox a b) \<and>
           \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
-    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
-    apply (simp add: fine_def)
-    apply (metis tagged_division_Un fine_Un)
-    apply auto
-    done
+  proof (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> _ p", OF _ _ False])
+    show "\<exists>p. p tagged_division_of {} \<and> g fine p"
+      by (simp add: fine_def)
+  qed (meson tagged_division_Un fine_Un)+
   obtain e where e: "e > 0" "ball x e \<subseteq> g x"
-    using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
-  from x(2)[OF e(1)]
-  obtain c d where c_d: "x \<in> cbox c d"
+    by (meson assms gauge_def openE)
+  then obtain c d where c_d: "x \<in> cbox c d"
                         "cbox c d \<subseteq> ball x e"
                         "cbox c d \<subseteq> cbox a b"
                         "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
-    by blast
+    by (meson x(2))
   have "g fine {(x, cbox c d)}"
     unfolding fine_def using e using c_d(2) by auto
   then show ?thesis
-    using tagged_division_of_self[OF c_d(1)] using c_d by auto
+    using tagged_division_of_self[OF c_d(1)] using c_d by simp
 qed
 
 lemma fine_division_exists_real:
@@ -2232,7 +1962,7 @@
     and "gauge d"
   obtains q where "q tagged_division_of (cbox a b)"
     and "d fine q"
-    and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
+    and "\<forall>(x,K) \<in> p. K \<subseteq> d(x) \<longrightarrow> (x,K) \<in> q"
 proof -
   have p: "finite p" "p tagged_partial_division_of (cbox a b)"
     using ptag tagged_division_of_def by blast+
@@ -2250,48 +1980,48 @@
     obtain q1 where q1: "q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}"
                 and "d fine q1"
                 and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p;  k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> q1"
-      using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
-      by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
+      using insert
+      by (metis (mono_tags, lifting) case_prodD subset_insertI tagged_partial_division_subset)
     have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
       unfolding xk by auto
     note p = tagged_partial_division_ofD[OF insert(4)]
     obtain u v where uv: "k = cbox u v"
       using p(4) xk by blast
-    have "finite {k. \<exists>x. (x, k) \<in> p}"
-      apply (rule finite_subset[of _ "snd ` p"])
-      using image_iff apply fastforce
-      using insert.hyps(1) by blast
+    have "{K. \<exists>x. (x, K) \<in> p} \<subseteq> snd ` p"
+      by force
+    then have "finite {K. \<exists>x. (x, K) \<in> p}"
+      using finite_surj insert.hyps(1) by blast
     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
     proof (rule Int_interior_Union_intervals)
       show "open (interior (cbox u v))"
         by auto
-      show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
+      show "\<And>T. T \<in> {K. \<exists>x. (x, K) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
         using p(4) by auto
-      show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
-        by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
+      show "\<And>T. T \<in> {K. \<exists>x. (x, K) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
+        using insert.hyps(2) p(5) uv xk by blast
     qed
     show ?case
     proof (cases "cbox u v \<subseteq> d x")
       case True
       have "{(x, cbox u v)} tagged_division_of cbox u v"
         by (simp add: p(2) uv xk tagged_division_of_self)
-      then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
-        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
-      with True show ?thesis
-        apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
-        using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
-        done
+      then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{K. \<exists>x. (x, K) \<in> insert xk p}"
+        by (smt (verit, best) "*" int q1 tagged_division_Un uv)
+      moreover have "d fine ({(x,cbox u v)} \<union> q1)"
+        using True \<open>d fine q1\<close> fine_def by fastforce
+      ultimately show ?thesis
+        by (metis (no_types, lifting) case_prodI2 insert_iff insert_is_Un q1I uv xk)
     next
       case False
       obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
         using fine_division_exists[OF assms(2)] by blast
       show ?thesis
-        apply (rule_tac x="q2 \<union> q1" in exI)
-        apply (intro conjI)
-        unfolding * uv
-        apply (rule tagged_division_Un q2 q1 int fine_Un)+
-          apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
-        done
+      proof (intro exI conjI)
+        show "q2 \<union> q1 tagged_division_of \<Union> {k. \<exists>x. (x, k) \<in> insert xk p}"
+          by (smt (verit, best) "*" int q1 q2(1) tagged_division_Un uv)
+        show "d fine q2 \<union> q1"
+          by (simp add: \<open>d fine q1\<close> fine_Un q2(2))
+      qed (use False uv xk q1I in auto)
     qed
   qed
   with p obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
@@ -2335,8 +2065,7 @@
     show "\<Union>?D0 \<subseteq> cbox a b"
       apply (simp add: UN_subset_iff)
       apply (intro conjI allI ballI subset_box_imp)
-       apply (simp add: field_simps)
-      apply (auto intro: mult_right_mono aibi)
+       apply (simp add: field_simps aibi mult_right_mono)
       apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem intro: mult_right_mono)
       done
   next
@@ -2352,22 +2081,19 @@
       fix v w m and n::nat
       assume "m \<le> n" \<comment> \<open>WLOG we can assume \<^term>\<open>m \<le> n\<close>, when the first disjunct becomes impossible\<close>
       have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
+        apply (rule ccontr)
         apply (simp add: subset_box disjoint_interval)
-        apply (rule ccontr)
         apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
         apply (drule_tac x=i in bspec, assumption)
         using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
         apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
-         apply (simp_all add: power_add)
-        apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
-        apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
+        apply (metis (no_types, opaque_lifting) power_add mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
         done
       then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
         by meson
     qed auto
     show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
-      apply (erule imageE SigmaE)+
-      using * by simp
+      using * by fastforce
   next
     show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
     proof (simp only: bex_simps split_paired_Bex_Sigma)
@@ -2389,9 +2115,8 @@
               by (meson sum_bounded_above that)
             also have "... = \<epsilon> / 2"
               by (simp add: field_split_simps)
-            also have "... < \<epsilon>"
-              by (simp add: \<open>0 < \<epsilon>\<close>)
-            finally show ?thesis .
+            finally show ?thesis
+              using \<open>0 < \<epsilon>\<close> by linarith 
           qed
           then show ?thesis
             by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
@@ -2404,13 +2129,7 @@
         then have "norm (b - a) < e * 2^n"
           by (auto simp: field_split_simps)
         then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
-        proof -
-          have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
-            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
-          also have "... < e * 2 ^ n"
-            using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
-          finally show ?thesis .
-        qed
+          by (smt (verit, del_insts) Basis_le_norm diff_add_cancel inner_simps(1) that)
         have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
                  for a m n x and y::real
           by auto
@@ -2438,9 +2157,9 @@
             next
               have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
                     a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
-                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
-                  apply (simp_all add: \<open>i \<in> Basis\<close> mem_box field_split_simps)
+                  apply (auto simp: \<open>i \<in> Basis\<close> mem_box field_split_simps)
                 done
               also have "... = x \<bullet> i"
                 using abi_less by (simp add: field_split_simps)
@@ -2449,8 +2168,8 @@
               have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
                 using abi_less by (simp add: field_split_simps)
               also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
+                using aibi [OF \<open>i \<in> Basis\<close>] xab
                 apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
-                using aibi [OF \<open>i \<in> Basis\<close>] xab
                   apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
                 done
               finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
@@ -2540,7 +2259,7 @@
   qed
   let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> \<not>(K \<subseteq> K')}"
   show ?thesis
-  proof (rule that)
+  proof 
     show "countable ?\<D>"
       by (blast intro: countable_subset [OF _ count])
     show "\<Union>?\<D> \<subseteq> cbox a b"
@@ -2597,6 +2316,6 @@
 
 lemma eventually_division_filter_tagged_division:
   "eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
-  unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto
+  using eventually_division_filter by auto
 
 end