diff -r 8281047b896d -r 1b17f0a41aa3 src/HOL/Analysis/Sum_Topology.thy
--- a/src/HOL/Analysis/Sum_Topology.thy	Tue Apr 15 15:30:21 2025 +0100
+++ b/src/HOL/Analysis/Sum_Topology.thy	Wed Apr 16 21:13:27 2025 +0100
@@ -106,8 +106,7 @@
 
 lemma continuous_map_component_injection:
    "i \<in> I \<Longrightarrow> continuous_map(X i) (sum_topology X I) (\<lambda>x. (i,x))"
-  apply (clarsimp simp: continuous_map_def openin_sum_topology)
-  by (smt (verit, best) Collect_cong mem_Collect_eq openin_subset subsetD)
+  by (auto simp: continuous_map_def openin_sum_topology Collect_conj_eq openin_Int)
 
 lemma subtopology_sum_topology:
   "subtopology (sum_topology X I) (Sigma I S) =
@@ -151,8 +150,12 @@
 proof -
   have "Q(X i)" if "i \<in> I" for i
   proof -
-    have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))"
-      by (meson closed_map_component_injection closed_map_def closedin_topspace major minor open_map_component_injection open_map_def openin_topspace that)
+    have "closed_map (X i) (sum_topology X I) (Pair i)"
+      by (simp add: closed_map_component_injection that)
+    moreover have "open_map (X i) (sum_topology X I) (Pair i)"
+      by (simp add: open_map_component_injection that)
+    ultimately have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))"
+      by (simp add: closed_map_def major minor open_map_def)
     then show ?thesis
       by (metis PQ embedding_map_component_injection embedding_map_imp_homeomorphic_space homeomorphic_space_sym that)
   qed