# HG changeset patch
# User nipkow
# Date 1755070497 -7200
# Node ID 304519f22c2ce13b646ae8e2864ae808482f1f35
# Parent  7ac70210d12cc5d99ad035c52ed0c470764cca92# Parent  1ee42e4832aa37de30abd26474f79292bd4f3919
prefer existing proof in Abstract_Topological_Spaces

diff -r 7ac70210d12c -r 304519f22c2c src/HOL/Analysis/Abstract_Topological_Spaces.thy
diff -r 7ac70210d12c -r 304519f22c2c src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Aug 13 08:54:01 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Aug 13 09:34:57 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