# HG changeset patch
# User nipkow
# Date 1755069625 -7200
# Node ID 1ee42e4832aa37de30abd26474f79292bd4f3919
# Parent  157aaea4c42cf46db9caeba6835702646a6c4e2b
tuned

diff -r 157aaea4c42c -r 1ee42e4832aa 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 09:20:25 2025 +0200
@@ -3279,8 +3279,8 @@
         case 1
         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 closed_real_atLeastAtMost assms
+           unfolding W_def closed_closedin continuous_map_closedin by blast 
         show ?thesis
         proof (rule * [OF 1 , of "U \<inter> W" "V \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
@@ -3306,8 +3306,8 @@
         case 3
         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 closed_real_atLeastAtMost assms
+           unfolding W_def closed_closedin continuous_map_closedin by blast 
         show ?thesis
         proof (rule * [OF 3, of "V \<inter> W" "U \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
diff -r 157aaea4c42c -r 1ee42e4832aa src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Aug 12 19:16:44 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Aug 13 09:20:25 2025 +0200
@@ -954,8 +954,8 @@
   show ?thesis
   proof
     assume ?lhs
-    with r show ?rhs
-      by (metis Pi_I' imageI invertible_fixpoint_property[of T i S r])
+    with r Pi_I' imageI invertible_fixpoint_property[of T i S r] show ?rhs
+      by metis
   next
     assume ?rhs
     with r show ?lhs