# HG changeset patch
# User paulson
# Date 1689199919 -3600
# Node ID 19c617950a8eadc3697267a59bcafa7c1ca8991f
# Parent  5f78a7e98bd0cf2871c308f9d19ff278ea39a4bf# Parent  c3376cd561a8e580f087eff0e7d6e96bfe6f3c56
merged

diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -109,7 +109,7 @@
 lemma cm_Euclidean_space_iff_continuous_on:
   "continuous_map (subtopology (Euclidean_space m) S) (Euclidean_space n) f
    \<longleftrightarrow> continuous_on (topspace (subtopology (Euclidean_space m) S)) f \<and>
-       f ` (topspace (subtopology (Euclidean_space m) S)) \<subseteq> topspace (Euclidean_space n)"
+       f \<in> (topspace (subtopology (Euclidean_space m) S)) \<rightarrow> topspace (Euclidean_space n)"
   (is "?P \<longleftrightarrow> ?Q \<and> ?R")
 proof -
   have ?Q if ?P
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -178,7 +178,7 @@
   shows "limitin Y (g \<circ> f) (g l) F"
 proof -
   have "g l \<in> topspace Y"
-    by (meson assms continuous_map_def limitin_topspace)
+    by (meson assms continuous_map f image_eqI in_mono limitin_def)
   moreover
   have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
             \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
@@ -194,14 +194,14 @@
 definition topcontinuous_at where
   "topcontinuous_at X Y f x \<longleftrightarrow>
      x \<in> topspace X \<and>
-     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+     f \<in> topspace X \<rightarrow> topspace Y \<and>
      (\<forall>V. openin Y V \<and> f x \<in> V
           \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"
 
 lemma topcontinuous_at_atin:
    "topcontinuous_at X Y f x \<longleftrightarrow>
         x \<in> topspace X \<and>
-        (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+        f \<in> topspace X \<rightarrow> topspace Y \<and>
         limitin Y f (f x) (atin X x)"
   unfolding topcontinuous_at_def
   by (fastforce simp add: limitin_atin)+
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -2583,7 +2583,7 @@
 proof
   show "?lhs \<Longrightarrow> ?rhs"
     unfolding continuous_map_eq_topcontinuous_at topcontinuous_at_def
-    by (metis centre_in_mball_iff openin_mball topspace_mtopology)
+    by (metis PiE centre_in_mball_iff openin_mball topspace_mtopology)
 next
   assume R: ?rhs
   then have "\<forall>x\<in>topspace X. f x \<in> M"
@@ -2598,7 +2598,7 @@
 
 lemma continuous_map_from_metric:
    "continuous_map mtopology X f \<longleftrightarrow>
-    f ` M \<subseteq> topspace X \<and>
+    f \<in> M \<rightarrow> topspace X \<and>
     (\<forall>a \<in> M. \<forall>U. openin X U \<and> f a \<in> U \<longrightarrow> (\<exists>r>0. \<forall>x. x \<in> M \<and> d a x < r \<longrightarrow> f x \<in> U))"
 proof (cases "f ` M \<subseteq> topspace X")
   case True
@@ -2607,7 +2607,7 @@
 next
   case False
   then show ?thesis
-    by (simp add: continuous_map_eq_image_closure_subset_gen)
+    by (simp add: continuous_map_def image_subset_iff_funcset)
 qed
 
 text \<open>An abstract formulation, since the limits do not have to be sequential\<close>
@@ -2671,7 +2671,7 @@
 proof -
   have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
     using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
-    by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology)
+    by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology Pi_iff)
   then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
     by metis
   show thesis
@@ -5107,14 +5107,14 @@
 qed
 
 
-lemma metrizable_space_product_topology:
+proposition metrizable_space_product_topology:
   "metrizable_space (product_topology X I) \<longleftrightarrow>
         topspace (product_topology X I) = {} \<or>
         countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
         (\<forall>i \<in> I. metrizable_space (X i))"
   by (metis (mono_tags, lifting) empty_metrizable_space metrizable_topology_A metrizable_topology_B metrizable_topology_D)
 
-lemma completely_metrizable_space_product_topology:
+proposition completely_metrizable_space_product_topology:
   "completely_metrizable_space (product_topology X I) \<longleftrightarrow>
         topspace (product_topology X I) = {} \<or>
         countable {i \<in> I. \<not> (\<exists>a. topspace(X i) \<subseteq> {a})} \<and>
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -894,7 +894,8 @@
 qed
 
 subsection \<open>Neigbourhood bases EXTRAS\<close>
-(* Neigbourhood bases (useful for "local" properties of various kind).       *)
+
+text \<open>Neigbourhood bases: useful for "local" properties of various kinds\<close>
 
 lemma openin_topology_neighbourhood_base_unique:
    "openin X = arbitrary union_of P \<longleftrightarrow>
@@ -1192,7 +1193,7 @@
   assumes "continuous_map X Y f" "t0_space Y" and x: "x \<in> topspace X"
   shows "f (Kolmogorov_quotient X x) = f x"
   using assms unfolding continuous_map_def t0_space_def
-  by (smt (verit, ccfv_SIG) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace x mem_Collect_eq)
+  by (smt (verit, ccfv_threshold) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace PiE mem_Collect_eq)
 
 lemma t0_space_Kolmogorov_quotient:
   "t0_space (subtopology X (Kolmogorov_quotient X ` topspace X))"
@@ -1239,7 +1240,7 @@
   have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\<rbrakk> \<Longrightarrow> f x = f y"
     using assms
     apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology)
-    by (smt (verit, del_insts) Int_iff mem_Collect_eq)
+    by (smt (verit, del_insts) Int_iff mem_Collect_eq Pi_iff)
   then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
     "g ` (topspace X \<inter> Kolmogorov_quotient X ` S) = f ` S"
     "\<And>x. x \<in> S \<Longrightarrow> g (Kolmogorov_quotient X x) = f x"
@@ -1321,7 +1322,7 @@
   obtain r where r: "continuous_map X (subtopology X S) r" "\<forall>x\<in>S. r x = x"
     using assms by (meson retract_of_space_def)
   then have \<section>: "S = {x \<in> topspace X. r x = x}"
-    using S retract_of_space_imp_subset by (force simp: continuous_map_def)
+    using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
   show ?thesis
     unfolding \<section> 
     using r continuous_map_into_fulltopology assms
@@ -1345,7 +1346,8 @@
   assume ?rhs
   then show ?lhs
     unfolding homeomorphic_maps_def
-    by (smt (verit, ccfv_threshold) continuous_map_eq continuous_map_subtopology_fst embedding_map_def embedding_map_graph homeomorphic_eq_everything_map  image_cong image_iff prod.collapse prod.inject)
+    by (smt (verit, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def 
+        embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1))
 qed
 
 
@@ -1663,9 +1665,8 @@
       have "continuous_map (subtopology X A) (subtopology Y K) f" if "kc_space X"
         unfolding continuous_map_closedin
       proof (intro conjI strip)
-        show "f x \<in> topspace (subtopology Y K)"
-          if "x \<in> topspace (subtopology X A)" for x
-          using that A_def K compactin_subset_topspace by auto
+        show "f \<in> topspace (subtopology X A) \<rightarrow> topspace (subtopology Y K)"
+          using A_def K compactin_subset_topspace by fastforce
       next
         fix C
         assume C: "closedin (subtopology Y K) C"
@@ -1927,7 +1928,7 @@
   using proper_map_paired [OF assms] by (simp add: o_def)
 
 lemma proper_map_from_composition_right:
-  assumes "Hausdorff_space Y" "proper_map X Z (g \<circ> f)" and "continuous_map X Y f"
+  assumes "Hausdorff_space Y" "proper_map X Z (g \<circ> f)" and contf: "continuous_map X Y f"
     and contg: "continuous_map Y Z g"
   shows "proper_map X Y f"
 proof -
@@ -1935,7 +1936,7 @@
   have "proper_map X Y (fst \<circ> (\<lambda>x. (f x, (g \<circ> f) x)))"
   proof (rule proper_map_compose)
     have [simp]: "x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y" for x
-      by (meson assms(3) continuous_map_def)
+      using contf continuous_map_preimage_topspace by auto
     show "proper_map X YZ (\<lambda>x. (f x, (g \<circ> f) x))"
       unfolding YZ_def
       using assms
@@ -2558,7 +2559,8 @@
       using \<open>closed_map X Y f\<close> \<open>closedin X C\<close> \<open>openin X U2\<close> closed_map_def by blast
     moreover
     have "f x \<in> topspace Y - f ` (C - U2)"
-      using \<open>closedin X C\<close> \<open>continuous_map X Y f\<close> \<open>x \<in> topspace X\<close> closedin_subset continuous_map_def subV by fastforce
+      using \<open>closedin X C\<close> \<open>continuous_map X Y f\<close> \<open>x \<in> topspace X\<close> closedin_subset continuous_map_def subV 
+      by (fastforce simp: Pi_iff)
     ultimately
     obtain V1 V2 where VV: "openin Y V1" "openin Y V2" "f x \<in> V1" 
                 and subV2: "f ` (C - U2) \<subseteq> V2" and "disjnt V1 V2"
@@ -3213,7 +3215,7 @@
   assume x: "x \<in> topspace X"
   then obtain U K where "openin X' U" "compactin X' K" "f x \<in> U" "U \<subseteq> K"
     using assms unfolding locally_compact_space_def perfect_map_def
-    by (metis (no_types, lifting) continuous_map_closedin)
+    by (metis (no_types, lifting) continuous_map_closedin Pi_iff)
   show "\<exists>U K. openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
   proof (intro exI conjI)
     have "continuous_map X X' f"
@@ -3433,7 +3435,7 @@
       by (auto simp: retraction_maps_def)
     show "S \<subseteq> {x \<in> topspace Y. r' x \<in> U}" "T \<subseteq> {x \<in> topspace Y. r' x \<in> V}"
       using openin_continuous_map_preimage UV r' \<open>closedin Y S\<close> \<open>closedin Y T\<close> 
-      by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff)
+      by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff Pi_iff)
     show "disjnt {x \<in> topspace Y. r' x \<in> U} {x \<in> topspace Y. r' x \<in> V}"
       using \<open>disjnt U V\<close> by (auto simp: disjnt_def)
   qed
@@ -4293,7 +4295,7 @@
   unfolding quasi_component_of_def
 proof (intro strip conjI)
   show "f x \<in> topspace Y" "f y \<in> topspace Y"
-    using assms by (simp_all add: continuous_map_def quasi_component_of_def)
+    using assms by (simp_all add: continuous_map_def quasi_component_of_def Pi_iff)
   fix T
   assume "closedin Y T \<and> openin Y T"
   with assms show "(f x \<in> T) = (f y \<in> T)"
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -1454,7 +1454,7 @@
 
 definition continuous_map where
   "continuous_map X Y f \<equiv>
-     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+     f \<in> topspace X \<rightarrow> topspace Y \<and>
      (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
 
 lemma continuous_map:
@@ -1466,17 +1466,24 @@
    "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
   by (auto simp: continuous_map_def)
 
+lemma continuous_map_funspace:
+   "continuous_map X Y f \<Longrightarrow> f \<in> topspace X \<rightarrow> topspace Y"
+  by (auto simp: continuous_map_def)
+
 lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
   by (auto simp: continuous_map_def)
 
+lemma continuous_map_on_empty2: "topspace Y = {} \<Longrightarrow> continuous_map X Y f \<longleftrightarrow> topspace X = {}"
+  by (auto simp: continuous_map_def)
+
 lemma continuous_map_closedin:
    "continuous_map X Y f \<longleftrightarrow>
-         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+         f \<in> topspace X \<rightarrow> topspace Y \<and>
          (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
 proof -
   have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
-    if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+    if "f \<in> topspace X \<rightarrow> topspace Y"
   proof -
     have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
       using that by blast
@@ -1555,9 +1562,7 @@
   shows "continuous_map X Y f"
   unfolding continuous_map_closedin
 proof (intro conjI ballI allI impI)
-  fix x
-  assume "x \<in> topspace X"
-  then show "f x \<in> topspace Y"
+  show "f \<in> topspace X \<rightarrow> topspace Y"
     using assms closure_of_subset_topspace by fastforce
 next
   fix C
@@ -1588,9 +1593,9 @@
 
 lemma continuous_map_eq_image_closure_subset_gen:
      "continuous_map X Y f \<longleftrightarrow>
-        f ` (topspace X) \<subseteq> topspace Y \<and>
+        f \<in> topspace X \<rightarrow> topspace Y \<and>
         (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
-  using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
+  by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)
 
 lemma continuous_map_closure_preimage_subset:
    "continuous_map X Y f
@@ -1650,15 +1655,13 @@
   shows "continuous_map X X'' (g \<circ> f)"
   unfolding continuous_map_def
 proof (intro conjI ballI allI impI)
-  fix x
-  assume "x \<in> topspace X"
-  then show "(g \<circ> f) x \<in> topspace X''"
+  show "g \<circ> f \<in> topspace X \<rightarrow> topspace X''"
     using assms unfolding continuous_map_def by force
 next
   fix U
   assume "openin X'' U"
   have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
-    by auto (meson f continuous_map_def)
+    using continuous_map_image_subset_topspace f by force
   show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
     unfolding eq
     using assms unfolding continuous_map_def
@@ -1672,7 +1675,7 @@
   have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
     using assms by auto
   show ?thesis
-    using assms by (simp add: continuous_map_def eq)
+    using assms by (force simp add: continuous_map_def eq)
 qed
 
 lemma restrict_continuous_map [simp]:
@@ -2327,8 +2330,8 @@
   shows "continuous_map X' X'' g"
   unfolding quotient_map_def continuous_map_def
 proof (intro conjI ballI allI impI)
-  show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
-    using assms unfolding quotient_map_def
+  show "g \<in> topspace X' \<rightarrow> topspace X''"
+    using assms unfolding quotient_map_def Pi_iff
     by (metis (no_types, opaque_lifting) continuous_map_image_subset_topspace image_comp image_subset_iff)
 next
   fix U'' :: "'c set"
@@ -2657,7 +2660,7 @@
        \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
       \<Longrightarrow> homeomorphic_maps X Y f' g'"
   unfolding homeomorphic_maps_def
-  by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
+  by (metis continuous_map_eq continuous_map_image_subset_topspace image_subset_iff) 
 
 lemma homeomorphic_maps_sym:
      "homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
@@ -2711,7 +2714,7 @@
         homeomorphic_maps Y X'' g k
         \<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
   unfolding homeomorphic_maps_def
-  by (auto simp: continuous_map_compose; simp add: continuous_map_def)
+  by (auto simp: continuous_map_compose; simp add: continuous_map_def Pi_iff)
 
 lemma homeomorphic_eq_everything_map:
    "homeomorphic_map X Y f \<longleftrightarrow>
@@ -2784,11 +2787,13 @@
   show ?rhs
   proof (intro conjI bijective_open_imp_homeomorphic_map L)
     show "open_map X Y f"
-      using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
+      using L using open_eq_continuous_inverse_map [of concl: X Y f g] 
+      by (simp add: continuous_map_def Pi_iff)
     show "open_map Y X g"
-      using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
+      using L using open_eq_continuous_inverse_map [of concl: Y X g f] 
+      by (simp add: continuous_map_def Pi_iff)
     show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
-      using L by (force simp: continuous_map_closedin)+
+      using L by (force simp: continuous_map_closedin Pi_iff)+
     show "inj_on f (topspace X)" "inj_on g (topspace Y)"
       using L unfolding inj_on_def by metis+
   qed
@@ -3020,7 +3025,7 @@
     have "f ` (topspace X \<inter> S) \<subseteq> topspace Y \<inter> T"
       using S hom homeomorphic_imp_surjective_map by fastforce
     then show "f ` (topspace X \<inter> S) = topspace Y \<inter> T"
-      using that unfolding homeomorphic_maps_def continuous_map_def
+      using that unfolding homeomorphic_maps_def continuous_map_def Pi_iff
       by (smt (verit, del_insts) Int_iff S image_iff subsetI subset_antisym)
   qed
   then show ?thesis
@@ -3064,8 +3069,8 @@
 lemma homeomorphic_empty_space_eq:
   assumes "topspace X = {}"
   shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
-  unfolding homeomorphic_maps_def homeomorphic_space_def
-  by (metis assms continuous_map_on_empty continuous_map_closedin ex_in_conv)
+  using assms
+  by (auto simp: homeomorphic_maps_def homeomorphic_space_def continuous_map_def)
 
 lemma homeomorphic_space_unfold:
   assumes "X homeomorphic_space Y"
@@ -3993,7 +3998,8 @@
 lemma retraction_maps_eq:
    "\<lbrakk>retraction_maps X Y f g; \<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>x. x \<in> topspace Y \<Longrightarrow> g x = g' x\<rbrakk>
         \<Longrightarrow> retraction_maps X Y f' g'"
-  unfolding retraction_maps_def by (metis (no_types, lifting) continuous_map_def continuous_map_eq)
+  unfolding retraction_maps_def
+  by (metis continuous_map_eq continuous_map_image_subset_topspace image_subset_iff)
 
 lemma section_map_eq:
    "\<lbrakk>section_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> section_map X Y g"
@@ -4012,8 +4018,8 @@
 proof
   assume ?lhs
   then obtain g where "homeomorphic_maps X Y f g"
-    unfolding homeomorphic_maps_def retraction_map_def section_map_def
-    by (smt (verit, best) continuous_map_def retraction_maps_def)
+    unfolding homeomorphic_maps_def retraction_map_def section_map_def 
+    by (smt (verit) Pi_iff continuous_map_def retraction_maps_def)
   then show ?rhs
     using homeomorphic_map_maps by blast
 next
@@ -4034,7 +4040,7 @@
   unfolding quotient_map_def
 proof (intro conjI subsetI allI impI)
   show "f ` topspace X = topspace Y"
-    using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def)
+    using assms by (force simp: retraction_map_def retraction_maps_def continuous_map_def Pi_iff)
 next
   fix U
   assume U: "U \<subseteq> topspace Y"
@@ -4043,12 +4049,13 @@
        "openin Y {x \<in> topspace Y. g x \<in> {x \<in> topspace X. f x \<in> U}}" for g
     using openin_subopen U that by fastforce
   then show "openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
-    using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def)
+    using assms by (auto simp: retraction_map_def retraction_maps_def continuous_map_def Pi_iff)
 qed
 
 lemma retraction_maps_compose:
    "\<lbrakk>retraction_maps X Y f f'; retraction_maps Y Z g g'\<rbrakk> \<Longrightarrow> retraction_maps X Z (g \<circ> f) (f' \<circ> g')"
-  by (clarsimp simp: retraction_maps_def continuous_map_compose) (simp add: continuous_map_def)
+  unfolding retraction_maps_def
+  by (smt (verit, ccfv_threshold) comp_apply continuous_map_compose continuous_map_image_subset_topspace image_subset_iff)
 
 lemma retraction_map_compose:
    "\<lbrakk>retraction_map X Y f; retraction_map Y Z g\<rbrakk> \<Longrightarrow> retraction_map X Z (g \<circ> f)"
@@ -4567,16 +4574,16 @@
   assumes P: "openin Y = arbitrary union_of P"
   shows
    "continuous_map X Y f \<longleftrightarrow>
-    (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+    f \<in> topspace X \<rightarrow> topspace Y \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
  (is "?lhs=?rhs")
 proof
   assume L: ?lhs 
-  then have "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
-    by (meson continuous_map_def)
+  then have "f \<in> topspace X \<rightarrow> topspace Y"
+    by (simp add: continuous_map_funspace)
   moreover have "\<And>U. P U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
     using L assms continuous_map openin_topology_base_unique by fastforce
   ultimately show ?rhs by auto
-qed (simp add: assms continuous_map_into_topology_base)
+qed (simp add: assms Pi_iff continuous_map_into_topology_base)
 
 lemma continuous_map_into_topology_subbase:
   fixes U P
@@ -4613,13 +4620,13 @@
   assumes "Y = topology(arbitrary union_of (finite intersection_of P relative_to U))"
   shows
    "continuous_map X Y f \<longleftrightarrow>
-    (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+    f \<in> topspace X \<rightarrow> topspace Y \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
    (is "?lhs=?rhs")
 proof
   assume L: ?lhs 
   show ?rhs
   proof (intro conjI strip)
-    show "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+    show "f \<in> topspace X \<rightarrow> topspace Y"
       using L continuous_map_def by fastforce
     fix V
     assume "P V"
@@ -5048,8 +5055,9 @@
   with fim inj have eq: "{x \<in> topspace X. f x = y} = {x \<in> topspace X. (g \<circ> f) x = g y}"
     by (auto simp: Pi_iff inj_onD)
   show "compactin X {x \<in> topspace X. f x = y}"
-    unfolding eq
-    by (smt (verit) Collect_cong \<open>y \<in> topspace Y\<close> contf continuous_map_closedin gf proper_map_def)
+    using contf gf \<open>y \<in> topspace Y\<close>
+    unfolding eq continuous_map_def proper_map_def
+ by blast
 qed
 
 
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -872,7 +872,7 @@
     show "continuous_map (subtopology X ?T) Y g"
       by (simp add: contg)
     have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
-      by (smt (verit, del_insts) DiffI mem_Collect_eq subset_iff closure_of_mono continuous_map_closedin contp) 
+      by (smt (verit) Collect_mono_iff DiffI closure_of_mono continuous_map contp image_subset_iff)
     then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
       by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
   qed
@@ -1352,7 +1352,7 @@
 lemma homeomorphic_path_connected_space_imp:
      "\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def
-  by (metis (no_types, opaque_lifting) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
+  by (smt (verit, ccfv_threshold) homeomorphic_imp_surjective_map homeomorphic_maps_def homeomorphic_maps_map path_connectedin_continuous_map_image path_connectedin_topspace)
 
 lemma homeomorphic_path_connected_space:
    "X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y"
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -490,10 +490,10 @@
     using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
   ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
 next
-  have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
-    using assms continuous_map_def by fastforce
+  have "f \<in> topspace T1 \<rightarrow> topspace (product_topology T I)"
+    using assms continuous_map_funspace by (force simp: Pi_iff)
   then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
-    by (simp add: product_topology_def)
+    by (fastforce simp add: product_topology_def Pi_iff)
 qed
 
 lemma continuous_map_product_then_coordinatewise [intro]:
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -4026,7 +4026,7 @@
         qed auto
       qed
       then show "continuous_map (top_of_set ?S) X g"
-        by (simp add: continuous_map_def gf)
+        by (simp add: "1" continuous_map)
     qed (auto simp: gf)
   qed
 qed
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -190,7 +190,7 @@
   have f: "f x = (?g x, ?h x)" for x
     by auto
   show ?thesis
-  proof (cases "(\<forall>x \<in> topspace Z. ?g x \<in> topspace X) \<and> (\<forall>x \<in> topspace Z. ?h x \<in> topspace Y)")
+  proof (cases "?g \<in> topspace Z \<rightarrow> topspace X \<and> ?h \<in> topspace Z \<rightarrow> topspace Y")
     case True
     show ?thesis
     proof safe
@@ -199,7 +199,7 @@
         unfolding continuous_map_def using True that
         apply clarify
         apply (drule_tac x="U \<times> topspace Y" in spec)
-        by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
+        by (auto simp: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
       with True show "continuous_map Z X (fst \<circ> f)"
         by (auto simp: continuous_map_def)
     next
@@ -208,7 +208,7 @@
         unfolding continuous_map_def using True that
         apply clarify
         apply (drule_tac x="topspace X \<times> V" in spec)
-        by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
+        by (simp add: openin_prod_Times_iff mem_Times_iff Pi_iff cong: conj_cong)
       with True show "continuous_map Z Y (snd \<circ> f)"
         by (auto simp: continuous_map_def)
     next
@@ -227,9 +227,9 @@
           done
       qed
       show "continuous_map Z (prod_topology X Y) f"
-        using True by (simp add: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
+        using True by (force simp: continuous_map_def openin_prod_topology_alt mem_Times_iff *)
     qed
-  qed (auto simp: continuous_map_def)
+  qed (force simp: continuous_map_def)
 qed
 
 lemma continuous_map_paired:
@@ -402,7 +402,7 @@
       using \<C> by simp
     obtain \<U> \<V> where \<U>: "\<And>U. U \<in> \<U> \<Longrightarrow> openin X U" "\<Y>' = (\<lambda>U. U \<times> topspace Y) ` \<U>"
       and \<V>: "\<And>V. V \<in> \<V> \<Longrightarrow> openin Y V" "\<X>' = (\<lambda>V. topspace X \<times> V) ` \<V>"
-      using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp add: subset_iff)
+      using XY by (clarsimp simp add: \<X>_def \<Y>_def subset_image_iff) (force simp: subset_iff)
     have "\<exists>\<D>. finite \<D> \<and> \<D> \<subseteq> \<X>' \<union> \<Y>' \<and> topspace X \<times> topspace Y \<subseteq> \<Union> \<D>"
     proof -
       have "topspace X \<subseteq> \<Union>\<U> \<or> topspace Y \<subseteq> \<Union>\<V>"
@@ -463,7 +463,7 @@
           show "(finite intersection_of (\<lambda>x. x \<in> \<X> \<or> x \<in> \<Y>)) (U \<times> V)"
             apply (simp add: intersection_of_def \<X>_def \<Y>_def)
             apply (rule_tac x="{(U \<times> topspace Y),(topspace X \<times> V)}" in exI)
-            using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp add:)
+            using \<open>openin X U\<close> \<open>openin Y V\<close> openin_subset UV apply (fastforce simp:)
             done
         qed
         ultimately show ?thesis
@@ -489,12 +489,18 @@
 
 lemma homeomorphic_maps_prod:
    "homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
-        topspace(prod_topology X Y) = {} \<and>
-        topspace(prod_topology X' Y') = {} \<or>
-        homeomorphic_maps X X' f f' \<and>
-        homeomorphic_maps Y Y' g g'"
+        topspace(prod_topology X Y) = {} \<and> topspace(prod_topology X' Y') = {} 
+      \<or> homeomorphic_maps X X' f f' \<and> homeomorphic_maps Y Y' g g'"  (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
   unfolding homeomorphic_maps_def continuous_map_prod_top
-  by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
+  by (auto simp: continuous_map_on_empty continuous_map_on_empty2 ball_conj_distrib)
+next
+  show "?rhs \<Longrightarrow> ?lhs"
+  unfolding homeomorphic_maps_def 
+  by (auto simp: continuous_map_prod_top continuous_map_on_empty continuous_map_on_empty2)
+qed
+
 
 lemma homeomorphic_maps_swap:
    "homeomorphic_maps (prod_topology X Y) (prod_topology Y X)
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -451,7 +451,8 @@
   fix x y
   assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
   then obtain U V where "openin Y U" "openin Y V" "f x \<in> U" "f y \<in> V" "disjnt U V"
-    using assms unfolding Hausdorff_space_def continuous_map_def by (meson inj_onD)
+    using assms
+    by (smt (verit, ccfv_threshold) Hausdorff_space_def continuous_map image_subset_iff inj_on_def)
   show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
   proof (intro exI conjI)
     show "openin X {x \<in> topspace X. f x \<in> U}"
@@ -501,12 +502,12 @@
       if "(x,y) \<in> topspace (prod_topology X Y) - (\<lambda>x. (x, f x)) ` topspace X"
       for x y
     proof -
-      have "x \<in> topspace X" "y \<in> topspace Y" "y \<noteq> f x"
+      have "x \<in> topspace X" and y: "y \<in> topspace Y" "y \<noteq> f x"
         using that by auto
-      moreover have "f x \<in> topspace Y"
-        by (meson \<open>x \<in> topspace X\<close> continuous_map_def f)
-      ultimately obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V"
-        using Y Hausdorff_space_def by metis
+      then have "f x \<in> topspace Y"
+        using continuous_map_image_subset_topspace f by blast
+      then obtain U V where UV: "openin Y U" "openin Y V" "f x \<in> U" "y \<in> V" "disjnt U V"
+        using Y y Hausdorff_space_def by metis
       show ?thesis
       proof (intro exI conjI)
         show "openin X {x \<in> topspace X. f x \<in> U}"
@@ -547,10 +548,8 @@
   show "continuous_map (subtopology Y (f ` (topspace X))) X g"
     unfolding continuous_map_closedin
   proof (intro conjI ballI allI impI)
-    fix x
-    assume "x \<in> topspace (subtopology Y (f ` topspace X))"
-    then show "g x \<in> topspace X"
-      by (auto simp: gf)
+    show "g \<in> topspace (subtopology Y (f ` topspace X)) \<rightarrow> topspace X"
+      using gf by auto
   next
     fix C
     assume C: "closedin X C"
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Analysis/Urysohn.thy
--- a/src/HOL/Analysis/Urysohn.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -380,7 +380,7 @@
       and ga: "g ` SA \<subseteq> {- d}" and gb: "g ` SB \<subseteq> {d}"
       using Urysohn_lemma \<open>normal_space X\<close> by metis
     then have g_le_d: "\<And>x. x \<in> topspace X \<Longrightarrow> \<bar>g x\<bar> \<le> d"
-      by (simp add: abs_le_iff continuous_map_def minus_le_iff)
+      by (fastforce simp: abs_le_iff continuous_map_def minus_le_iff)
     have g_eq_d: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<le> -d\<rbrakk> \<Longrightarrow> g x = -d"
       using ga by (auto simp: SA_def)
     have g_eq_negd: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<ge> d\<rbrakk> \<Longrightarrow> g x = d"
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Homology/Brouwer_Degree.thy
--- a/src/HOL/Homology/Brouwer_Degree.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Brouwer_Degree.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -1026,7 +1026,7 @@
     have rimeq: "r ` (topspace (subtopology (nsphere n) {x. x k \<le> 0}) \<inter> {x. x k = 0})
                = topspace (subtopology (nsphere n) {x. 0 \<le> x k}) \<inter> {x. x k = 0}"
       using continuous_map_eq_topcontinuous_at continuous_map_nsphere_reflection topcontinuous_at_atin
-      by (fastforce simp: r_def)
+      by (fastforce simp: r_def Pi_iff)
     show "?f \<in> iso ?G (relative_homology_group p (subtopology (nsphere n) {x. x k \<ge> 0}) {x. x k = 0})"
       using homeomorphic_map_relative_homology_iso [OF hmrs Int_lower1 rimeq]
       by (metis hom_induced_restrict relative_homology_group_restrict)
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Homology/Homology_Groups.thy
--- a/src/HOL/Homology/Homology_Groups.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Homology_Groups.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -508,8 +508,8 @@
         hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
            \<in> carrier (relative_homology_group p Y T)"
       for p X S Y f T c
-      using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]]
-      by (simp add: image_subset_iff subtopology_restrict continuous_map_def)
+      using hom_carrier [OF 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]] 
+            continuous_map_image_subset_topspace by fastforce
     have inhom: "(\<lambda>c. if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
                       c \<in> carrier (relative_homology_group p X S)
             then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
@@ -530,10 +530,10 @@
         proof (cases "continuous_map X Y f")
           case True
           then have "f ` (topspace X \<inter> S) \<subseteq> topspace Y"
-            by (meson IntE continuous_map_def image_subsetI)
+            using continuous_map_image_subset_topspace by blast
           then show ?thesis
             using True False that
-          using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
+            using 1 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p]
           by (simp add: 4 continuous_map_image_subset_topspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
         qed (simp add: group.is_monoid)
       qed
@@ -543,7 +543,7 @@
               f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
         for p X S Y T f c
       using 2 [of X Y f "topspace X \<inter> S" "topspace Y \<inter> T" p c]
-      by simp (meson IntE continuous_map_def image_subsetI)
+            continuous_map_image_subset_topspace by fastforce
     show ?thesis
       apply (rule_tac x="\<lambda>p X S Y T f c.
                if continuous_map X Y f \<and> f ` (topspace X \<inter> S) \<subseteq> T \<and>
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Wed Jul 12 23:11:59 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)
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/Homology/Simplices.thy
--- a/src/HOL/Homology/Simplices.thy	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/Homology/Simplices.thy	Wed Jul 12 23:11:59 2023 +0100
@@ -699,7 +699,7 @@
    "\<lbrakk>singular_simplex p X c;
      \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk>
     \<Longrightarrow> simplex_map p f c = simplex_map p g c"
-  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def)
+  by (auto simp: singular_simplex_def simplex_map_def continuous_map_def Pi_iff)
 
 lemma simplex_map_id_gen:
    "\<lbrakk>singular_simplex p X c;
@@ -879,14 +879,14 @@
     have "continuous_map (subtopology (product_topology (\<lambda>n. euclideanreal) UNIV) (standard_simplex p)) X f"
       using \<open>singular_simplex p X f\<close> singular_simplex_def by blast
     then have "\<And>c. c \<notin> standard_simplex p \<or> f c = a"
-      by (simp add: assms continuous_map_def)
+      by (simp add: assms continuous_map_def Pi_iff)
     then show ?thesis
       by (metis (no_types) L extensional_restrict restrict_ext singular_simplex_def)
   qed
 next
   assume ?rhs
   with assms show ?lhs
-    by (auto simp: singular_simplex_def topspace_subtopology)
+    by (auto simp: singular_simplex_def)
 qed
 
 lemma singular_chain_singleton:
diff -r 5f78a7e98bd0 -r 19c617950a8e src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Jul 12 22:05:19 2023 +0200
+++ b/src/HOL/ROOT	Wed Jul 12 23:11:59 2023 +0100
@@ -98,7 +98,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=1800, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
@@ -111,7 +111,7 @@
     "root.bib"
 
 session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   theories
     Complex_Analysis
@@ -125,7 +125,7 @@
     Metric_Arith_Examples
 
 session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
-  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
+  options [timeout=300, document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Algebra"
@@ -322,6 +322,7 @@
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   "
+  options [timeout = 300]
   sessions
     "HOL-Algebra"
   theories
@@ -846,6 +847,7 @@
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
+  options [timeout = 600]
   sessions
     "HOL-Combinatorics"
   theories