diff -r 021fb1b01de5 -r 74c75da4cb01 src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Tue Jul 11 20:22:08 2023 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Wed Jul 12 18:28:11 2023 +0100
@@ -54,7 +54,7 @@
     moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
       by (metis subt_eq topspace_subtopology)
     ultimately show ?thesis
-      using cmr continuous_map_def by fastforce
+      using fim by auto
   qed
   then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
     using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
@@ -623,7 +623,7 @@
         using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
       then have "ret 0 x \<in> topspace (Euclidean_space n)"
         if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
-        using that by (simp add: continuous_map_def retraction_maps_def)
+        using that by (metis continuous_map_image_subset_topspace image_subset_iff retraction_maps_def)
       then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
         by (auto simp: local.cong ret_def hi_def lo_def)
       show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
@@ -1353,7 +1353,7 @@
     have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
       unfolding 1
     proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
-      show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
+      show hesub: "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
         using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
       have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
       proof (intro continuous_on_compose)
@@ -1365,12 +1365,10 @@
           by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
         with cmh show "continuous_on (e ` {- r<..<r}) h"
           by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
-        have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
-          using subCr cmh by (simp add: continuous_map_def image_subset_iff)
-        moreover have "continuous_on (topspace ?E) e'"
+         have "continuous_on (topspace ?E) e'"
           by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
-        ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
-          by (simp add: e'_def continuous_on_subset)
+        then show "continuous_on (h ` e ` {- r<..<r}) e'"
+          using hesub by (simp add: 1 e'_def continuous_on_subset)
       qed
       show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
         using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)