
diff -r 9e0c035d026d -r eb9a9690b8f5 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Mon Jul 10 18:48:22 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Tue Jul 11 20:21:58 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)"




