# HG changeset patch
# User paulson
# Date 1679049770 0
# Node ID 05329cd9db4bc852bc3b5cf20e77e1221c1463d4
# Parent  a76f49a034488bb12cfadcfc0da4551ad10481ba# Parent  71f001027a13516216178c73388147647d3e27f3
merged

diff -r a76f49a03448 -r 05329cd9db4b src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Thu Mar 16 17:12:06 2023 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Fri Mar 17 10:42:50 2023 +0000
@@ -62,11 +62,8 @@
   unfolding homotopic_with_def
   apply (rule iffI, blast, clarify)
   apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then p v else q v" in exI)
-  apply auto
-  using continuous_map_eq apply fastforce
-  apply (drule_tac x=t in bspec, force)
-  apply (subst assms; simp)
-  done
+  apply simp
+  by (smt (verit, best) SigmaE assms case_prod_conv continuous_map_eq topspace_prod_topology)
 
 lemma homotopic_with_mono:
   assumes hom: "homotopic_with P X Y f g"
@@ -121,11 +118,11 @@
 
 lemma homotopic_with_imp_subset1:
      "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
-  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
 
 lemma homotopic_with_imp_subset2:
      "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
-  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
 
 lemma homotopic_with_subset_left:
      "\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
@@ -140,7 +137,7 @@
 text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
 
 lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \<longleftrightarrow> continuous_map X Y f \<and> P f"
-  by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)
+  by (metis homotopic_with_equal homotopic_with_imp_continuous_maps homotopic_with_imp_property)
 
 lemma homotopic_with_symD:
     assumes "homotopic_with P X Y f g"
@@ -262,44 +259,26 @@
 corollary homotopic_compose:
   assumes "homotopic_with (\<lambda>x. True) X Y f f'" "homotopic_with (\<lambda>x. True) Y Z g g'"
   shows "homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g' \<circ> f')"
-proof (rule homotopic_with_trans [where g = "g \<circ> f'"])
-  show "homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g \<circ> f')"
-    using assms by (simp add: homotopic_with_compose_continuous_map_left homotopic_with_imp_continuous_maps)
-  show "homotopic_with (\<lambda>x. True) X Z (g \<circ> f') (g' \<circ> f')"
-    using assms by (simp add: homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps)
-qed
+  by (metis assms homotopic_with_compose_continuous_map_left homotopic_with_compose_continuous_map_right homotopic_with_imp_continuous_maps homotopic_with_trans)
 
 proposition homotopic_with_compose_continuous_right:
     "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
      \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
-  apply (clarsimp simp add: homotopic_with_def)
-  subgoal for k
-    apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
-    by (intro conjI continuous_intros continuous_on_compose2 [where f=snd and g=h]; fastforce simp: o_def elim: continuous_on_subset)
-  done
+  by (simp add: homotopic_with_compose_continuous_map_right)
 
 proposition homotopic_with_compose_continuous_left:
      "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
       \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
-  apply (clarsimp simp add: homotopic_with_def)
-  subgoal for k
-  apply (rule_tac x="h \<circ> k" in exI)
-    by (intro conjI continuous_intros continuous_on_compose [where f=snd and g=h, unfolded o_def]; fastforce simp: o_def elim: continuous_on_subset)
-  done
+  by (simp add: homotopic_with_compose_continuous_map_left)
 
 lemma homotopic_from_subtopology:
-   "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X s) X' f g"
-  unfolding homotopic_with_def
-  by (force simp add: continuous_map_from_subtopology prod_topology_subtopology(2) elim!: ex_forward)
+   "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X S) X' f g"
+  by (metis continuous_map_id_subt homotopic_with_compose_continuous_map_right o_id)
 
 lemma homotopic_on_emptyI:
     assumes "topspace X = {}" "P f" "P g"
     shows "homotopic_with P X X' f g"
-  unfolding homotopic_with_def
-proof (intro exI conjI ballI)
-  show "P (\<lambda>x. (\<lambda>(t,x). if t = 0 then f x else g x) (t, x))" if "t \<in> {0..1}" for t::real
-    by (cases "t = 0", auto simp: assms)
-qed (auto simp: continuous_map_atin assms)
+  by (metis assms continuous_map_on_empty empty_iff homotopic_with_equal)
 
 lemma homotopic_on_empty:
    "topspace X = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
@@ -342,15 +321,7 @@
        and g': "\<And>x. x \<in> topspace X \<Longrightarrow> g' x = g x"
        and P:  "(\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> P h \<longleftrightarrow> P k)"
    shows "homotopic_with P X Y f' g'"
-  using h unfolding homotopic_with_def
-  apply clarify
-  subgoal for h
-    apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI)
-    apply (simp add: f' g', safe)
-     apply (fastforce intro: continuous_map_eq)
-    apply (subst P; fastforce)
-    done
-  done
+  by (smt (verit, ccfv_SIG) assms homotopic_with)
 
 lemma homotopic_with_prod_topology:
   assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
@@ -461,10 +432,8 @@
       assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
       obtain c d where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. d)"
         using False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close>  RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
-      then have "c \<in> T" "d \<in> T"
-        using False homotopic_with_imp_continuous_maps by fastforce+
       with T have "path_component T c d"
-        using path_connected_component by blast
+        by (metis False ex_in_conv homotopic_with_imp_subset2 image_subset_iff path_connected_component)
       then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
         by (simp add: homotopic_constant_maps)
       with c d show "homotopic_with_canon (\<lambda>x. True) S T f g"
@@ -479,13 +448,13 @@
 
 definition\<^marker>\<open>tag important\<close> homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   where
-     "homotopic_paths s p q \<equiv>
-       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
+     "homotopic_paths S p q \<equiv>
+       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} S p q"
 
 lemma homotopic_paths:
-   "homotopic_paths s p q \<longleftrightarrow>
+   "homotopic_paths S p q \<longleftrightarrow>
       (\<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and>
-          h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and>
+          h ` ({0..1} \<times> {0..1}) \<subseteq> S \<and>
           (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
           (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
           (\<forall>t \<in> {0..1::real}. pathstart(h \<circ> Pair t) = pathstart p \<and>
@@ -493,56 +462,48 @@
   by (auto simp: homotopic_paths_def homotopic_with pathstart_def pathfinish_def)
 
 proposition homotopic_paths_imp_pathstart:
-     "homotopic_paths s p q \<Longrightarrow> pathstart p = pathstart q"
+     "homotopic_paths S p q \<Longrightarrow> pathstart p = pathstart q"
   by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)
 
 proposition homotopic_paths_imp_pathfinish:
-     "homotopic_paths s p q \<Longrightarrow> pathfinish p = pathfinish q"
+     "homotopic_paths S p q \<Longrightarrow> pathfinish p = pathfinish q"
   by (metis (mono_tags, lifting) homotopic_paths_def homotopic_with_imp_property)
 
 lemma homotopic_paths_imp_path:
-     "homotopic_paths s p q \<Longrightarrow> path p \<and> path q"
+     "homotopic_paths S p q \<Longrightarrow> path p \<and> path q"
   using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
 
 lemma homotopic_paths_imp_subset:
-     "homotopic_paths s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
+     "homotopic_paths S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
   by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
 
-proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> s"
+proposition homotopic_paths_refl [simp]: "homotopic_paths S p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> S"
   by (simp add: homotopic_paths_def path_def path_image_def)
 
-proposition homotopic_paths_sym: "homotopic_paths s p q \<Longrightarrow> homotopic_paths s q p"
+proposition homotopic_paths_sym: "homotopic_paths S p q \<Longrightarrow> homotopic_paths S q p"
   by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
 
-proposition homotopic_paths_sym_eq: "homotopic_paths s p q \<longleftrightarrow> homotopic_paths s q p"
+proposition homotopic_paths_sym_eq: "homotopic_paths S p q \<longleftrightarrow> homotopic_paths S q p"
   by (metis homotopic_paths_sym)
 
 proposition homotopic_paths_trans [trans]:
-  assumes "homotopic_paths s p q" "homotopic_paths s q r"
-  shows "homotopic_paths s p r"
-proof -
-  have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
-    using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
-  then have "homotopic_with_canon (\<lambda>f. pathstart f = pathstart p \<and> pathfinish f = pathfinish p) {0..1} s q r"
-    using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
-  then show ?thesis
-    using assms homotopic_paths_def homotopic_with_trans by blast
-qed
+  assumes "homotopic_paths S p q" "homotopic_paths S q r"
+  shows "homotopic_paths S p r"
+  using assms homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart unfolding homotopic_paths_def
+  by (smt (verit, ccfv_SIG) homotopic_with_mono homotopic_with_trans)
 
 proposition homotopic_paths_eq:
-     "\<lbrakk>path p; path_image p \<subseteq> s; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> homotopic_paths s p q"
-  unfolding homotopic_paths_def
-  by (rule homotopic_with_eq)
-     (auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq)
+     "\<lbrakk>path p; path_image p \<subseteq> S; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> homotopic_paths S p q"
+  by (smt (verit, best) homotopic_paths homotopic_paths_refl)
 
 proposition homotopic_paths_reparametrize:
   assumes "path p"
-      and pips: "path_image p \<subseteq> s"
+      and pips: "path_image p \<subseteq> S"
       and contf: "continuous_on {0..1} f"
       and f01:"f ` {0..1} \<subseteq> {0..1}"
       and [simp]: "f(0) = 0" "f(1) = 1"
       and q: "\<And>t. t \<in> {0..1} \<Longrightarrow> q(t) = p(f t)"
-    shows "homotopic_paths s p q"
+    shows "homotopic_paths S p q"
 proof -
   have contp: "continuous_on {0..1} p"
     by (metis \<open>path p\<close> path_def)
@@ -550,18 +511,18 @@
     using contf continuous_on_compose continuous_on_subset f01 by blast
   then have "path q"
     by (simp add: path_def) (metis q continuous_on_cong)
-  have piqs: "path_image q \<subseteq> s"
+  have piqs: "path_image q \<subseteq> S"
     by (metis (no_types, opaque_lifting) pips f01 image_subset_iff path_image_def q)
   have fb0: "\<And>a b. \<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> (1 - a) * f b + a * b"
     using f01 by force
   have fb1: "\<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1\<rbrakk> \<Longrightarrow> (1 - a) * f b + a * b \<le> 1" for a b
     using f01 [THEN subsetD, of "f b"] by (simp add: convex_bound_le)
-  have "homotopic_paths s q p"
+  have "homotopic_paths S q p"
   proof (rule homotopic_paths_trans)
-    show "homotopic_paths s q (p \<circ> f)"
+    show "homotopic_paths S q (p \<circ> f)"
       using q by (force intro: homotopic_paths_eq [OF  \<open>path q\<close> piqs])
   next
-    show "homotopic_paths s (p \<circ> f) p"
+    show "homotopic_paths S (p \<circ> f) p"
       using pips [unfolded path_image_def]
       apply (simp add: homotopic_paths_def homotopic_with_def)
       apply (rule_tac x="p \<circ> (\<lambda>y. (1 - (fst y)) *\<^sub>R ((f \<circ> snd) y) + (fst y) *\<^sub>R snd y)"  in exI)
@@ -572,7 +533,7 @@
     by (simp add: homotopic_paths_sym)
 qed
 
-lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
+lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths S p q; S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
   unfolding homotopic_paths by fast
 
 
@@ -601,8 +562,8 @@
 text\<open> Congruence properties of homotopy w.r.t. path-combining operations.\<close>
 
 lemma homotopic_paths_reversepath_D:
-      assumes "homotopic_paths s p q"
-      shows   "homotopic_paths s (reversepath p) (reversepath q)"
+      assumes "homotopic_paths S p q"
+      shows   "homotopic_paths S (reversepath p) (reversepath q)"
   using assms
   apply (simp add: homotopic_paths_def homotopic_with_def, clarify)
   apply (rule_tac x="h \<circ> (\<lambda>x. (fst x, 1 - snd x))" in exI)
@@ -611,12 +572,12 @@
   done
 
 proposition homotopic_paths_reversepath:
-     "homotopic_paths s (reversepath p) (reversepath q) \<longleftrightarrow> homotopic_paths s p q"
+     "homotopic_paths S (reversepath p) (reversepath q) \<longleftrightarrow> homotopic_paths S p q"
   using homotopic_paths_reversepath_D by force
 
 
 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')"
+    "\<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 (rename_tac k1 k2)
   apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
@@ -624,7 +585,7 @@
   done
 
 proposition homotopic_paths_continuous_image:
-    "\<lbrakk>homotopic_paths s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
+    "\<lbrakk>homotopic_paths S f g; continuous_on S h; h ` S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
   unfolding homotopic_paths_def
   by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
 
@@ -634,8 +595,8 @@
 text\<^marker>\<open>tag important\<close>\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
 
 proposition homotopic_paths_rid:
-  assumes "path p" "path_image p \<subseteq> s"
-  shows "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
+  assumes "path p" "path_image p \<subseteq> S"
+  shows "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p)) p"
 proof -
   have \<section>: "continuous_on {0..1} (\<lambda>t::real. if t \<le> 1/2 then 2 *\<^sub>R t else 1)"
     unfolding split_01
@@ -647,15 +608,15 @@
 qed
 
 proposition homotopic_paths_lid:
-   "\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
-  using homotopic_paths_rid [of "reversepath p" s]
+   "\<lbrakk>path p; path_image p \<subseteq> S\<rbrakk> \<Longrightarrow> homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p) p"
+  using homotopic_paths_rid [of "reversepath p" S]
   by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
         pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
 
 proposition homotopic_paths_assoc:
-   "\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
+   "\<lbrakk>path p; path_image p \<subseteq> S; path q; path_image q \<subseteq> S; path r; path_image r \<subseteq> S; pathfinish p = pathstart q;
      pathfinish q = pathstart r\<rbrakk>
-    \<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
+    \<Longrightarrow> homotopic_paths S (p +++ (q +++ r)) ((p +++ q) +++ r)"
   apply (subst homotopic_paths_sym)
   apply (rule homotopic_paths_reparametrize
            [where f = "\<lambda>t. if  t \<le> 1/2 then inverse 2 *\<^sub>R t
@@ -666,8 +627,8 @@
   done
 
 proposition homotopic_paths_rinv:
-  assumes "path p" "path_image p \<subseteq> s"
-    shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
+  assumes "path p" "path_image p \<subseteq> S"
+    shows "homotopic_paths S (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
 proof -
   have p: "continuous_on {0..1} p" 
     using assms by (auto simp: path_def)
@@ -690,67 +651,67 @@
 qed
 
 proposition homotopic_paths_linv:
-  assumes "path p" "path_image p \<subseteq> s"
-    shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
-  using homotopic_paths_rinv [of "reversepath p" s] assms by simp
+  assumes "path p" "path_image p \<subseteq> S"
+    shows "homotopic_paths S (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
+  using homotopic_paths_rinv [of "reversepath p" S] assms by simp
 
 
 subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
 
 definition\<^marker>\<open>tag important\<close> homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
- "homotopic_loops s p q \<equiv>
-     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
+ "homotopic_loops S p q \<equiv>
+     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} S p q"
 
 lemma homotopic_loops:
-   "homotopic_loops s p q \<longleftrightarrow>
+   "homotopic_loops S p q \<longleftrightarrow>
       (\<exists>h. continuous_on ({0..1::real} \<times> {0..1}) h \<and>
-          image h ({0..1} \<times> {0..1}) \<subseteq> s \<and>
+          image h ({0..1} \<times> {0..1}) \<subseteq> S \<and>
           (\<forall>x \<in> {0..1}. h(0,x) = p x) \<and>
           (\<forall>x \<in> {0..1}. h(1,x) = q x) \<and>
           (\<forall>t \<in> {0..1}. pathfinish(h \<circ> Pair t) = pathstart(h \<circ> Pair t)))"
   by (simp add: homotopic_loops_def pathstart_def pathfinish_def homotopic_with)
 
 proposition homotopic_loops_imp_loop:
-     "homotopic_loops s p q \<Longrightarrow> pathfinish p = pathstart p \<and> pathfinish q = pathstart q"
+     "homotopic_loops S p q \<Longrightarrow> pathfinish p = pathstart p \<and> pathfinish q = pathstart q"
 using homotopic_with_imp_property homotopic_loops_def by blast
 
 proposition homotopic_loops_imp_path:
-     "homotopic_loops s p q \<Longrightarrow> path p \<and> path q"
+     "homotopic_loops S p q \<Longrightarrow> path p \<and> path q"
   unfolding homotopic_loops_def path_def
   using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
 
 proposition homotopic_loops_imp_subset:
-     "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
+     "homotopic_loops S p q \<Longrightarrow> path_image p \<subseteq> S \<and> path_image q \<subseteq> S"
   unfolding homotopic_loops_def path_image_def
   by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
 
 proposition homotopic_loops_refl:
-     "homotopic_loops s p p \<longleftrightarrow>
-      path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
+     "homotopic_loops S p p \<longleftrightarrow>
+      path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p"
   by (simp add: homotopic_loops_def path_image_def path_def)
 
-proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
+proposition homotopic_loops_sym: "homotopic_loops S p q \<Longrightarrow> homotopic_loops S q p"
   by (simp add: homotopic_loops_def homotopic_with_sym)
 
-proposition homotopic_loops_sym_eq: "homotopic_loops s p q \<longleftrightarrow> homotopic_loops s q p"
+proposition homotopic_loops_sym_eq: "homotopic_loops S p q \<longleftrightarrow> homotopic_loops S q p"
   by (metis homotopic_loops_sym)
 
 proposition homotopic_loops_trans:
-   "\<lbrakk>homotopic_loops s p q; homotopic_loops s q r\<rbrakk> \<Longrightarrow> homotopic_loops s p r"
+   "\<lbrakk>homotopic_loops S p q; homotopic_loops S q r\<rbrakk> \<Longrightarrow> homotopic_loops S p r"
   unfolding homotopic_loops_def by (blast intro: homotopic_with_trans)
 
 proposition homotopic_loops_subset:
-   "\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
+   "\<lbrakk>homotopic_loops S p q; S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
   by (fastforce simp add: 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>
-          \<Longrightarrow> homotopic_loops s p q"
+   "\<lbrakk>path p; path_image p \<subseteq> S; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
+          \<Longrightarrow> homotopic_loops S p q"
   unfolding homotopic_loops_def path_image_def path_def pathstart_def pathfinish_def
   by (auto intro: homotopic_with_eq [OF homotopic_with_refl [where f = p, THEN iffD2]])
 
 proposition homotopic_loops_continuous_image:
-   "\<lbrakk>homotopic_loops s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
+   "\<lbrakk>homotopic_loops S f g; continuous_on S h; h ` S \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
   unfolding homotopic_loops_def
   by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
 
@@ -758,21 +719,21 @@
 subsection\<open>Relations between the two variants of homotopy\<close>
 
 proposition homotopic_paths_imp_homotopic_loops:
-    "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
+    "\<lbrakk>homotopic_paths S p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops S p q"
   by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
 
 proposition homotopic_loops_imp_homotopic_paths_null:
-  assumes "homotopic_loops s p (linepath a a)"
-    shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
+  assumes "homotopic_loops S p (linepath a a)"
+    shows "homotopic_paths S p (linepath (pathstart p) (pathstart p))"
 proof -
   have "path p" by (metis assms homotopic_loops_imp_path)
   have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
-  have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
+  have pip: "path_image p \<subseteq> S" by (metis assms homotopic_loops_imp_subset)
   let ?A = "{0..1::real} \<times> {0..1::real}"
   obtain h where conth: "continuous_on ?A h"
-             and hs: "h ` ?A \<subseteq> s"
-             and [simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(0,x) = p x"
-             and [simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(1,x) = a"
+             and hs: "h ` ?A \<subseteq> S"
+             and h0[simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(0,x) = p x"
+             and h1[simp]: "\<And>x. x \<in> {0..1} \<Longrightarrow> h(1,x) = a"
              and ends: "\<And>t. t \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair t) = pathstart (h \<circ> Pair t)"
     using assms by (auto simp: homotopic_loops homotopic_with)
   have conth0: "path (\<lambda>u. h (u, 0))"
@@ -781,7 +742,7 @@
     show "continuous_on ((\<lambda>x. (x, 0)) ` {0..1}) h"
       by (force intro: continuous_on_subset [OF conth])
   qed (force intro: continuous_intros)
-  have pih0: "path_image (\<lambda>u. h (u, 0)) \<subseteq> s"
+  have pih0: "path_image (\<lambda>u. h (u, 0)) \<subseteq> S"
     using hs by (force simp: path_image_def)
   have c1: "continuous_on ?A (\<lambda>x. h (fst x * snd x, 0))"
   proof (rule continuous_on_compose [of _ _ h, unfolded o_def])
@@ -801,21 +762,20 @@
     with \<open>c \<le> 1\<close> show ?thesis by fastforce
   qed
   have *: "\<And>p x. \<lbrakk>path p \<and> path(reversepath p);
-                  path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s;
+                  path_image p \<subseteq> S \<and> path_image(reversepath p) \<subseteq> S;
                   pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
                    pathstart(reversepath p) = a \<and> pathstart p = x\<rbrakk>
-                  \<Longrightarrow> homotopic_paths s (p +++ linepath a a +++ reversepath p) (linepath x x)"
+                  \<Longrightarrow> homotopic_paths S (p +++ linepath a a +++ reversepath p) (linepath x x)"
     by (metis homotopic_paths_lid homotopic_paths_join
               homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv)
-  have 1: "homotopic_paths s p (p +++ linepath (pathfinish p) (pathfinish p))"
+  have 1: "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
     using \<open>path p\<close> homotopic_paths_rid homotopic_paths_sym pip by blast
-  moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p))
+  moreover have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
                                    (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))"
-    apply (rule homotopic_paths_sym)
-    using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s]
-    by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset)
+    using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" S]
+    by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_sym pathstart_join)
   moreover 
-  have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))
+  have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))
                                    ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))"
     unfolding homotopic_paths_def homotopic_with_def
   proof (intro exI strip conjI)
@@ -823,28 +783,25 @@
                +++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)" 
     have "continuous_on ?A ?h"
       by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
-    moreover have "?h ` ?A \<subseteq> s"
+    moreover have "?h ` ?A \<subseteq> S"
       unfolding joinpaths_def subpath_def
       by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
   ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
-                         (top_of_set s) ?h"
+                         (top_of_set S) ?h"
     by (simp add: subpath_reversepath)
   qed (use ploop in \<open>simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\<close>)
-  moreover have "homotopic_paths s ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))
+  moreover have "homotopic_paths S ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))
                                    (linepath (pathstart p) (pathstart p))"
-  proof (rule *; simp add: pih0 pathstart_def pathfinish_def conth0)
-    show "a = (linepath a a +++ reversepath (\<lambda>u. h (u, 0))) 0 \<and> reversepath (\<lambda>u. h (u, 0)) 0 = a"
-      by (simp_all add: reversepath_def joinpaths_def)
-  qed
+    by (rule *; simp add: pih0 pathstart_def pathfinish_def conth0; simp add: reversepath_def joinpaths_def)
   ultimately show ?thesis
     by (blast intro: homotopic_paths_trans)
 qed
 
 proposition homotopic_loops_conjugate:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
+  fixes S :: "'a::real_normed_vector set"
+  assumes "path p" "path q" and pip: "path_image p \<subseteq> S" and piq: "path_image q \<subseteq> S"
       and pq: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
-    shows "homotopic_loops s (p +++ q +++ reversepath p) q"
+    shows "homotopic_loops S (p +++ q +++ reversepath p) q"
 proof -
   have contp: "continuous_on {0..1} p"  using \<open>path p\<close> [unfolded path_def] by blast
   have contq: "continuous_on {0..1} q"  using \<open>path q\<close> [unfolded path_def] by blast
@@ -860,18 +817,18 @@
       by (auto intro: continuous_on_subset [OF contp] simp: algebra_simps add_increasing2 mult_left_le_one_le)
   qed (force intro: continuous_intros)
 
-  have ps1: "\<And>a b. \<lbrakk>b * 2 \<le> 1; 0 \<le> b; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((1 - a) * (2 * b) + a) \<in> s"
+  have ps1: "\<And>a b. \<lbrakk>b * 2 \<le> 1; 0 \<le> b; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((1 - a) * (2 * b) + a) \<in> S"
     using sum_le_prod1
     by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD])
-  have ps2: "\<And>a b. \<lbrakk>\<not> 4 * b \<le> 3; b \<le> 1; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((a - 1) * (4 * b - 3) + 1) \<in> s"
+  have ps2: "\<And>a b. \<lbrakk>\<not> 4 * b \<le> 3; b \<le> 1; 0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> p ((a - 1) * (4 * b - 3) + 1) \<in> S"
     apply (rule pip [unfolded path_image_def, THEN subsetD])
     apply (rule image_eqI, blast)
     apply (simp add: algebra_simps)
-    by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono
+    by (metis add_mono affine_ineq linear mult.commute mult.left_neutral mult_right_mono
               add.commute zero_le_numeral)
-  have qs: "\<And>a b. \<lbrakk>4 * b \<le> 3; \<not> b * 2 \<le> 1\<rbrakk> \<Longrightarrow> q (4 * b - 2) \<in> s"
+  have qs: "\<And>a b. \<lbrakk>4 * b \<le> 3; \<not> b * 2 \<le> 1\<rbrakk> \<Longrightarrow> q (4 * b - 2) \<in> S"
     using path_image_def piq by fastforce
-  have "homotopic_loops s (p +++ q +++ reversepath p)
+  have "homotopic_loops S (p +++ q +++ reversepath p)
                           (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))"
     unfolding homotopic_loops_def homotopic_with_def
   proof (intro exI strip conjI)
@@ -881,25 +838,20 @@
     then have "continuous_on ?A ?h"
       using pq qloop
       by (intro continuous_on_homotopic_join_lemma) (auto simp: path_defs joinpaths_def subpath_def c1 c2)
-    then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set s) ?h"
+    then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set S) ?h"
       by (auto simp: joinpaths_def subpath_def  ps1 ps2 qs)
     show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x"  for x
       using pq by (simp add: pathfinish_def subpath_refl)
   qed (auto simp: subpath_reversepath)
-  moreover have "homotopic_loops s (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q"
+  moreover have "homotopic_loops S (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q"
   proof -
-    have "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q) q"
+    have "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q) q"
       using \<open>path q\<close> homotopic_paths_lid qloop piq by auto
-    hence 1: "\<And>f. homotopic_paths s f q \<or> \<not> homotopic_paths s f (linepath (pathfinish q) (pathfinish q) +++ q)"
+    hence 1: "\<And>f. homotopic_paths S f q \<or> \<not> homotopic_paths S f (linepath (pathfinish q) (pathfinish q) +++ q)"
       using homotopic_paths_trans by blast
-    hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q"
-    proof -
-      have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q"
-        by (simp add: \<open>path q\<close> homotopic_paths_rid piq)
-      thus ?thesis
-        by (metis (no_types) 1 \<open>path q\<close> homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym
-                  homotopic_paths_trans qloop pathfinish_linepath piq)
-    qed
+    hence "homotopic_paths S (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q"
+      by (smt (verit, best) \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_imp_subset homotopic_paths_lid 
+          homotopic_paths_rid homotopic_paths_trans pathstart_join piq qloop)
     thus ?thesis
       by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym)
   qed
@@ -918,9 +870,9 @@
   show ?thesis
   proof (cases "pathfinish p = pathfinish q")
     case True
-    have pipq: "path_image p \<subseteq> S" "path_image q \<subseteq> S"
+    obtain pipq: "path_image p \<subseteq> S" "path_image q \<subseteq> S"
       by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> homotopic_loops_imp_subset homotopic_paths_imp_path loops
-           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+
+           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)
     have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
       using \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> homotopic_paths_rid homotopic_paths_sym by blast
     moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
@@ -929,10 +881,8 @@
       by (simp add: True \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
     moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
       by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
-    moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
-      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
     ultimately show ?thesis
-      using homotopic_paths_trans by metis
+      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid homotopic_paths_trans path_join_path_ends pathfinish_linepath pipq(2))
   next
     case False
     then show ?thesis
@@ -981,19 +931,13 @@
   assumes \<section>: "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
       and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> S\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
     shows "homotopic_paths S g h"
-proof (rule homotopic_paths_linear [OF \<section>])
-  show "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
-  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
-qed
+  using homotopic_paths_linear [OF \<section>] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)
 
 lemma homotopic_loops_nearby_explicit:
   assumes \<section>: "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
       and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> S\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
     shows "homotopic_loops S g h"
-proof (rule homotopic_loops_linear [OF \<section>])
-  show "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
-  by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
-qed
+  using homotopic_loops_linear [OF \<section>] by (metis linorder_not_le no norm_minus_commute segment_bound1 subsetI)
 
 lemma homotopic_nearby_paths:
   fixes g h :: "real \<Rightarrow> 'a::euclidean_space"
@@ -1028,9 +972,9 @@
 subsection\<open> Homotopy and subpaths\<close>
 
 lemma homotopic_join_subpaths1:
-  assumes "path g" and pag: "path_image g \<subseteq> s"
+  assumes "path g" and pag: "path_image g \<subseteq> S"
       and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}" "u \<le> v" "v \<le> w"
-    shows "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
+    shows "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
 proof -
   have 1: "t * 2 \<le> 1 \<Longrightarrow> u + t * (v * 2) \<le> v + t * (u * 2)" for t
     using affine_ineq \<open>u \<le> v\<close> by fastforce
@@ -1068,51 +1012,44 @@
 qed
 
 lemma homotopic_join_subpaths2:
-  assumes "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-    shows "homotopic_paths s (subpath w v g +++ subpath v u g) (subpath w u g)"
-by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)
+  assumes "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
+  shows "homotopic_paths S (subpath w v g +++ subpath v u g) (subpath w u g)"
+  by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)
 
 lemma homotopic_join_subpaths3:
-  assumes hom: "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-      and "path g" and pag: "path_image g \<subseteq> s"
+  assumes hom: "homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
+      and "path g" and pag: "path_image g \<subseteq> S"
       and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}"
-    shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)"
+    shows "homotopic_paths S (subpath v w g +++ subpath w u g) (subpath v u g)"
 proof -
-  have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
-  proof (rule homotopic_paths_join)
-    show "homotopic_paths s (subpath u w g) (subpath u v g +++ subpath v w g)"
-      using hom homotopic_paths_sym_eq by blast
-    show "homotopic_paths s (subpath w v g) (subpath w v g)"
-      by (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
-  qed auto
-  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)"
-    by (rule homotopic_paths_sym [OF homotopic_paths_assoc])
-       (use assms in \<open>simp_all add: path_image_subpath_subset [THEN order_trans]\<close>)
-  also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
+  obtain wvg: "path (subpath w v g)" "path_image (subpath w v g) \<subseteq> S" 
+     and wug: "path (subpath w u g)" "path_image (subpath w u g) \<subseteq> S"
+     and vug: "path (subpath v u g)" "path_image (subpath v u g) \<subseteq> S"
+    by (meson \<open>path g\<close> pag path_image_subpath_subset path_subpath subset_trans u v w)
+  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)"
+    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)))"
-  proof (rule homotopic_paths_join; simp)
-    show "path (subpath u v g) \<and> path_image (subpath u v g) \<subseteq> s"
-      by (metis \<open>path g\<close> order.trans pag path_image_subpath_subset path_subpath u v)
-    show "homotopic_paths s (subpath v w g +++ subpath w v g) (linepath (g v) (g v))"
-      by (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
-  qed 
-  also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
-  proof (rule homotopic_paths_rid)
-    show "path (subpath u v g)"
-      using \<open>path g\<close> path_subpath u v by blast
-    show "path_image (subpath u v g) \<subseteq> s"
-      by (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
-  qed
-  finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (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)"
+    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
     using homotopic_join_subpaths2 by blast
 qed
 
 proposition homotopic_join_subpaths:
-   "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
-    \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-  using le_cases3 [of u v w] homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 
-  by metis
+   "\<lbrakk>path g; path_image g \<subseteq> S; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
+    \<Longrightarrow> homotopic_paths S (subpath u v g +++ subpath v w g) (subpath u w g)"
+  by (smt (verit, del_insts) homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3)
 
 text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
 
@@ -1929,11 +1866,11 @@
 subsection\<open>Basic properties of local compactness\<close>
 
 proposition locally_compact:
-  fixes s :: "'a :: metric_space set"
+  fixes S :: "'a :: metric_space set"
   shows
-    "locally compact s \<longleftrightarrow>
-     (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
-                    openin (top_of_set s) u \<and> compact v)"
+    "locally compact S \<longleftrightarrow>
+     (\<forall>x \<in> S. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and>
+                    openin (top_of_set S) u \<and> compact v)"
      (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -1942,16 +1879,16 @@
 next
   assume r [rule_format]: ?rhs
   have *: "\<exists>u v.
-              openin (top_of_set s) u \<and>
-              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
+              openin (top_of_set S) u \<and>
+              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"
-      using r [OF \<open>x \<in> s\<close>] by auto
+    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="(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
@@ -3315,39 +3252,39 @@
 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
 
 locale\<^marker>\<open>tag important\<close> Retracts =
-  fixes s h t k
-  assumes conth: "continuous_on s h"
-      and imh: "h ` s = t"
+  fixes S h t k
+  assumes conth: "continuous_on S h"
+      and imh: "h ` S = t"
       and contk: "continuous_on t k"
-      and imk: "k ` t \<subseteq> s"
+      and imk: "k ` t \<subseteq> S"
       and idhk: "\<And>y. y \<in> t \<Longrightarrow> h(k y) = y"
 
 begin
 
 lemma homotopically_trivial_retraction_gen:
   assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> s; P f;
-                       continuous_on U g; g ` U \<subseteq> s; P g\<rbrakk>
-                       \<Longrightarrow> homotopic_with_canon P U s f g"
+      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f;
+                       continuous_on U g; g ` U \<subseteq> S; P g\<rbrakk>
+                       \<Longrightarrow> homotopic_with_canon P U S f g"
       and contf: "continuous_on U f" and imf: "f ` U \<subseteq> t" and Qf: "Q f"
       and contg: "continuous_on U g" and img: "g ` U \<subseteq> t" and Qg: "Q g"
     shows "homotopic_with_canon Q U t f g"
 proof -
   have "continuous_on U (k \<circ> f)"
     using contf continuous_on_compose continuous_on_subset contk imf by blast
-  moreover have "(k \<circ> f) ` U \<subseteq> s"
+  moreover have "(k \<circ> f) ` U \<subseteq> S"
     using imf imk by fastforce
   moreover have "P (k \<circ> f)"
     by (simp add: P Qf contf imf)
   moreover have "continuous_on U (k \<circ> g)"
     using contg continuous_on_compose continuous_on_subset contk img by blast
-  moreover have "(k \<circ> g) ` U \<subseteq> s"
+  moreover have "(k \<circ> g) ` U \<subseteq> S"
     using img imk by fastforce
   moreover have "P (k \<circ> g)"
     by (simp add: P Qg contg img)
-  ultimately have "homotopic_with_canon P U s (k \<circ> f) (k \<circ> g)"
+  ultimately have "homotopic_with_canon P U S (k \<circ> f) (k \<circ> g)"
     by (rule hom)
   then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
     apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
@@ -3363,21 +3300,21 @@
 
 lemma homotopically_trivial_retraction_null_gen:
   assumes P: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> t; Q f\<rbrakk> \<Longrightarrow> P(k \<circ> f)"
-      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
+      and Q: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> U \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> s; P f\<rbrakk>
-                     \<Longrightarrow> \<exists>c. homotopic_with_canon P U s f (\<lambda>x. c)"
+      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S; P f\<rbrakk>
+                     \<Longrightarrow> \<exists>c. homotopic_with_canon P U S f (\<lambda>x. c)"
       and contf: "continuous_on U f" and imf:"f ` U \<subseteq> t" and Qf: "Q f"
   obtains c where "homotopic_with_canon Q U t f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> U \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
   have "continuous_on U (k \<circ> f)"
     using contf continuous_on_compose continuous_on_subset contk imf by blast
-  moreover have "(k \<circ> f) ` U \<subseteq> s"
+  moreover have "(k \<circ> f) ` U \<subseteq> S"
     using imf imk by fastforce
   moreover have "P (k \<circ> f)"
     by (simp add: P Qf contf imf)
-  ultimately obtain c where "homotopic_with_canon P U s (k \<circ> f) (\<lambda>x. c)"
+  ultimately obtain c where "homotopic_with_canon P U S (k \<circ> f) (\<lambda>x. c)"
     by (metis hom)
   then have "homotopic_with_canon Q U t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
     apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
@@ -3395,30 +3332,30 @@
 
 lemma cohomotopically_trivial_retraction_gen:
   assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+      and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> U; P f;
-                       continuous_on s g; g ` s \<subseteq> U; P g\<rbrakk>
-                       \<Longrightarrow> homotopic_with_canon P s U f g"
+      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f;
+                       continuous_on S g; g ` S \<subseteq> U; P g\<rbrakk>
+                       \<Longrightarrow> homotopic_with_canon P S U f g"
       and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
       and contg: "continuous_on t g" and img: "g ` t \<subseteq> U" and Qg: "Q g"
     shows "homotopic_with_canon Q t U f g"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
   have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
-  have "continuous_on s (f \<circ> h)"
+  have "continuous_on S (f \<circ> h)"
     using contf conth continuous_on_compose imh by blast
-  moreover have "(f \<circ> h) ` s \<subseteq> U"
+  moreover have "(f \<circ> h) ` S \<subseteq> U"
     using imf imh by fastforce
   moreover have "P (f \<circ> h)"
     by (simp add: P Qf contf imf)
-  moreover have "continuous_on s (g \<circ> h)"
+  moreover have "continuous_on S (g \<circ> h)"
     using contg continuous_on_compose continuous_on_subset conth imh by blast
-  moreover have "(g \<circ> h) ` s \<subseteq> U"
+  moreover have "(g \<circ> h) ` S \<subseteq> U"
     using img imh by fastforce
   moreover have "P (g \<circ> h)"
     by (simp add: P Qg contg img)
-  ultimately have "homotopic_with_canon P s U (f \<circ> h) (g \<circ> h)"
+  ultimately have "homotopic_with_canon P S U (f \<circ> h) (g \<circ> h)"
     by (rule hom)
   then have "homotopic_with_canon Q t U (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
     apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
@@ -3433,25 +3370,25 @@
 
 lemma cohomotopically_trivial_retraction_null_gen:
   assumes P: "\<And>f. \<lbrakk>continuous_on t f; f ` t \<subseteq> U; Q f\<rbrakk> \<Longrightarrow> P(f \<circ> h)"
-      and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
+      and Q: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
-      and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> U; P f\<rbrakk>
-                       \<Longrightarrow> \<exists>c. homotopic_with_canon P s U f (\<lambda>x. c)"
+      and hom: "\<And>f g. \<lbrakk>continuous_on S f; f ` S \<subseteq> U; P f\<rbrakk>
+                       \<Longrightarrow> \<exists>c. homotopic_with_canon P S U f (\<lambda>x. c)"
       and contf: "continuous_on t f" and imf: "f ` t \<subseteq> U" and Qf: "Q f"
   obtains c where "homotopic_with_canon Q t U f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
-  have "continuous_on s (f \<circ> h)"
+  have "continuous_on S (f \<circ> h)"
     using contf conth continuous_on_compose imh by blast
-  moreover have "(f \<circ> h) ` s \<subseteq> U"
+  moreover have "(f \<circ> h) ` S \<subseteq> U"
     using imf imh by fastforce
   moreover have "P (f \<circ> h)"
     by (simp add: P Qf contf imf)
-  ultimately obtain c where "homotopic_with_canon P s U (f \<circ> h) (\<lambda>x. c)"
+  ultimately obtain c where "homotopic_with_canon P S U (f \<circ> h) (\<lambda>x. c)"
     by (metis hom)
   then have \<section>: "homotopic_with_canon Q t U (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
   proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
-    show "\<And>h. \<lbrakk>continuous_map (top_of_set s) (top_of_set U) h; P h\<rbrakk> \<Longrightarrow> Q (h \<circ> k)"
+    show "\<And>h. \<lbrakk>continuous_map (top_of_set S) (top_of_set U) h; P h\<rbrakk> \<Longrightarrow> Q (h \<circ> k)"
       using Q by auto
   qed (auto simp: contk imk)
   moreover have "homotopic_with_canon Q t U f (\<lambda>x. c)"
@@ -3549,7 +3486,7 @@
 qed
 
 lemma deformation_retraction_imp_homotopy_equivalent_space:
-  "\<lbrakk>homotopic_with (\<lambda>x. True) X X (s \<circ> r) id; retraction_maps X Y r s\<rbrakk>
+  "\<lbrakk>homotopic_with (\<lambda>x. True) X X (S \<circ> r) id; retraction_maps X Y r S\<rbrakk>
     \<Longrightarrow> X homotopy_equivalent_space Y"
   unfolding homotopy_equivalent_space_def retraction_maps_def
   using homotopic_with_id2 by fastforce