# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1587247997 -3600
# Node ID fbd77ee16f25b9819d9be5cc760d8800b2424459
# Parent  ed065b4a85f2da41245516a822438dbcc06a1a30
more applys

diff -r ed065b4a85f2 -r fbd77ee16f25 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Fri Apr 17 22:59:26 2020 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Sat Apr 18 23:13:17 2020 +0100
@@ -1018,10 +1018,9 @@
   obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - S \<Longrightarrow> e \<le> dist x y"
     using separate_compact_closed [of "path_image g" "-S"] assms by force
   show ?thesis
-    apply (intro exI conjI)
-    using e [unfolded dist_norm]
-    apply (auto simp: intro!: homotopic_paths_nearby_explicit assms  \<open>e > 0\<close>)
-    by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
+    apply (intro exI conjI strip)
+    using e [unfolded dist_norm] \<open>e > 0\<close>
+    by (fastforce simp: path_image_def intro!: homotopic_paths_nearby_explicit assms)+
 qed
 
 lemma homotopic_nearby_loops:
@@ -1035,9 +1034,8 @@
     using separate_compact_closed [of "path_image g" "-S"] assms by force
   show ?thesis
     apply (intro exI conjI)
-    using e [unfolded dist_norm]
-    apply (auto simp: intro!: homotopic_loops_nearby_explicit assms  \<open>e > 0\<close>)
-    by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
+    using e [unfolded dist_norm] \<open>e > 0\<close>
+    by (fastforce simp: path_image_def intro!: homotopic_loops_nearby_explicit assms)+
 qed
 
 
@@ -1133,27 +1131,27 @@
 text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
 
 lemma path_component_imp_homotopic_points:
-    "path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
-apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
-                 pathstart_def pathfinish_def path_image_def path_def, clarify)
-apply (rule_tac x="g \<circ> fst" in exI)
-apply (intro conjI continuous_intros continuous_on_compose)+
-apply (auto elim!: continuous_on_subset)
-done
+  assumes "path_component S a b"
+  shows "homotopic_loops S (linepath a a) (linepath b b)"
+proof -
+  obtain g :: "real \<Rightarrow> 'a" where g: "continuous_on {0..1} g" "g ` {0..1} \<subseteq> S" "g 0 = a" "g 1 = b"
+    using assms by (auto simp: path_defs)
+  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)
+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 (simp add: path_component_def homotopic_loops_def homotopic_with_def
-                 pathstart_def pathfinish_def path_image_def path_def, clarify)
+apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
 apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
-apply (intro conjI continuous_intros continuous_on_compose)+
-apply (auto elim!: continuous_on_subset)
+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"
+   "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])
 
@@ -1189,14 +1187,17 @@
 lemma simply_connected_eq_contractible_loop_any:
   fixes S :: "_::real_normed_vector set"
   shows "simply_connected S \<longleftrightarrow>
-            (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and>
-                  pathfinish p = pathstart p \<and> a \<in> S
+            (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<and> a \<in> S
                   \<longrightarrow> homotopic_loops S p (linepath a a))"
-  unfolding simply_connected_def
-apply (rule iffI, force, clarify)
-  apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
-using homotopic_loops_sym apply blast+
-done
+        (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
 
 lemma simply_connected_eq_contractible_loop_some:
   fixes S :: "_::real_normed_vector set"
@@ -1325,14 +1326,14 @@
     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 apply (simp add: path_image_def) by force
+      using that by (force simp add: 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)
     have "path (snd \<circ> p)"
       by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF \<open>path p\<close>])
     moreover have "path_image (snd \<circ> p) \<subseteq> T"
-      using that apply (simp add: path_image_def) by force
+      using that by (force simp: path_image_def)
     ultimately have p2: "homotopic_loops T (snd \<circ> p) (linepath b b)"
       using T that
       by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
@@ -1340,7 +1341,7 @@
       using p1 p2 unfolding homotopic_loops
       apply clarify
       apply (rename_tac h k)
-      apply (rule_tac x="\<lambda>z. Pair (h z) (k z)" in exI)
+      apply (rule_tac x="\<lambda>z. (h z, k z)" in exI)
       apply (force intro: continuous_intros simp: pathstart_def pathfinish_def)+
       done
   qed
@@ -1413,8 +1414,7 @@
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and S: "contractible S"
     obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
-  apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
-  using assms by (auto simp: comp_def)
+  by (auto simp: comp_def intro: nullhomotopic_through_contractible [OF continuous_on_id _ f S])
 
 lemma homotopic_through_contractible:
   fixes S :: "_::real_normed_vector set"
@@ -1485,8 +1485,7 @@
   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"
-    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
-    using ST by blast
+    using ST by (blast intro: a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
   then show ?thesis
     unfolding starlike_def using bexI [OF _ \<open>a \<in> T\<close>]
     by (simp add: closed_segment_eq_open)
@@ -1500,16 +1499,16 @@
 proof -
   obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
     using S by (auto simp: starlike_def)
-  have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
-    apply clarify
-    apply (erule a [unfolded closed_segment_def, THEN subsetD], simp)
-    apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
-    done
+  have "\<And>t b. 0 \<le> t \<and> t \<le> 1 \<Longrightarrow>
+              \<exists>u. (1 - t) *\<^sub>R b + t *\<^sub>R a = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
+    by (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
+  then have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
+    using a [unfolded closed_segment_def] by force
   then have "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
     using \<open>a \<in> S\<close>
-    apply (simp add: homotopic_with_def)
+    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 (intro conjI ballI continuous_on_compose continuous_intros; simp add: P)
+    apply (force simp add: P intro: continuous_intros)
     done
   then show ?thesis
     using that by blast
@@ -1601,9 +1600,8 @@
     apply (rule exI [where x=a])
     apply (rule exI [where x=b])
     apply (rule exI [where x = "\<lambda>z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
-    apply (intro conjI ballI continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
     using hsub ksub
-    apply auto
+    apply (fastforce intro!: continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
     done
 qed
 
@@ -1614,13 +1612,11 @@
 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)
 
@@ -1640,8 +1636,7 @@
     shows "locally P t"
   using assms
   unfolding locally_def
-  apply (elim all_forward)
-  by (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans)
+  by (elim all_forward) (meson dual_order.trans 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)"
@@ -1653,16 +1648,21 @@
 lemma locally_singleton [iff]:
   fixes a :: "'a::metric_space"
   shows "locally P {a} \<longleftrightarrow> P {a}"
-apply (simp add: locally_def openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR cong: conj_cong)
-using zero_less_one by blast
+proof -
+  have "\<forall>x::real. \<not> 0 < x \<Longrightarrow> P {a}"
+    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)
+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
+  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
 
 lemma locally_Int:
   assumes S: "locally P S" and T: "locally P T"
@@ -1700,11 +1700,14 @@
          where opeS: "openin (top_of_set S) U1 \<and> P U2 \<and> x \<in> U1 \<and> U1 \<subseteq> U2 \<and> U2 \<subseteq> U"
            and opeT: "openin (top_of_set T) V1 \<and> Q V2 \<and> y \<in> V1 \<and> V1 \<subseteq> V2 \<and> V2 \<subseteq> V"
     by (meson PS QT locallyE)
-  with \<open>U \<times> V \<subseteq> W\<close> show "\<exists>u v. openin (top_of_set (S \<times> T)) u \<and> R v \<and> (x,y) \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> W"
-    apply (rule_tac x="U1 \<times> V1" in exI)
-    apply (rule_tac x="U2 \<times> V2" in exI)
-    apply (auto simp: openin_Times R openin_Times_eq)
-    done
+  then have "openin (top_of_set (S \<times> T)) (U1 \<times> V1)"
+    by (simp add: openin_Times)
+  moreover have "R (U2 \<times> V2)"
+    by (simp add: R opeS opeT)
+  moreover have "U1 \<times> V1 \<subseteq> U2 \<times> V2 \<and> U2 \<times> V2 \<subseteq> W"
+    using opeS opeT \<open>U \<times> V \<subseteq> W\<close> by auto 
+  ultimately show "\<exists>U V. openin (top_of_set (S \<times> T)) U \<and> R V \<and> (x,y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+    using opeS opeT by auto 
 qed
 
 
@@ -1744,7 +1747,7 @@
   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
   have "V \<subseteq> g ` f ` V"
-    by (metis hom homeomorphism_def homeomorphism_of_subsets set_eq_subset \<open>V \<subseteq> S\<close>)
+    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)
   have "openin (top_of_set (g ` T)) U"
@@ -1752,10 +1755,16 @@
   then have 1: "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"
-    apply (rule_tac x="f ` V" in exI)
-    apply (intro conjI Q [OF \<open>P V\<close> homv])
-    using \<open>W \<subseteq> T\<close> \<open>y \<in> W\<close>  \<open>f ` V \<subseteq> W\<close>  uv  apply (auto simp: fv)
-    done
+  proof (intro exI conjI)
+    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
   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)
 qed
@@ -1798,8 +1807,8 @@
 lemma locally_translation:
   fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
   shows "(\<And>S. P ((+) a ` S) = P S) \<Longrightarrow> locally P ((+) a ` S) = locally P S"
-apply (rule homeomorphism_locally [OF homeomorphism_translation])
-  by (metis (no_types) homeomorphism_def)
+  using homeomorphism_locally [OF homeomorphism_translation]
+  by (metis (full_types) homeomorphism_image2)
 
 lemma locally_injective_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1848,13 +1857,9 @@
   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"
-    apply (subst openin_subopen, clarify)
-    apply (rule_tac x=T in exI, auto)
-    done
+    by (subst openin_subopen, blast)
   have 2: "openin (top_of_set S) ?B"
-    apply (subst openin_subopen, clarify)
-    apply (rule_tac x=T in exI, auto)
-    done
+    by (subst openin_subopen, blast)
   have \<section>: "?A \<inter> ?B = {}"
     by (clarsimp simp: set_eq_iff) (metis (no_types, hide_lams) Int_iff opD openin_Int)
   have *: "S \<subseteq> ?A \<union> ?B"
@@ -1922,12 +1927,20 @@
 qed
 
 lemma locally_constant:
-     "connected S \<Longrightarrow> locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S"
-apply (simp add: locally_def)
-apply (rule iffI)
- apply (rule locally_constant_imp_constant, assumption)
- apply (metis (mono_tags, hide_lams) constant_on_def constant_on_subset openin_subtopology_self)
-by (meson constant_on_subset openin_imp_subset order_refl)
+  assumes "connected S"
+  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, hide_lams) constant_on_def constant_on_subset openin_subtopology_self)
+  then show ?rhs
+    using assms
+    by (simp add: locally_constant_imp_constant)
+next
+  assume ?rhs then show ?lhs
+    using assms by (metis constant_on_subset locallyI openin_imp_subset order_refl)
+qed
 
 
 subsection\<open>Basic properties of local compactness\<close>
@@ -1942,9 +1955,7 @@
 proof
   assume ?lhs
   then show ?rhs
-    apply clarify
-    apply (erule_tac w = "s \<inter> ball x 1" in locallyE)
-    by auto
+    by (meson locallyE openin_subtopology_self)
 next
   assume r [rule_format]: ?rhs
   have *: "\<exists>u v.
@@ -1964,10 +1975,7 @@
       done
   qed
   show ?lhs
-    apply (rule locallyI)
-    apply (subst (asm) openin_open)
-    apply (blast intro: *)
-    done
+    by (rule locallyI) (metis "*" Int_iff openin_open)
 qed
 
 lemma locally_compactE:
@@ -1980,12 +1988,18 @@
 lemma locally_compact_alt:
   fixes S :: "'a :: heine_borel set"
   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)"
-  apply (simp add: locally_compact)
-  apply (intro ball_cong ex_cong refl iffI)
-   apply (meson bounded_subset closure_minimal compact_eq_bounded_closed dual_order.trans)
-  by (meson closure_subset compact_closure)
+         (\<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
 
 lemma locally_compact_Int_cball:
   fixes S :: "'a :: heine_borel set"
@@ -2150,10 +2164,10 @@
       by (meson \<open>x \<in> S\<close> opS openin_contains_cball)
     then have "cball x e2 \<inter> (S \<union> T) = cball x e2 \<inter> S"
       by force
-    ultimately show ?thesis
-      apply (rule_tac x="min e1 e2" in exI)
-      apply (auto simp: cball_min_Int \<open>e2 > 0\<close> inf_assoc closed_Int)
-      by (metis closed_Int closed_cball inf_left_commute)
+    ultimately have "closed (cball x (min e1 e2) \<inter> (S \<union> T))"
+      by (metis (no_types, lifting) cball_min_Int closed_Int closed_cball inf_assoc inf_commute)
+    then show ?thesis
+      by (metis \<open>0 < e1\<close> \<open>0 < e2\<close> min_def)
   qed
   moreover have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> T" for x
   proof -
@@ -2571,9 +2585,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"
-apply (clarsimp simp add: locally_def)
-apply (drule assms; blast)
-done
+  by (force simp add: locally_def dest: assms)
 
 lemma locally_path_connected_2:
   assumes "locally path_connected S"
@@ -5537,11 +5549,23 @@
     by (simp add: homotopic_on_emptyI)
 next
   case equal
-  then show ?thesis
-    apply (auto simp: homotopic_with)
-    apply (rule_tac x="\<lambda>x. h (0, a)" in exI)
-     apply (fastforce simp add:)
-    using continuous_on_const by blast
+  show ?thesis
+  proof
+    assume L: ?lhs
+    with equal have [simp]: "f a \<in> S"
+      using homotopic_with_imp_subset1 by fastforce
+    obtain h:: "real \<times> 'M \<Rightarrow> 'a" 
+      where h: "continuous_on ({0..1} \<times> {a}) h" "h ` ({0..1} \<times> {a}) \<subseteq> S" "h (0, a) = f a"    
+      using L equal by (auto simp: homotopic_with)
+    then have "continuous_on (cball a r) (\<lambda>x. h (0, a))" "(\<lambda>x. h (0, a)) ` cball a r \<subseteq> S"
+      by (auto simp: equal)
+    then show ?rhs
+      using h(3) local.equal by force
+  next
+    assume ?rhs
+    then show ?lhs
+      using equal continuous_on_const by (force simp add: homotopic_with)
+  qed
 next
   case greater
   let ?P = "continuous_on {x. norm(x - a) = r} f \<and> f ` {x. norm(x - a) = r} \<subseteq> S"
@@ -5560,11 +5584,11 @@
   proof
     fix g
     assume g: "continuous_on (cball a r) g \<and> g ` cball a r \<subseteq> S \<and> (\<forall>xa\<in>sphere a r. g xa = f xa)"
-    then
-    show ?P
-      apply (safe elim!: continuous_on_eq [OF continuous_on_subset])
-      apply (auto simp: dist_norm norm_minus_commute)
-      by (metis dist_norm image_subset_iff mem_sphere norm_minus_commute sphere_cball subsetCE)
+    then have "f ` {x. norm (x - a) = r} \<subseteq> S"
+      using sphere_cball [of a r] unfolding image_subset_iff sphere_def
+      by (metis dist_commute dist_norm mem_Collect_eq subset_eq)
+    with g show ?P
+      by (auto simp: dist_norm norm_minus_commute elim!: continuous_on_eq [OF continuous_on_subset])
   qed
   moreover have ?thesis if ?P
   proof
@@ -5577,12 +5601,15 @@
       by (auto simp: homotopic_with_def)
     obtain b1::'M where "b1 \<in> Basis"
       using SOME_Basis by auto
-    have "c \<in> S"
-      apply (rule him [THEN subsetD])
-      apply (rule_tac x = "(0, a + r *\<^sub>R b1)" in image_eqI)
-      using h greater \<open>b1 \<in> Basis\<close>
-       apply (auto simp: dist_norm)
-      done
+    have "c \<in> h ` ({0..1} \<times> sphere a r)"
+    proof
+      show "c = h (0, a + r *\<^sub>R b1)"
+        by (simp add: h)
+      show "(0, a + r *\<^sub>R b1) \<in> {0..1::real} \<times> sphere a r"
+        using greater \<open>b1 \<in> Basis\<close> by (auto simp: dist_norm)
+    qed
+    then have "c \<in> S"
+      using him by blast
     have uconth: "uniformly_continuous_on ({0..1::real} \<times> (sphere a r)) h"
       by (force intro: compact_Times conth compact_uniformly_continuous)
     let ?g = "\<lambda>x. h (norm (x - a)/r,