# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1683373330 -3600
# Node ID 30f69046f120ee5c689e3c75a80254df133e59f5
# Parent  c35f06b0931e7a0fb3a8aa17b9dae20f6f4f8f79
fixes esp to theory presentation

diff -r c35f06b0931e -r 30f69046f120 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sat May 06 11:10:23 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sat May 06 12:42:10 2023 +0100
@@ -1045,7 +1045,7 @@
 qed
 
 
-subsection\<open>T_0 spaces and the Kolmogorov quotient\<close>
+subsection\<open>$T_0$ spaces and the Kolmogorov quotient\<close>
 
 definition t0_space where
   "t0_space X \<equiv>
@@ -1646,16 +1646,18 @@
     then have "closedin X C"
       using assms by (auto simp: kc_space_def)
     show ?thesis
-      apply (rule_tac x="(topspace X - C) \<times> V" in exI)
-      using VU
-      apply (auto simp:  )
-          apply (metis VU(1) \<open>closedin X C\<close> closedin_def openin_prod_Times_iff)
-      using that apply blast
-        apply (auto simp: C_def image_iff Ball_def)
-      using V'_def VU(4) apply auto[1]
-       apply (simp add: \<open>b \<in> V\<close>)
-      using \<open>V \<subseteq> topspace Y\<close> apply blast
-      using \<open>V \<subseteq> V'\<close> \<open>V \<subseteq> topspace Y\<close> by blast
+    proof (intro exI conjI)
+      show "openin (prod_topology X Y) ((topspace X - C) \<times> V)"
+        by (simp add: VU \<open>closedin X C\<close> openin_diff openin_prod_Times_iff)
+      have "a \<notin> C"
+        using VU by (auto simp: C_def V'_def)
+      then show "(a, b) \<in> (topspace X - C) \<times> V"
+        using \<open>a \<notin> C\<close> \<open>b \<in> V\<close> that by blast
+      show "(topspace X - C) \<times> V \<subseteq> topspace X \<times> topspace Y - K"
+        using \<open>V \<subseteq> V'\<close> \<open>V \<subseteq> topspace Y\<close> 
+        apply (simp add: C_def )
+        by (smt (verit, ccfv_threshold) DiffE DiffI IntI SigmaE SigmaI image_eqI mem_Collect_eq prod.sel(1) snd_conv subset_iff)
+    qed
   qed
   ultimately show "closedin (prod_topology X Y) K"
     by (metis surj_pair closedin_def openin_subopen topspace_prod_topology)
@@ -1668,8 +1670,7 @@
 
 subsection \<open>Regular spaces\<close>
 
-text \<open>Regular spaces. These are *not* a priori assumed to be Hausdorff/T_1\<close>
-
+text \<open>Regular spaces are *not* a priori assumed to be Hausdorff or $T_1$\<close>
 
 definition regular_space 
   where "regular_space X \<equiv>