--- 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)"
--- 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