# HG changeset patch
# User desharna
# Date 1755068041 -7200
# Node ID 7ac70210d12cc5d99ad035c52ed0c470764cca92
# Parent  157aaea4c42cf46db9caeba6835702646a6c4e2b
tuned proof to reduce duplication and validation time

diff -r 157aaea4c42c -r 7ac70210d12c src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Tue Aug 12 19:16:44 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Aug 13 08:54:01 2025 +0200
@@ -3266,6 +3266,11 @@
                      "\<not> disjnt V {x. x \<in> topspace X \<and> f x = b}" 
      for a b U V
     proof -
+      have closedin_topspace: "closedin X {x \<in> topspace X. f x \<in> {y..z}}" for y z
+        using closed_real_atLeastAtMost[unfolded closed_closedin]
+          \<open>continuous_map X euclideanreal f\<close>[unfolded continuous_map_closedin]
+        by blast
+
       have "\<forall>y. connectedin X {x. x \<in> topspace X \<and> f x = y}"
         using R monotone_map by fastforce
       then have **: False if "p \<in> U \<and> q \<in> V \<and> f p = f q \<and> f q \<in> K" for p q
@@ -3280,7 +3285,7 @@
         define W where "W \<equiv> {x \<in> topspace X. f x \<in> {a..b}}"
         have "closedin X W"
           unfolding W_def
-          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
+          using closedin_topspace .
         show ?thesis
         proof (rule * [OF 1 , of "U \<inter> W" "V \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
@@ -3307,7 +3312,7 @@
         define W where "W \<equiv> {x \<in> topspace X. f x \<in> {b..a}}"
         have "closedin X W"
           unfolding W_def
-          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
+          using closedin_topspace .
         show ?thesis
         proof (rule * [OF 3, of "V \<inter> W" "U \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"