diff -r 183a28459663 -r ca486ee0e4c5 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Mon Oct 02 11:28:23 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Tue Oct 03 15:01:54 2023 +0100
@@ -2562,12 +2562,12 @@
 lemma derived_set_of_infinite_mball:
   "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mball x e)}"
   unfolding derived_set_of_infinite_openin_metric
-  by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
 
 lemma derived_set_of_infinite_mcball:
   "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mcball x e)}"
   unfolding derived_set_of_infinite_openin_metric
-  by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
 
 end
 
@@ -2671,7 +2671,8 @@
 proof -
   have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
     using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
-    by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology Pi_iff)
+    unfolding continuous_map_def Pi_iff topspace_mtopology
+    by (smt (verit, del_insts) eventually_mono)
   then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
     by metis
   show thesis
@@ -3992,7 +3993,8 @@
 lemma uniformly_continuous_map_compose:
   assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g"
   shows "uniformly_continuous_map m1 m3 (g \<circ> f)"
-  by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff uniformly_continuous_map_def)
+  using f g unfolding uniformly_continuous_map_def comp_apply Pi_iff
+  by metis
 
 lemma uniformly_continuous_map_real_const [simp]:
    "uniformly_continuous_map m euclidean_metric (\<lambda>x. c)"
@@ -5109,7 +5111,6 @@
     by (metis (full_types) completely_metrizable_space_def)
 qed
 
-
 proposition metrizable_space_product_topology:
   "metrizable_space (product_topology X I) \<longleftrightarrow>
         (product_topology X I) = trivial_topology \<or>