diff -r 5a0d1075911c -r a1de627d417a src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Tue Apr 08 19:06:00 2025 +0100
@@ -618,6 +618,11 @@
     by (auto simp: isCont_def)
 qed
   
+lemma analytic_on_imp_nicely_meromorphic_on:
+  "f analytic_on A \<Longrightarrow> f nicely_meromorphic_on A"
+  by (meson analytic_at_imp_isCont analytic_on_analytic_at
+            analytic_on_imp_meromorphic_on isContD nicely_meromorphic_on_def)
+
 lemma remove_sings_meromorphic [meromorphic_intros]:
   assumes "f meromorphic_on A"
   shows   "remove_sings f meromorphic_on A"