--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Feb 06 15:41:23 2023 +0000
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Tue Feb 07 14:10:08 2023 +0000
@@ -624,6 +624,10 @@
 
 named_theorems fps_expansion_intros
 
+lemma has_fps_expansion_schematicI:
+  "f has_fps_expansion A \<Longrightarrow> A = B \<Longrightarrow> f has_fps_expansion B"
+  by simp
+
 lemma fps_nth_fps_expansion:
   fixes f :: "complex \<Rightarrow> complex"
   assumes "f has_fps_expansion F"