# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1679072788 0
# Node ID 48aa9928f090bb97ca2335d5a31ae8857e4b96f9
# Parent  7969fa41439b8daa0aa7c8f534dd3ad7805b2918
Numerous significant simplifications

diff -r 7969fa41439b -r 48aa9928f090 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Fri Mar 17 11:24:52 2023 +0000
+++ b/src/HOL/Analysis/Homotopy.thy	Fri Mar 17 17:06:28 2023 +0000
@@ -156,7 +156,7 @@
   qed
   show ?thesis
     using assms
-    apply (clarsimp simp add: homotopic_with_def)
+    apply (clarsimp simp: homotopic_with_def)
     subgoal for h
       by (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *])
     done
@@ -211,7 +211,7 @@
     show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
     proof 
       fix t show "t\<in>{0..1} \<Longrightarrow> P (\<lambda>x. k (t, x))"
-        by (cases "t \<le> 1/2") (auto simp add: k_def P)
+        by (cases "t \<le> 1/2") (auto simp: k_def P)
     qed
   qed
 qed
@@ -578,7 +578,7 @@
 
 proposition homotopic_paths_join:
     "\<lbrakk>homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q\<rbrakk> \<Longrightarrow> homotopic_paths S (p +++ q) (p' +++ q')"
-  apply (clarsimp simp add: homotopic_paths_def homotopic_with_def)
+  apply (clarsimp simp: homotopic_paths_def homotopic_with_def)
   apply (rename_tac k1 k2)
   apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
   apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
@@ -639,8 +639,8 @@
     show "continuous_on {x \<in> ?A. snd x \<le> 1/2} (\<lambda>t. p (fst t * (2 * snd t)))"
          "continuous_on {x \<in> ?A. 1/2 \<le> snd x} (\<lambda>t. p (fst t * (1 - (2 * snd t - 1))))"
          "continuous_on ?A snd"
-      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp add: mult_le_one)+
-  qed (auto simp add: algebra_simps)
+      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+
+  qed (auto simp: algebra_simps)
   then show ?thesis
     using assms
     apply (subst homotopic_paths_sym_eq)
@@ -1004,7 +1004,7 @@
         by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
       show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \<in> {0..1}" for t 
         using assms
-        unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute)
+        unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute)
     qed (use False in auto)
   qed
   then show ?thesis
@@ -1062,26 +1062,24 @@
   then have "continuous_on ({0..1} \<times> {0..1}) (g \<circ> fst)"
     by (fastforce intro!: continuous_intros)+
   with g show ?thesis
-    by (auto simp add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
+    by (auto simp: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
 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 add: homotopic_loops_def homotopic_with_def path_defs)
+   "\<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"
-by (auto simp: path_component_imp_homotopic_points
-         dest: homotopic_loops_imp_path_component_value [where t=1])
+  using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce
 
 lemma path_connected_eq_homotopic_points:
-    "path_connected S \<longleftrightarrow>
+  "path_connected S \<longleftrightarrow>
       (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
-by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
+  by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
 
 
 subsection\<open>Simply connected sets\<close>
@@ -1134,16 +1132,9 @@
   then show ?rhs
   using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
 next
-  assume r: ?rhs
-  note pa = r [THEN conjunct2, rule_format]
-  show ?lhs
-  proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
-    fix p a
-    assume "path p" and "path_image p \<subseteq> S" "pathfinish p = pathstart p"
-      and "a \<in> S"
-    with pa [of p] show "homotopic_loops S p (linepath a a)"
-      using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
-  qed
+  assume ?rhs
+  then show ?lhs
+    by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any)
 qed
 
 lemma simply_connected_eq_contractible_loop_all:
@@ -1158,19 +1149,8 @@
 next
   case False
   then obtain a where "a \<in> S" by blast
-  show ?thesis
-  proof
-    assume "simply_connected S"
-    then show ?rhs
-      using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any
-      by blast
-  next
-    assume ?rhs
-    then show "simply_connected S"
-      unfolding simply_connected_eq_contractible_loop_any 
-      by (meson False homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans 
-          path_component_imp_homotopic_points path_component_refl)
-  qed
+  then show ?thesis
+    by (meson False homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
 qed
 
 lemma simply_connected_eq_contractible_path:
@@ -1212,19 +1192,17 @@
            "path_image q \<subseteq> S" "pathstart q = pathstart p"
            "pathfinish q = pathfinish p" for p q
   proof -
-    have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
-      by (simp add: homotopic_paths_rid homotopic_paths_sym that)
-    also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
-                                 (p +++ reversepath q +++ q)"
+    have "homotopic_paths S p (p +++ reversepath q +++ q)"
       using that
-      by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
+      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)"
       by (simp add: that homotopic_paths_assoc)
     also have "homotopic_paths S ((p +++ reversepath q) +++ q)
                                  (linepath (pathstart q) (pathstart q) +++ q)"
       using * [of "p +++ reversepath q"] that
-      by (simp add: homotopic_paths_join path_image_join)
+      by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
     also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
       using that homotopic_paths_lid by blast
     finally show ?thesis .
@@ -1291,12 +1269,12 @@
   have "\<forall>p. path p \<and>
             path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<longrightarrow>
             homotopic_loops S p (linepath a a)"
-    using a apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
+    using a apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
     apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
     apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset)
     done
   with \<open>a \<in> S\<close> show ?thesis
-    by (auto simp add: simply_connected_eq_contractible_loop_all False)
+    by (auto simp: simply_connected_eq_contractible_loop_all False)
 qed
 
 corollary contractible_imp_connected:
@@ -1369,20 +1347,20 @@
 lemma homotopic_into_contractible:
   fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
-      and g: "continuous_on S g" "g ` S \<subseteq> T"
-      and T: "contractible T"
-    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S f T id T g id]
-by (simp add: assms contractible_imp_path_connected)
+    and g: "continuous_on S g" "g ` S \<subseteq> T"
+    and T: "contractible T"
+  shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+  using homotopic_through_contractible [of S f T id T g id]
+  by (simp add: assms contractible_imp_path_connected)
 
 lemma homotopic_from_contractible:
   fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
-      and g: "continuous_on S g" "g ` S \<subseteq> T"
-      and "contractible S" "path_connected T"
-    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S id S f T id g]
-by (simp add: assms contractible_imp_path_connected)
+    and g: "continuous_on S g" "g ` S \<subseteq> T"
+    and "contractible S" "path_connected T"
+  shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+  using homotopic_through_contractible [of S id S f T id g]
+  by (simp add: assms contractible_imp_path_connected)
 
 subsection\<open>Starlike sets\<close>
 
@@ -1402,8 +1380,7 @@
 proof -
   have "rel_interior S \<noteq> {}"
     by (simp add: assms rel_interior_eq_empty)
-  then obtain a where a: "a \<in> rel_interior S"  by blast
-  with ST have "a \<in> T"  by blast
+  with ST obtain a where a: "a \<in> rel_interior S" and "a \<in> T" by blast
   have "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
     by (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a]) (use assms in auto)
   then have "\<forall>x\<in>T. a \<in> T \<and> open_segment a x \<subseteq> T"
@@ -1439,7 +1416,7 @@
 lemma starlike_imp_contractible:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> contractible S"
-using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
+  using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
 
 lemma contractible_UNIV [simp]: "contractible (UNIV :: 'a::real_normed_vector set)"
   by (simp add: starlike_imp_contractible)
@@ -1447,27 +1424,27 @@
 lemma starlike_imp_simply_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> simply_connected S"
-by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
+  by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
 
 lemma convex_imp_simply_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "convex S \<Longrightarrow> simply_connected S"
-using convex_imp_starlike starlike_imp_simply_connected by blast
+  using convex_imp_starlike starlike_imp_simply_connected by blast
 
 lemma starlike_imp_path_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> path_connected S"
-by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
+  by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
 
 lemma starlike_imp_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> connected S"
-by (simp add: path_connected_imp_connected starlike_imp_path_connected)
+  by (simp add: path_connected_imp_connected starlike_imp_path_connected)
 
 lemma is_interval_simply_connected_1:
   fixes S :: "real set"
   shows "is_interval S \<longleftrightarrow> simply_connected S"
-using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
+  by (meson convex_imp_simply_connected is_interval_connected_1 is_interval_convex_1 simply_connected_imp_connected)
 
 lemma contractible_empty [simp]: "contractible {}"
   by (simp add: contractible_def homotopic_on_emptyI)
@@ -1476,15 +1453,8 @@
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" and TS: "rel_interior S \<subseteq> T" "T \<subseteq> closure S"
   shows "contractible T"
-proof (cases "S = {}")
-  case True
-  with assms show ?thesis
-    by (simp add: subsetCE)
-next
-  case False
-  show ?thesis
-    by (meson False assms starlike_convex_tweak_boundary_points starlike_imp_contractible)
-qed
+  by (metis assms closure_eq_empty contractible_empty empty_subsetI 
+      starlike_convex_tweak_boundary_points starlike_imp_contractible subset_antisym)
 
 lemma convex_imp_contractible:
   fixes S :: "'a::real_normed_vector set"
@@ -1494,13 +1464,13 @@
 lemma contractible_sing [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "contractible {a}"
-by (rule convex_imp_contractible [OF convex_singleton])
+  by (rule convex_imp_contractible [OF convex_singleton])
 
 lemma is_interval_contractible_1:
   fixes S :: "real set"
   shows  "is_interval S \<longleftrightarrow> contractible S"
-using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
-      is_interval_simply_connected_1 by auto
+  using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
+    is_interval_simply_connected_1 by auto
 
 lemma contractible_Times:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -1556,9 +1526,7 @@
 lemma locally_open_subset:
   assumes "locally P S" "openin (top_of_set S) t"
     shows "locally P t"
-  using assms
-  unfolding locally_def
-  by (elim all_forward) (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans)
+  by (smt (verit, ccfv_SIG) assms order.trans locally_def openin_imp_subset openin_subset_trans openin_trans)
 
 lemma locally_diff_closed:
     "\<lbrakk>locally P S; closedin (top_of_set S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
@@ -1575,16 +1543,13 @@
     using zero_less_one by blast
   then show ?thesis
     unfolding locally_def
-    by (auto simp add: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
+    by (auto simp: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
 qed
 
 lemma locally_iff:
     "locally P S \<longleftrightarrow>
      (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>V. P V \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> V \<and> V \<subseteq> S \<inter> T)))"
-  apply (simp add: le_inf_iff locally_def openin_open, safe)
-   apply (metis IntE IntI le_inf_iff)
-  apply (metis IntI Int_subset_iff)
-  done
+  by (smt (verit) locally_def openin_open)
 
 lemma locally_Int:
   assumes S: "locally P S" and T: "locally P T"
@@ -1649,34 +1614,29 @@
     using hom by (auto simp: homeomorphism_def)
   have gw: "g ` W = S \<inter> f -` W"
     using \<open>W \<subseteq> T\<close> g by force
-  have \<circ>: "openin (top_of_set S) (g ` W)"
-  proof -
-    have "continuous_on S f"
-      using f(3) by blast
-    then show "openin (top_of_set S) (g ` W)"
-      by (simp add: gw Collect_conj_eq \<open>openin (top_of_set T) W\<close> continuous_on_open f(2))
-  qed
+  have "openin (top_of_set S) (g ` W)"
+    using \<open>openin (top_of_set T) W\<close> continuous_on_open f gw by auto
   then obtain U V
     where osu: "openin (top_of_set S) U" and uv: "P V" "g y \<in> U" "U \<subseteq> V" "V \<subseteq> g ` W"
-    using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
+    by (metis S \<open>y \<in> W\<close> image_eqI locallyE)
   have "V \<subseteq> S" using uv by (simp add: gw)
   have fv: "f ` V = T \<inter> {x. g x \<in> V}"
     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
-  have contvf: "continuous_on V f"
-    using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
-  have contvg: "continuous_on (f ` V) g"
-    using \<open>f ` V \<subseteq> W\<close> \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
+  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 add: homeomorphism_def contvf contvg)
+    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 1: "openin (top_of_set T) (T \<inter> g -` U)"
+  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
-  have 2: "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
+  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 "Q (f ` V)"
       using Q homv \<open>P V\<close> by blast
@@ -1687,44 +1647,28 @@
     show "f ` V \<subseteq> W"
       using \<open>f ` V \<subseteq> W\<close> by blast
   qed
-  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 1 2)
+  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
 qed
 
 lemma homeomorphism_locally:
   fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes hom: "homeomorphism S T f g"
-      and eq: "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
+  assumes "homeomorphism S T f g"
+      and "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
     shows "locally P S \<longleftrightarrow> locally Q T"
-     (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    using eq hom homeomorphism_locally_imp by blast
-next
-  assume ?rhs
-  then show ?lhs
-    using eq homeomorphism_sym homeomorphism_symD [OF hom] 
-    by (blast intro: homeomorphism_locally_imp) 
-qed
+  by (smt (verit) assms homeomorphism_locally_imp homeomorphism_symD)
 
 lemma homeomorphic_locally:
   fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
   assumes hom: "S homeomorphic T"
           and iff: "\<And>X Y. X homeomorphic Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
     shows "locally P S \<longleftrightarrow> locally Q T"
-proof -
-  obtain f g where hom: "homeomorphism S T f g"
-    using assms by (force simp: homeomorphic_def)
-  then show ?thesis
-    using homeomorphic_def local.iff
-    by (blast intro!: homeomorphism_locally)
-qed
+  by (smt (verit, ccfv_SIG) hom homeomorphic_def homeomorphism_locally homeomorphism_locally_imp iff)
 
 lemma homeomorphic_local_compactness:
   fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
   shows "S homeomorphic T \<Longrightarrow> locally compact S \<longleftrightarrow> locally compact T"
-by (simp add: homeomorphic_compactness homeomorphic_locally)
+  by (simp add: homeomorphic_compactness homeomorphic_locally)
 
 lemma locally_translation:
   fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
@@ -1746,7 +1690,7 @@
       and oo: "\<And>T. openin (top_of_set S) T \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
       and Q: "\<And>T. \<lbrakk>T \<subseteq> S; P T\<rbrakk> \<Longrightarrow> Q(f ` T)"
     shows "locally Q (f ` S)"
-proof (clarsimp simp add: locally_def)
+proof (clarsimp simp: locally_def)
   fix W y
   assume oiw: "openin (top_of_set (f ` S)) W" and "y \<in> W"
   then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
@@ -1756,8 +1700,7 @@
     using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
   then obtain U V
     where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
-    using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
-    by auto
+    by (metis IntI P \<open>y \<in> W\<close> locallyE oivf vimageI)
   then have "openin (top_of_set (f ` S)) (f ` U)"
     by (simp add: oo)
   then show "\<exists>X. openin (top_of_set (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
@@ -1778,17 +1721,16 @@
 proof -
   let ?A = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
   let ?B = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
-  have 1: "openin (top_of_set S) ?A"
-    by (subst openin_subopen, blast)
-  have 2: "openin (top_of_set S) ?B"
-    by (subst openin_subopen, blast)
-  have \<section>: "?A \<inter> ?B = {}"
+  have "?A \<inter> ?B = {}"
     by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int)
-  have *: "S \<subseteq> ?A \<union> ?B"
+  moreover have "S \<subseteq> ?A \<union> ?B"
     by clarsimp (meson opI)
-  have "?A = {} \<or> ?B = {}"
-    using \<open>connected S\<close> [unfolded connected_openin, simplified, rule_format, OF 1 \<section> * 2] 
-    by blast
+  moreover have "openin (top_of_set S) ?A"
+    by (subst openin_subopen, blast)
+  moreover have "openin (top_of_set S) ?B"
+    by (subst openin_subopen, blast)
+  ultimately have "?A = {} \<or> ?B = {}"
+    by (metis (no_types, lifting) \<open>connected S\<close> connected_openin)
   then show ?thesis
     by clarsimp (meson opI etc)
 qed
@@ -1851,15 +1793,11 @@
   shows "locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then have "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x\<in>T. f x = f a)"
-    unfolding locally_def
-    by (metis (mono_tags, opaque_lifting) constant_on_def constant_on_subset openin_subtopology_self)
   then show ?rhs
-    using assms
-    by (simp add: locally_constant_imp_constant)
+    by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff)
 next
   assume ?rhs then show ?lhs
-    using assms by (metis constant_on_subset locallyI openin_imp_subset order_refl)
+    by (metis constant_on_subset locallyI openin_imp_subset order_refl)
 qed
 
 
@@ -1938,10 +1876,8 @@
   proof
     fix x
     assume "x \<in> S"
-    then obtain e where "e>0" and e: "closed (cball x e \<inter> S)"
-      using R by blast
-    then have "compact (cball x e \<inter> S)"
-      by (simp add: bounded_Int compact_eq_bounded_closed)
+    then obtain e where "e>0" and "compact (cball x e \<inter> S)"
+      by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R)
     moreover have "\<forall>y\<in>ball x e \<inter> S. \<exists>\<epsilon>>0. cball y \<epsilon> \<inter> S \<subseteq> ball x e"
       by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq)
     moreover have "openin (top_of_set S) (ball x e \<inter> S)"
@@ -1984,10 +1920,8 @@
     have "openin (top_of_set S) (\<Union> (u ` T))"
       using T that uv by fastforce
     moreover
-    have "compact (\<Union> (v ` T))"
-      by (meson T compact_UN subset_eq that(1) uv)
-    moreover have "\<Union> (v ` T) \<subseteq> S"
-      by (metis SUP_least T(1) subset_eq that(1) uv)
+    obtain "compact (\<Union> (v ` T))" "\<Union> (v ` T) \<subseteq> S"
+      by (metis T UN_subset_iff \<open>K \<subseteq> S\<close> compact_UN subset_iff uv)
     ultimately show ?thesis
       using T by auto 
   qed
@@ -1996,7 +1930,7 @@
 next
   assume ?rhs
   then show ?lhs
-    apply (clarsimp simp add: locally_compact)
+    apply (clarsimp simp: locally_compact)
     apply (drule_tac x="{x}" in spec, simp)
     done
 qed
@@ -2014,14 +1948,7 @@
     have ope: "openin (top_of_set S) (ball x e)"
       by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
     show ?thesis
-    proof (intro exI conjI)
-      let ?U = "ball x e"
-      let ?V = "cball x e"
-      show "x \<in> ?U" "?U \<subseteq> ?V" "?V \<subseteq> S" "compact ?V"
-        using \<open>e > 0\<close> e by auto
-      show "openin (top_of_set S) ?U"
-        using ope by blast
-    qed
+      by (meson \<open>0 < e\<close> ball_subset_cball centre_in_ball compact_cball e ope)
   qed
   show ?thesis
     unfolding locally_compact by (blast intro: *)
@@ -2045,13 +1972,13 @@
 
 lemma locally_compact_Int:
   fixes S :: "'a :: t2_space set"
-  shows "\<lbrakk>locally compact S; locally compact t\<rbrakk> \<Longrightarrow> locally compact (S \<inter> t)"
-by (simp add: compact_Int locally_Int)
+  shows "\<lbrakk>locally compact S; locally compact T\<rbrakk> \<Longrightarrow> locally compact (S \<inter> T)"
+  by (simp add: compact_Int locally_Int)
 
 lemma locally_compact_closedin:
   fixes S :: "'a :: heine_borel set"
-  shows "\<lbrakk>closedin (top_of_set S) t; locally compact S\<rbrakk>
-        \<Longrightarrow> locally compact t"
+  shows "\<lbrakk>closedin (top_of_set S) T; locally compact S\<rbrakk>
+        \<Longrightarrow> locally compact T"
   unfolding closedin_closed
   using closed_imp_locally_compact locally_compact_Int by blast
 
@@ -2130,12 +2057,7 @@
     obtain e2 where "e2 > 0" and e2: "closed (cball x e2 \<inter> T)"
       using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
     moreover have "closed (cball x (min e1 e2) \<inter> (S \<union> T))"
-    proof -
-      have "closed (cball x e1 \<inter> (cball x e2 \<inter> S))"
-        by (metis closed_Int closed_cball e1 inf_left_commute)
-      then show ?thesis
-        by (simp add: Int_Un_distrib cball_min_Int closed_Int closed_Un e2 inf_assoc)
-    qed
+      by (smt (verit) Int_Un_distrib2 Int_commute cball_min_Int closed_Int closed_Un closed_cball e1 e2 inf_left_commute)
     ultimately show ?thesis
       by (rule_tac x="min e1 e2" in exI) linarith
   qed
@@ -2298,7 +2220,7 @@
             by (simp_all add: closedin_closed_Int)
           moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
             using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
-            by (auto simp add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
+            by (auto simp: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
           ultimately have cloDV1: "closedin (top_of_set D) (D \<inter> V1)"
                       and cloDV2:  "closedin (top_of_set D) (D \<inter> V2)"
             by metis+
@@ -2721,7 +2643,7 @@
   fixes S :: "'a:: real_normed_vector set"
   assumes "convex S"
   shows "locally path_connected S"
-proof (clarsimp simp add: locally_path_connected)
+proof (clarsimp simp: locally_path_connected)
   fix V x
   assume "openin (top_of_set S) V" and "x \<in> V"
   then obtain T e where  "V = S \<inter> T" "x \<in> S" "0 < e" "ball x e \<subseteq> T"
@@ -3824,7 +3746,7 @@
       show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
                            (\<lambda>(t,x). (1 - t) * x + t * z)"
         using  \<open>z \<in> S\<close> 
-        by (auto simp add: case_prod_unfold intro!: continuous_intros \<section>)
+        by (auto simp: case_prod_unfold intro!: continuous_intros \<section>)
     qed auto
   qed (simp add: contractible_space_empty)
 qed
@@ -3946,7 +3868,7 @@
     by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto)
   moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
     by (rule homotopic_with_compose_continuous_left [where Y=T])
-       (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+       (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)
 qed
@@ -3987,7 +3909,7 @@
     by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto)
   moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
     by (rule homotopic_with_compose_continuous_right [where X=T])
-       (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+       (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
   ultimately show ?thesis
     using homotopic_with_trans by (fastforce simp add: o_def)
 qed
@@ -4123,7 +4045,7 @@
   fixes U :: "'a::euclidean_space set"
   assumes "convex U" "\<not> collinear U" "countable S"
     shows "path_connected(U - S)"
-proof (clarsimp simp add: path_connected_def)
+proof (clarsimp simp: path_connected_def)
   fix a b
   assume "a \<in> U" "a \<notin> S" "b \<in> U" "b \<notin> S"
   let ?m = "midpoint a b"
@@ -4245,7 +4167,7 @@
   next
     assume ge2: "aff_dim S \<ge> 2"
     then have "\<not> collinear S"
-    proof (clarsimp simp add: collinear_affine_hull)
+    proof (clarsimp simp: collinear_affine_hull)
       fix u v
       assume "S \<subseteq> affine hull {u, v}"
       then have "aff_dim S \<le> aff_dim {u, v}"
@@ -4282,7 +4204,7 @@
   assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
       and "\<not> collinear S" "countable T"
     shows "path_connected(S - T)"
-proof (clarsimp simp add: path_connected_component)
+proof (clarsimp simp: path_connected_component)
   fix x y
   assume xy: "x \<in> S" "x \<notin> T" "y \<in> S" "y \<notin> T"
   show "path_component (S - T) x y"
@@ -4483,7 +4405,7 @@
       by blast
   next
     show "cball a r \<inter> T \<subseteq> f ` (cball a r \<inter> T)"
-    proof (clarsimp simp add: dist_norm norm_minus_commute)
+    proof (clarsimp simp: dist_norm norm_minus_commute)
       fix x
       assume x: "norm (x - a) \<le> r" and "x \<in> T"
       have "\<exists>v \<in> {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \<bullet> 1 = 0"
@@ -4575,7 +4497,7 @@
       then show "continuous_on S gg"
         by (rule continuous_on_subset) (use ST in auto)
       show "ff ` S \<subseteq> S"
-      proof (clarsimp simp add: ff_def)
+      proof (clarsimp simp: ff_def)
         fix x
         assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
         then have "f x \<in> cball a r \<inter> T"
@@ -4584,7 +4506,7 @@
           using ST(1) \<open>x \<in> T\<close> gid hom homeomorphism_def x by fastforce
       qed
       show "gg ` S \<subseteq> S"
-      proof (clarsimp simp add: gg_def)
+      proof (clarsimp simp: gg_def)
         fix x
         assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
         then have "g x \<in> cball a r \<inter> T"