# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1744581655 -3600
# Node ID 26f9f484f266b39026a5bcf4f4e7665417ae1d0f
# Parent  d35d355f733042bbe4383417a657e134bc4c4ffe
Tidied some proofs

diff -r d35d355f7330 -r 26f9f484f266 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sat Apr 12 22:42:32 2025 +0100
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sun Apr 13 23:00:55 2025 +0100
@@ -4737,7 +4737,7 @@
     then have XKD: "compactin (subtopology X K) D"
       by (simp add: K closedin_compact_space compact_space_subtopology)
     then show "compactin X D"
-      using compactin_subtopology_imp_compact by blast
+      by (simp add: compactin_subtopology)
     show "connectedin X D"
       using D connectedin_connected_components_of connectedin_subtopology by blast
     have "K \<noteq> topspace X"
diff -r d35d355f7330 -r 26f9f484f266 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Sat Apr 12 22:42:32 2025 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Apr 13 23:00:55 2025 +0100
@@ -240,33 +240,19 @@
 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   (is "istopology ?L")
 proof -
-  have "?L {}" by blast
-  {
-    fix A B
-    assume A: "?L A" and B: "?L B"
-    from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V"
+  have "\<And>S T Sa Sb. \<lbrakk>openin U Sa; openin U Sb\<rbrakk> \<Longrightarrow> \<exists>S. Sa \<inter> V \<inter> (Sb \<inter> V) = S \<inter> V \<and> openin U S"
+    by (metis Int_assoc inf.absorb2 inf_sup_ord(2) openin_Int)
+  moreover 
+  have "\<exists>S. \<Union> \<K> = S \<inter> V \<and> openin U S"
+    if \<K>: "\<forall>K\<in>\<K>. \<exists>S. K = S \<inter> V \<and> openin U S" for \<K>
+  proof -
+    obtain f where f: "\<forall>K\<in>\<K>. K = f K \<inter> V \<and> openin U (f K)"
+      using \<K> by metis
+    with f show ?thesis
       by blast
-    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
-      using Sa Sb by blast+
-    then have "?L (A \<inter> B)" by blast
-  }
-  moreover
-  {
-    fix K
-    assume K: "K \<subseteq> Collect ?L"
-    have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
-      by blast
-    from K[unfolded th0 subset_image_iff]
-    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
-      by blast
-    have "\<Union>K = (\<Union>Sk) \<inter> V"
-      using Sk by auto
-    moreover have "openin U (\<Union>Sk)"
-      using Sk by (auto simp: subset_eq)
-    ultimately have "?L (\<Union>K)" by blast
-  }
+  qed
   ultimately show ?thesis
-    unfolding subset_eq mem_Collect_eq istopology_def by auto
+ unfolding istopology_def by force
 qed
 
 lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
@@ -346,15 +332,13 @@
 lemma subtopology_superset:
   assumes UV: "topspace U \<subseteq> V"
   shows "subtopology U V = U"
-proof -
-  { fix S
-    have "openin U S" if "openin U T" "S = T \<inter> V" for T
-      by (metis Int_subset_iff assms inf.orderE openin_subset that)
-    then have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
-      by (metis assms inf.orderE inf_assoc openin_subset)
-  }
-  then show ?thesis
-    unfolding topology_eq openin_subtopology by blast
+  unfolding topology_eq openin_subtopology
+proof (intro strip)
+  fix S
+  have "openin U S" if "openin U T" "S = T \<inter> V" for T
+    by (metis Int_subset_iff assms inf.orderE openin_subset that)
+  then show "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
+    by (metis assms inf.orderE inf_assoc openin_subset)
 qed
 
 lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
@@ -402,25 +386,25 @@
   by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
 
 lemma closedin_closed_subtopology:
-     "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
+  "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
   by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
 
 lemma closedin_trans_full:
-   "\<lbrakk>closedin (subtopology X U) S; closedin X U\<rbrakk> \<Longrightarrow> closedin X S"
+  "\<lbrakk>closedin (subtopology X U) S; closedin X U\<rbrakk> \<Longrightarrow> closedin X S"
   using closedin_closed_subtopology by blast
 
 lemma openin_subtopology_Un:
-    "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
+  "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
      \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
-by (simp add: openin_subtopology) blast
+  by (simp add: openin_subtopology) blast
 
 lemma closedin_subtopology_Un:
-    "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
+  "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
      \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
-by (simp add: closedin_subtopology) blast
+  by (simp add: closedin_subtopology) blast
 
 lemma openin_trans_full:
-   "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
+  "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
   by (simp add: openin_open_subtopology)
 
 
@@ -518,11 +502,12 @@
   have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
     unfolding T_def
     apply clarsimp
-    apply (rule_tac x="d - dist x a" in exI)
-    by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
+    subgoal for x a d
+      apply (rule_tac x="d - dist x a" in exI)
+      by (metis add_0_left dist_commute dist_triangle_lt less_diff_eq)
+    done
   assume ?rhs then have 2: "S = U \<inter> T"
-    unfolding T_def
-    by auto (metis dist_self)
+    unfolding T_def by fastforce
   from 1 2 show ?lhs
     unfolding openin_open open_dist by fast
 qed
@@ -1346,7 +1331,7 @@
 proof -
   show ?thesis
     unfolding locally_finite_in_def
-  proof safe
+  proof (intro conjI strip)
     fix x
     assume "x \<in> topspace X"
     then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
@@ -1362,8 +1347,8 @@
     then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
       using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
   next
-    show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
-      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
+    show "\<Union> (f ` \<A>) \<subseteq> topspace X"
+      using \<A> f by (force simp: locally_finite_in_def image_iff)
   qed
 qed
 
@@ -1371,7 +1356,7 @@
   assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
   shows "locally_finite_in (subtopology X S) \<A>"
   unfolding locally_finite_in_def
-proof safe
+proof (intro conjI strip)
   fix x
   assume x: "x \<in> topspace (subtopology X S)"
   then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
@@ -1388,7 +1373,7 @@
       using x \<open>x \<in> V\<close> by (simp)
   qed
 next
-  show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
+  show "\<Union> \<A> \<subseteq> topspace (subtopology X S)"
     using assms unfolding locally_finite_in_def topspace_subtopology by blast
 qed
 
@@ -1552,19 +1537,26 @@
   assumes "continuous_map X Y f"
   shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
 proof -
-  have *: "f ` (topspace X) \<subseteq> topspace Y"
-    by (meson assms continuous_map)
-  have "X closure_of T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of (f ` T)}"
-    if "T \<subseteq> topspace X" for T
+  let ?T = "S \<inter> topspace X"
+  have *: "X closure_of ?T \<subseteq> {x \<in> X closure_of ?T. f x \<in> Y closure_of (f ` ?T)}"
   proof (rule closure_of_minimal)
-    show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
-      using closure_of_subset * that  by (fastforce simp: in_closure_of)
+    have "f ` (topspace X) \<subseteq> topspace Y"
+      by (meson assms continuous_map)
+    then show "?T \<subseteq> {x \<in> X closure_of ?T. f x \<in> Y closure_of f ` ?T}"
+      using closure_of_subset by (fastforce simp: in_closure_of)
   next
-    show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
+    show "closedin X {x \<in> X closure_of ?T. f x \<in> Y closure_of f ` ?T}"
       using assms closedin_continuous_map_preimage_gen by fastforce
   qed
+  have "f x \<in> Y closure_of (f ` S)" if "x \<in> X closure_of (S \<inter> topspace X)" for x
+  proof -
+    have "f x \<in> Y closure_of f ` ?T"
+      using that * by blast
+    then show ?thesis
+      by (meson closure_of_mono inf_le1 subset_eq subset_image_iff)
+  qed
   then show ?thesis
-    by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
+    by (metis closure_of_restrict image_subsetI inf_commute)
 qed
 
 lemma continuous_map_subset_aux1: 
@@ -1677,9 +1669,7 @@
   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}}"
     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
-    using \<open>openin X'' U\<close> by blast
+    by (metis (no_types, lifting) ext \<open>openin X'' U\<close> continuous_map_def eq f g)
 qed
 
 lemma continuous_map_eq:
@@ -1704,11 +1694,10 @@
   show ?rhs
   proof -
     have "\<And>A. f \<in> (X closure_of A) \<rightarrow> subtopology X' S closure_of f ` A"
-      by (metis L continuous_map_eq_image_closure_subset image_subset_iff_funcset)
+      by (metis L continuous_map_eq_image_closure_subset)
     then show ?thesis
-      by (metis closure_of_subset_subtopology closure_of_subtopology_subset
-          closure_of_topspace continuous_map_eq_image_closure_subset
-          image_subset_iff_funcset subset_trans)
+      by (metis closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace
+          continuous_map_subset_aux2 image_subset_iff_funcset subset_trans)
   qed
 next
   assume R: ?rhs
@@ -1809,7 +1798,7 @@
 
 lemma closed_map_on_empty:
    "closed_map trivial_topology Y f"
-  by (simp add: closed_map_def closedin_topspace_empty)
+  by (simp add: closed_map_def)
 
 lemma closed_map_const:
    "closed_map X Y (\<lambda>x. c) \<longleftrightarrow> X = trivial_topology \<or> closedin Y {c}"
@@ -1868,8 +1857,7 @@
   by (metis (no_types, lifting) closed_map_def image_comp)
 
 lemma closed_map_inclusion_eq:
-   "closed_map (subtopology X S) X id \<longleftrightarrow>
-        closedin X (topspace X \<inter> S)"
+   "closed_map (subtopology X S) X id \<longleftrightarrow> closedin X (topspace X \<inter> S)"
 proof -
   have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
     by (smt (verit, best) closedin_Int closure_of_subset_eq inf_sup_aci le_iff_inf that)
@@ -1953,7 +1941,8 @@
 proof
   assume ?lhs
   then show ?rhs
-    by (simp add: closed_map_def closed_map_imp_subset_topspace closure_of_minimal closure_of_subset image_mono)
+    by (simp add: closed_map_def closed_map_imp_subset_topspace closure_of_minimal 
+        closure_of_subset image_mono)
 next
   assume ?rhs
   then show ?lhs
@@ -2048,7 +2037,7 @@
     then obtain V where V: "openin Y V" 
       and sub: "topspace Y - f ` U \<subseteq> V" "{x \<in> topspace X. f x \<in> V} \<subseteq> topspace X - U"
       using R Diff_subset \<open>closedin X U\<close> unfolding closedin_def
-      by (smt (verit, ccfv_threshold) Collect_mem_eq Collect_mono_iff)
+      by blast
     then have "f ` U \<subseteq> topspace Y - V"
       using R \<open>closedin X U\<close> closedin_subset by fastforce
     with sub have "f ` U = topspace Y - V"
@@ -2084,7 +2073,6 @@
     show "\<forall>T. ?P T"
     proof (cases "openin X U")
       case True
-      note [[unify_search_bound=3]]
       obtain V where V: "\<And>y. \<lbrakk>y \<in> topspace Y; {x \<in> topspace X. f x = y} \<subseteq> U\<rbrakk> \<Longrightarrow>
                        openin Y (V y) \<and> y \<in> V y \<and> {x \<in> topspace X. f x \<in> V y} \<subseteq> U"
         using R by (simp add: True) meson
@@ -2093,7 +2081,7 @@
         fix T
         assume "openin X U" and "T \<subseteq> topspace Y" and "{x \<in> topspace X. f x \<in> T} \<subseteq> U"
         with V show "\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
-          by (rule_tac x="\<Union>y\<in>T. V y" in exI) fastforce
+          by (intro exI [where x="\<Union>y\<in>T. V y"]) fastforce
       qed
     qed auto
   qed
@@ -2101,7 +2089,7 @@
 
 lemma open_map_in_subtopology:
    "openin Y S
-        \<Longrightarrow> open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f \<in> topspace X \<rightarrow> S"
+     \<Longrightarrow> open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f \<in> topspace X \<rightarrow> S"
   by (metis image_subset_iff_funcset open_map_def open_map_into_subtopology openin_imp_subset openin_topspace openin_trans_full)
 
 lemma open_map_from_open_subtopology:
@@ -2130,7 +2118,8 @@
     using cmf closed_map_def by blast
   moreover 
   have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
-    by (smt (verit, ccfv_SIG) \<open>closedin Y U\<close> closedin_subset fim image_iff subsetD)
+    by (metis \<open>closedin Y U\<close> closedin_imp_subset fim image_iff insert_absorb insert_subset
+        subtopology_topspace)
   then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
   ultimately show "closedin Z (g ` U)"
     by metis
@@ -2149,7 +2138,8 @@
     using cmf open_map_def by blast
   moreover 
   have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
-    by (smt (verit, ccfv_SIG) \<open>openin Y U\<close> openin_subset fim image_iff subsetD)
+    by (metis (no_types, lifting) \<open>openin Y U\<close> fim image_iff in_mono interior_of_eq
+        interior_of_subset_topspace)
   then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
   ultimately show "openin Z (g ` U)"
     by metis
@@ -2200,7 +2190,7 @@
 lemma quotient_map_eq:
   assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
   shows "quotient_map X X' g"
-  by (smt (verit) Collect_cong assms image_cong quotient_map_def)
+  using assms by (smt (verit) Collect_cong assms image_cong quotient_map_def)
 
 lemma quotient_map_compose:
   assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
@@ -2280,13 +2270,14 @@
   assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
   shows "quotient_map X X' f"
 proof -
-  { fix U
-    assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
-    then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
-      using om unfolding open_map_def by blast
-    then have "openin X' U"
+  have "openin X' U"
+    if U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}" for U
+  proof -
+    have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
+      using om that unfolding open_map_def by blast
+    then show ?thesis
       using U feq by (subst openin_subopen) force
-  }
+  qed
   moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
     using that assms unfolding continuous_map_def by blast
   ultimately show ?thesis
@@ -2334,11 +2325,7 @@
     by (simp add: L assms bijective_open_imp_closed_map quotient_imp_surjective_map)
   then show ?rhs
     using L om by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
-next
-  assume ?rhs
-  then show ?lhs
-    by (simp add: continuous_closed_imp_quotient_map)
-qed
+qed (auto simp add: continuous_closed_imp_quotient_map)
 
 lemma continuous_compose_quotient_map:
   assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
@@ -2548,7 +2535,7 @@
     show "g ` topspace Y = h ` topspace X"
       using f g by (force dest!: quotient_imp_surjective_map)
     show "continuous_map Y Z g"
-      by (smt (verit)  f g h continuous_compose_quotient_map_eq continuous_map_eq o_def)
+      by (metis comp_apply continuous_compose_quotient_map continuous_map_eq f g h)
   qed (simp add: g)
 qed
 
@@ -2942,7 +2929,9 @@
       by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
     moreover have "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)"  (is "?lhs = ?rhs")
       if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
-      by (smt (verit, del_insts) S \<open>x \<in> topspace X\<close> image_iff inj inj_on_def subsetD that)
+      unfolding image_iff
+      using S \<open>x \<in> topspace X\<close> that 
+      by (metis (full_types) inj inj_onD [OF inj] subsetD the_inv_into_f_f)
     ultimately show ?thesis
       by (auto simp flip: fim simp: all_subset_image)
   qed
@@ -2971,14 +2960,12 @@
       using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
       by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
   moreover
-  { fix x
-    assume "x \<in> topspace X"
-    then have "f x \<in> topspace Y"
-      using hom homeomorphic_imp_surjective_map by blast }
+  have "f x \<in> topspace Y" if "x \<in> topspace X" for x
+    using that hom homeomorphic_imp_surjective_map by blast 
   moreover
   { fix x
-    assume "x \<in> topspace X" and "x \<notin> X closure_of (topspace X - S)" and "f x \<in> Y closure_of (topspace Y - f ` S)"
-    then have "False"
+    assume "x \<in> topspace X" and "f x \<in> Y closure_of (topspace Y - f ` S)"
+    then have "x \<in> X closure_of (topspace X - S)"
       using homeomorphic_map_closure_of [OF hom] hom
       unfolding homeomorphic_eq_everything_map
       by (metis Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff inj_on_image_set_diff)
@@ -3007,9 +2994,10 @@
   then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
     by blast
   then show "x \<notin> Y interior_of f ` S"
-    using S hom homeomorphic_map_interior_of y(1)
+    using S hom homeomorphic_map_interior_of
     unfolding homeomorphic_map_def
-    by (smt (verit, ccfv_SIG) in_closure_of inj_on_image_mem_iff interior_of_subset_topspace) 
+    by (metis (no_types, lifting) closure_of_subset_topspace inj_on_image_mem_iff
+        interior_of_subset_closure_of subset_inj_on)
 qed
 
 lemma homeomorphic_maps_subtopologies:
@@ -3191,11 +3179,9 @@
 
 lemma connectedin_closedin:
    "connectedin X S \<longleftrightarrow>
-        S \<subseteq> topspace X \<and>
-        \<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
-                  S \<subseteq> (E1 \<union> E2) \<and>
-                  (E1 \<inter> E2 \<inter> S = {}) \<and>
-                  \<not>(E1 \<inter> S = {}) \<and> \<not>(E2 \<inter> S = {}))"
+      S \<subseteq> topspace X \<and>
+      \<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
+                S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
 proof -
   have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
              R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
@@ -3271,10 +3257,6 @@
 lemma connected_space_subconnected:
   "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. connectedin X S \<and> x \<in> S \<and> y \<in> S)" (is "?lhs = ?rhs")
 proof
-  assume ?lhs
-  then show ?rhs
-    using connectedin_topspace by blast
-next
   assume R [rule_format]: ?rhs
   have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
     and "U \<noteq> {}" "V \<noteq> {}" for U V
@@ -3284,13 +3266,13 @@
     then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
       using R [of u v] that
       by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
-    then show False
-      using that unfolding connectedin
+    with that show False
+      unfolding connectedin
       by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
   qed
   then show ?lhs
     by (auto simp: connected_space_def)
-qed
+qed (use connectedin_topspace in blast)
 
 lemma connectedin_intermediate_closure_of:
   assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
@@ -3557,6 +3539,10 @@
 lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
   by (metis compactin_subspace inf.absorb_iff2 le_inf_iff subtopology_subtopology topspace_subtopology)
 
+lemma compact_imp_compactin_subtopology:
+  assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
+  by (simp add: assms compactin_subtopology)
+
 lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
   by (simp add: compactin_subspace)
 
@@ -3655,65 +3641,6 @@
    "\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
 by (induction rule: finite_induct) (simp_all add: compactin_Un)
 
-lemma compactin_subtopology_imp_compact:
-  assumes "compactin (subtopology X S) K" shows "compactin X K"
-  using assms
-proof (clarsimp simp add: compactin_def)
-  fix \<U>
-  define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
-  assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
-  then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
-    unfolding \<V>_def by (auto simp: openin_subtopology)
-  moreover
-  assume "\<forall>\<U>. (\<forall>x\<in>\<U>. openin (subtopology X S) x) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
-  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
-    by meson
-  then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
-    unfolding \<V>_def using that by blast
-  let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
-  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
-  proof (intro exI conjI)
-    show "finite ?\<F>"
-      using \<open>finite \<F>\<close> by blast
-    show "?\<F> \<subseteq> \<U>"
-      using someI_ex [OF \<F>] by blast
-    show "K \<subseteq> \<Union>?\<F>"
-    proof clarsimp
-      fix x
-      assume "x \<in> K"
-      then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
-        using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
-        by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
-    qed
-  qed
-qed
-
-lemma compact_imp_compactin_subtopology:
-  assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
-  using assms
-proof (clarsimp simp add: compactin_def)
-  fix \<U> :: "'a set set"
-  define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
-  assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
-  then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
-    unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
-  moreover
-  assume "\<forall>\<U>. (\<forall>U\<in>\<U>. openin X U) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
-  ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
-    by meson
-  let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
-  show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
-  proof (intro exI conjI)
-    show "finite ?\<F>"
-      using \<open>finite \<F>\<close> by blast
-    show "?\<F> \<subseteq> \<U>"
-      using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
-    show "K \<subseteq> \<Union>?\<F>"
-      using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
-  qed
-qed
-
-
 proposition compact_space_fip:
    "compact_space X \<longleftrightarrow>
     (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
@@ -3825,11 +3752,7 @@
   show "finite S"
     using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
     by clarsimp (metis UN_singleton finite_subset_image infinite_super)
-next
-  assume ?rhs
-  then show ?lhs
-    by (simp add: finite_imp_compactin)
-qed
+qed (simp add: finite_imp_compactin)
 
 lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
   by (simp add: compactin_discrete_topology compact_space_def)
@@ -3987,11 +3910,10 @@
 
 lemma embedding_imp_closed_map:
    "\<lbrakk>embedding_map X Y f; closedin Y (f ` topspace X)\<rbrakk> \<Longrightarrow> closed_map X Y f"
-  unfolding closed_map_def
-  by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq)
+  by (meson closed_map_from_closed_subtopology embedding_map_def homeomorphic_imp_closed_map)
 
 lemma embedding_imp_closed_map_eq:
-   "embedding_map X Y f \<Longrightarrow> (closed_map X Y f \<longleftrightarrow> closedin Y (f ` topspace X))"
+  "embedding_map X Y f \<Longrightarrow> (closed_map X Y f \<longleftrightarrow> closedin Y (f ` topspace X))"
   using closed_map_def embedding_imp_closed_map by blast
 
 
@@ -4067,7 +3989,7 @@
 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')"
   unfolding retraction_maps_def
-  by (smt (verit, ccfv_threshold) comp_apply continuous_map_compose continuous_map_image_subset_topspace image_subset_iff)
+  by (metis comp_def 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)"
@@ -4098,19 +4020,18 @@
         \<Longrightarrow> retraction_maps X (subtopology X (s ` (topspace Y))) (s \<circ> r) id"
   unfolding retraction_maps_def
   by (auto simp: continuous_map_compose continuous_map_into_subtopology continuous_map_from_subtopology)
+
 subsection \<open>Continuity\<close>
 
 lemma continuous_on_open:
   "continuous_on S f \<longleftrightarrow>
-    (\<forall>T. openin (top_of_set (f ` S)) T \<longrightarrow>
-      openin (top_of_set S) (S \<inter> f -` T))"
+    (\<forall>T. openin (top_of_set (f ` S)) T \<longrightarrow> openin (top_of_set S) (S \<inter> f -` T))"
   unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
 lemma continuous_on_closed:
   "continuous_on S f \<longleftrightarrow>
-    (\<forall>T. closedin (top_of_set (f ` S)) T \<longrightarrow>
-      closedin (top_of_set S) (S \<inter> f -` T))"
+    (\<forall>T. closedin (top_of_set (f ` S)) T \<longrightarrow> closedin (top_of_set S) (S \<inter> f -` T))"
   unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
@@ -4140,8 +4061,7 @@
   have "openin (top_of_set (f ` S)) (T \<inter> f ` S)"
     using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
   then show ?thesis
-    using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
-    using * by auto
+    by (metis "*" assms(1) continuous_on_open)
 qed
 
 lemma continuous_closedin_preimage:
@@ -4154,8 +4074,7 @@
     using closedin_closed_Int[of T "f ` S", OF assms(2)]
     by (simp add: Int_commute)
   then show ?thesis
-    using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
-    using * by auto
+    by (metis "*" assms(1) continuous_on_closed)
 qed
 
 lemma continuous_openin_preimage_eq:
@@ -4240,7 +4159,7 @@
     proof (subst openin_subopen, clarify)
       show "\<exists>U. openin (top_of_set T) U \<and> y \<in> U \<and> U \<subseteq> T'" if "y \<in> T'" for y
         using that \<open>x \<in> S'\<close> Times_in_interior_subtopology [OF _ \<open>?lhs\<close>, of x y]
-        by simp (metis mem_Sigma_iff subsetD subsetI)
+        by (smt (verit) mem_Sigma_iff subset_iff)
     qed
     ultimately show ?rhs
       by simp
@@ -4281,11 +4200,11 @@
 proof
   assume ?lhs
   with assms show ?rhs
-    apply (simp add: Pi_iff continuous_openin_preimage_eq openin_open)
-    by (metis inf.orderE inf_assoc subsetI vimageI vimage_Int)
+    by (metis continuous_map_openin_preimage_eq continuous_map_subtopology_eu
+        topspace_euclidean_subtopology)
 next
   assume R [rule_format]: ?rhs
-  show ?lhs
+  then show ?lhs
   proof (clarsimp simp add: continuous_openin_preimage_eq)
     show "\<And>T. open T \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` T)"
       by (metis (no_types) R assms image_subset_iff_funcset image_subset_iff_subset_vimage inf.orderE inf_assoc openin_open_Int vimage_Int)
@@ -4332,56 +4251,56 @@
 We do not require \<open>UNIV\<close> to be an open set, as this will not be the case in applications. (We are
 thinking of a topology on a subset of \<open>UNIV\<close>, the remaining part of \<open>UNIV\<close> being irrelevant.)\<close>
 
-inductive generate_topology_on for S where
-  Empty: "generate_topology_on S {}"
-| Int: "generate_topology_on S a \<Longrightarrow> generate_topology_on S b \<Longrightarrow> generate_topology_on S (a \<inter> b)"
-| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on S k) \<Longrightarrow> generate_topology_on S (\<Union>K)"
-| Basis: "s \<in> S \<Longrightarrow> generate_topology_on S s"
+inductive generate_topology_on for \<S> where
+  Empty: "generate_topology_on \<S> {}"
+| Int: "generate_topology_on \<S> a \<Longrightarrow> generate_topology_on \<S> b \<Longrightarrow> generate_topology_on \<S> (a \<inter> b)"
+| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology_on \<S> k) \<Longrightarrow> generate_topology_on \<S> (\<Union>K)"
+| Basis: "s \<in> \<S> \<Longrightarrow> generate_topology_on \<S> s"
 
 lemma istopology_generate_topology_on:
-  "istopology (generate_topology_on S)"
+  "istopology (generate_topology_on \<S>)"
 unfolding istopology_def by (auto intro: generate_topology_on.intros)
 
-text \<open>The basic property of the topology generated by a set \<open>S\<close> is that it is the
-smallest topology containing all the elements of \<open>S\<close>:\<close>
+text \<open>The basic property of the topology generated by a set \<open>\<S>\<close> is that it is the
+smallest topology containing all the elements of \<open>\<S>\<close>:\<close>
 
 lemma generate_topology_on_coarsest:
-  assumes T: "istopology T" "\<And>s. s \<in> S \<Longrightarrow> T s"
-          and gen: "generate_topology_on S s0"
+  assumes T: "istopology T" "\<And>S. S \<in> \<S> \<Longrightarrow> T S"
+          and gen: "generate_topology_on \<S> s0"
   shows "T s0"
   using gen 
 by (induct rule: generate_topology_on.induct) (use T in \<open>auto simp: istopology_def\<close>)
 
 abbreviation\<^marker>\<open>tag unimportant\<close> topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
-  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
+  where "topology_generated_by \<S> \<equiv> topology (generate_topology_on \<S>)"
 
 lemma openin_topology_generated_by_iff:
-  "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
-  using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
+  "openin (topology_generated_by \<S>) s \<longleftrightarrow> generate_topology_on \<S> s"
+  using topology_inverse'[OF istopology_generate_topology_on[of \<S>]] by simp
 
 lemma openin_topology_generated_by:
-  "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
+  "openin (topology_generated_by \<S>) s \<Longrightarrow> generate_topology_on \<S> s"
 using openin_topology_generated_by_iff by auto
 
 lemma topology_generated_by_topspace [simp]:
-  "topspace (topology_generated_by S) = (\<Union>S)"
+  "topspace (topology_generated_by \<S>) = (\<Union>\<S>)"
 proof
   {
-    fix s assume "openin (topology_generated_by S) s"
-    then have "generate_topology_on S s" by (rule openin_topology_generated_by)
-    then have "s \<subseteq> (\<Union>S)" by (induct, auto)
+    fix S assume "openin (topology_generated_by \<S>) S"
+    then have "generate_topology_on \<S> S" by (rule openin_topology_generated_by)
+    then have "S \<subseteq> (\<Union>\<S>)" by (induct, auto)
   }
-  then show "topspace (topology_generated_by S) \<subseteq> (\<Union>S)"
+  then show "topspace (topology_generated_by \<S>) \<subseteq> (\<Union>\<S>)"
     unfolding topspace_def by auto
 next
-  have "generate_topology_on S (\<Union>S)"
-    using generate_topology_on.UN[OF generate_topology_on.Basis, of S S] by simp
-  then show "(\<Union>S) \<subseteq> topspace (topology_generated_by S)"
+  have "generate_topology_on \<S> (\<Union>\<S>)"
+    using generate_topology_on.UN[OF generate_topology_on.Basis, of \<S> \<S>] by simp
+  then show "(\<Union>\<S>) \<subseteq> topspace (topology_generated_by \<S>)"
     unfolding topspace_def using openin_topology_generated_by_iff by auto
 qed
 
 lemma topology_generated_by_Basis:
-  "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
+  "s \<in> \<S> \<Longrightarrow> openin (topology_generated_by \<S>) s"
   by (simp add: Basis openin_topology_generated_by_iff)
 
 lemma generate_topology_on_Inter:
@@ -4777,7 +4696,7 @@
   assumes "continuous_map T1 T2 g"
   shows "continuous_map (pullback_topology A f T1) T2 (g o f)"
 unfolding continuous_map_alt
-proof (auto)
+proof (intro conjI strip)
   fix U::"'b set" assume "openin T2 U"
   then have "openin T1 (g-`U \<inter> topspace T1)"
     using assms unfolding continuous_map_alt by auto
@@ -4790,18 +4709,16 @@
   finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
     by auto
 next
-  fix x assume "x \<in> topspace (pullback_topology A f T1)"
-  then have "f x \<in> topspace T1"
-    unfolding topspace_pullback_topology by auto
-  then show "g (f x) \<in> topspace T2"
-    using assms unfolding continuous_map_def by auto
+  show "g \<circ> f \<in> topspace (pullback_topology A f T1) \<rightarrow> topspace T2"
+    using assms unfolding continuous_map_def topspace_pullback_topology
+    by fastforce
 qed
 
 proposition continuous_map_pullback' [intro]:
   assumes "continuous_map T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
   shows "continuous_map T1 (pullback_topology A f T2) g"
-unfolding continuous_map_alt
-proof (auto)
+  unfolding continuous_map_alt
+proof (intro conjI strip)
   fix U assume "openin (pullback_topology A f T2) U"
   then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
     unfolding openin_pullback_topology by auto
@@ -4817,15 +4734,11 @@
     using assms(1) \<open>openin T2 V\<close> by auto
   finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
 next
-  fix x assume "x \<in> topspace T1"
-  have "(f o g) x \<in> topspace T2"
-    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
-  then have "g x \<in> f-`(topspace T2)"
-    unfolding comp_def by blast
-  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
-  ultimately show "g x \<in> topspace (pullback_topology A f T2)"
-    unfolding topspace_pullback_topology by blast
+  show "g \<in> topspace T1 \<rightarrow> topspace (pullback_topology A f T2)"
+    using assms unfolding continuous_map_def topspace_pullback_topology
+    by fastforce
 qed
+
 subsection\<open>Proper maps (not a priori assumed continuous) \<close>
 
 definition proper_map