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