diff -r 00b59ba22c01 -r 882b80bd10c8 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Mar 25 21:34:36 2025 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Wed Mar 26 21:11:04 2025 +0000
@@ -41,6 +41,9 @@
   "(\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e) \<Longrightarrow> uniform_limit S f l F"
   by (simp add: uniform_limit_iff)
 
+lemma uniform_limit_singleton [simp]: "uniform_limit {x} f g F \<longleftrightarrow> ((\<lambda>n. f n x) \<longlongrightarrow> g x) F"
+  by (simp add: uniform_limit_iff tendsto_iff)
+
 lemma uniform_limit_sequentially_iff:
   "uniform_limit S f l sequentially \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. dist (f n x) (l x) < e)"
   unfolding uniform_limit_iff eventually_sequentially ..
@@ -71,6 +74,19 @@
     by eventually_elim (use \<delta> l in blast)
 qed
 
+lemma uniform_limit_compose':
+  assumes "uniform_limit A f g F" and "h \<in> B \<rightarrow> A"
+  shows   "uniform_limit B (\<lambda>n x. f n (h x)) (\<lambda>x. g (h x)) F"
+  unfolding uniform_limit_iff
+proof (intro strip)
+  fix e :: real
+  assume e: "e > 0"
+  with assms(1) have "\<forall>\<^sub>F n in F. \<forall>x\<in>A. dist (f n x) (g x) < e"
+    by (auto simp: uniform_limit_iff)
+  thus "\<forall>\<^sub>F n in F. \<forall>x\<in>B. dist (f n (h x)) (g (h x)) < e"
+    by eventually_elim (use assms(2) in blast)
+qed
+
 lemma metric_uniform_limit_imp_uniform_limit:
   assumes f: "uniform_limit S f a F"
   assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
@@ -982,7 +998,7 @@
   shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
 apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
 apply (rule eventuallyI continuous_intros assms)+
-apply (simp add:)
+apply auto
 done
 
 lemma powser_continuous_sums: