diff -r 88f101c3cfe2 -r 111b1b2a2d13 src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Tue Apr 15 23:04:44 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Tue Apr 15 15:17:25 2025 +0200
@@ -242,6 +242,94 @@
     using False remove_sings_eqI by auto
 qed simp
 
+lemma remove_sings_analytic_on:
+  assumes "isolated_singularity_at f z" "f \<midarrow>z\<rightarrow> c"
+  shows   "remove_sings f analytic_on {z}"
+proof -
+  from assms(1) obtain A where A: "open A" "z \<in> A" "f holomorphic_on (A - {z})"
+    using analytic_imp_holomorphic isolated_singularity_at_iff_analytic_nhd by auto
+  have ana: "f analytic_on (A - {z})"
+    by (subst analytic_on_open) (use A in auto)
+
+  have "remove_sings f holomorphic_on A"
+  proof (rule no_isolated_singularity)
+    have "f holomorphic_on (A - {z})"
+      by fact
+    moreover have "remove_sings f holomorphic_on (A - {z}) \<longleftrightarrow> f holomorphic_on (A - {z})"
+      by (intro holomorphic_cong remove_sings_at_analytic) (auto intro!: analytic_on_subset[OF ana])
+    ultimately show "remove_sings f holomorphic_on (A - {z})"
+      by blast
+    hence "continuous_on (A-{z}) (remove_sings f)"
+      by (intro holomorphic_on_imp_continuous_on)
+    moreover have "isCont (remove_sings f) z"
+      using assms isCont_def remove_sings_eqI tendsto_remove_sings_iff by blast
+    ultimately show "continuous_on A (remove_sings f)"
+      by (metis A(1) DiffI closed_singleton continuous_on_eq_continuous_at open_Diff singletonD)
+  qed (use A(1) in auto)
+  thus ?thesis
+    using A(1,2) analytic_at by blast
+qed
+
+lemma residue_remove_sings [simp]:
+  assumes "isolated_singularity_at f z"
+  shows   "residue (remove_sings f) z = residue f z"
+proof -
+  from assms have "eventually (\<lambda>w. remove_sings f w = f w) (at z)"
+    using eventually_remove_sings_eq_at by blast
+  then obtain A where A: "open A" "z \<in> A" "\<And>w. w \<in> A - {z} \<Longrightarrow> remove_sings f w = f w"
+    by (subst (asm) eventually_at_topological) blast
+  from A(1,2) obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "cball z \<epsilon> \<subseteq> A"
+    using open_contains_cball_eq by blast
+  hence eq: "remove_sings f w = f w" if "w \<in> cball z \<epsilon> - {z}" for w
+    using that A \<epsilon> by blast
+
+  define P where "P = (\<lambda>f c \<epsilon>. (f has_contour_integral of_real (2 * pi) * \<i> * c) (circlepath z \<epsilon>))"
+  have "P (remove_sings f) c \<delta> \<longleftrightarrow> P f c \<delta>" if "0 < \<delta>" "\<delta> < \<epsilon>" for c \<delta>
+    unfolding P_def using \<open>\<epsilon> > 0\<close> that by (intro has_contour_integral_cong) (auto simp: eq)
+  hence *: "(\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P (remove_sings f) c \<epsilon>) \<longleftrightarrow> (\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P f c \<epsilon>)" if "e \<le> \<epsilon>" for c e
+    using that by force
+  have **: "(\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P (remove_sings f) c \<epsilon>) \<longleftrightarrow> (\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P f c \<epsilon>)" for c
+  proof
+    assume "(\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P (remove_sings f) c \<epsilon>)"
+    then obtain e where "e > 0" "\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P (remove_sings f) c \<epsilon>"
+      by blast
+    thus "(\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P f c \<epsilon>)"
+      by (intro exI[of _ "min e \<epsilon>"]) (use *[of "min e \<epsilon>" c] \<epsilon>(1) in auto)
+  next
+    assume "(\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P f c \<epsilon>)"
+    then obtain e where "e > 0" "\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P f c \<epsilon>"
+      by blast
+    thus "(\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> P (remove_sings f) c \<epsilon>)"
+      by (intro exI[of _ "min e \<epsilon>"]) (use *[of "min e \<epsilon>" c] \<epsilon>(1) in auto)
+  qed
+  show ?thesis
+    unfolding residue_def by (intro arg_cong[of _ _ Eps] ext **[unfolded P_def])
+qed    
+
+lemma remove_sings_shift_0:
+  "remove_sings f z = remove_sings (\<lambda>w. f (z + w)) 0"
+proof (cases "\<exists>c. f \<midarrow>z\<rightarrow> c")
+  case True
+  then obtain c where c: "f \<midarrow>z\<rightarrow> c"
+    by blast
+  from c have "remove_sings f z = c"
+    by (rule remove_sings_eqI)
+  moreover have "remove_sings (\<lambda>w. f (z + w)) 0 = c"
+    by (rule remove_sings_eqI) (use c in \<open>simp_all add: at_to_0' filterlim_filtermap add_ac\<close>)
+  ultimately show ?thesis
+    by simp
+next
+  case False
+  hence "\<not>(\<exists>c. (\<lambda>w. f (z + w)) \<midarrow>0\<rightarrow> c)"
+    by (simp add: at_to_0' filterlim_filtermap add_ac)
+  with False show ?thesis
+    by (simp add: remove_sings_def)
+qed
+
+lemma remove_sings_shift_0':
+  "NO_MATCH 0 z \<Longrightarrow> remove_sings f z = remove_sings (\<lambda>w. f (z + w)) 0"
+  by (rule remove_sings_shift_0)
+
 
 subsection \<open>Meromorphicity\<close>
 
@@ -735,6 +823,37 @@
     using eq[OF w not_pole[OF w]] .
 qed
 
+lemma nicely_meromorphic_on_unop:
+  assumes "f nicely_meromorphic_on A"
+  assumes "f meromorphic_on A \<Longrightarrow> (\<lambda>z. h (f z)) meromorphic_on A"
+  assumes "\<And>z. z \<in> A \<Longrightarrow> is_pole f z \<Longrightarrow> is_pole (\<lambda>z. h (f z)) z"
+  assumes "\<And>z. z \<in> f ` A \<Longrightarrow> isCont h z"
+  assumes "h 0 = 0"
+  shows   "(\<lambda>z. h (f z)) nicely_meromorphic_on A"
+  unfolding nicely_meromorphic_on_def
+proof (intro conjI ballI)
+  show "(\<lambda>z. h (f z)) meromorphic_on A"
+    using assms(1,2) by (auto simp: nicely_meromorphic_on_def)
+next
+  fix z assume z: "z \<in> A"
+  hence "is_pole f z \<and> f z = 0 \<or> f \<midarrow>z\<rightarrow> f z"
+    using assms by (auto simp: nicely_meromorphic_on_def)
+  thus "is_pole (\<lambda>z. h (f z)) z \<and> h (f z) = 0 \<or> (\<lambda>z. h (f z)) \<midarrow>z\<rightarrow> h (f z)"
+  proof (rule disj_forward)
+    assume "is_pole f z \<and> f z = 0"
+    thus "is_pole (\<lambda>z. h (f z)) z \<and> h (f z) = 0"
+      using assms z by auto
+  next
+    assume *: "f \<midarrow>z\<rightarrow> f z"
+    from z assms have "isCont h (f z)"
+      by auto
+    with * show "(\<lambda>z. h (f z)) \<midarrow>z\<rightarrow> h (f z)"
+      using continuous_within continuous_within_compose3 by blast
+  qed
+qed
+
+
+
 subsection \<open>Closure properties and proofs for individual functions\<close>
 
 lemma meromorphic_on_const [intro, meromorphic_intros]: "(\<lambda>_. c) meromorphic_on A"
@@ -848,6 +967,33 @@
   by (rule laurent_expansion_intros exI ballI
            assms[THEN meromorphic_on_imp_has_laurent_expansion] | assumption)+
 
+lemma nicely_meromorphic_on_const [intro]: "(\<lambda>_. c) nicely_meromorphic_on A"
+  unfolding nicely_meromorphic_on_def by auto
+
+lemma nicely_meromorphic_on_cmult_left [intro]:
+  assumes "f nicely_meromorphic_on A"
+  shows   "(\<lambda>z. c * f z) nicely_meromorphic_on A"
+proof (cases "c = 0")
+  case [simp]: False
+  show ?thesis
+    using assms by (rule nicely_meromorphic_on_unop) (auto intro!: meromorphic_intros)
+qed (auto intro!: nicely_meromorphic_on_const)
+
+lemma nicely_meromorphic_on_cmult_right [intro]:
+  assumes "f nicely_meromorphic_on A"
+  shows   "(\<lambda>z. f z * c) nicely_meromorphic_on A"
+  using nicely_meromorphic_on_cmult_left[OF assms, of c] by (simp add: mult.commute)
+
+lemma nicely_meromorphic_on_scaleR [intro]:
+  assumes "f nicely_meromorphic_on A"
+  shows   "(\<lambda>z. c *\<^sub>R f z) nicely_meromorphic_on A"
+  using assms by (auto simp: scaleR_conv_of_real)
+
+lemma nicely_meromorphic_on_uminus [intro]:
+  assumes "f nicely_meromorphic_on A"
+  shows   "(\<lambda>z. -f z) nicely_meromorphic_on A"
+  using nicely_meromorphic_on_cmult_left[OF assms, of "-1"] by simp
+
 lemma meromorphic_on_If [meromorphic_intros]:
   assumes "f meromorphic_on A" "g meromorphic_on B"
   assumes "\<And>z. z \<in> A \<Longrightarrow> z \<in> B \<Longrightarrow> f z = g z" "open A" "open B" "C \<subseteq> A \<union> B"
@@ -954,6 +1100,31 @@
     by eventually_elim auto
 qed
 
+lemma remove_sings_constant_on_open_iff:
+  assumes "f meromorphic_on A" "open A"
+  shows   "remove_sings f constant_on A \<longleftrightarrow> (\<exists>c. \<forall>\<^sub>\<approx>x\<in>A. f x = c)"
+proof
+  assume "remove_sings f constant_on A"
+  then obtain c where c: "remove_sings f z = c" if "z \<in> A" for z
+    using that by (auto simp: constant_on_def)
+  have "\<forall>\<^sub>\<approx>x\<in>A. x \<in> A"
+    using \<open>open A\<close> by (simp add: eventually_in_cosparse)
+  hence "\<forall>\<^sub>\<approx>x\<in>A. f x = c"
+    using eventually_remove_sings_eq[OF assms(1)] by eventually_elim (use c in auto)
+  thus "\<exists>c. \<forall>\<^sub>\<approx>x\<in>A. f x = c"
+    by blast
+next
+  assume "\<exists>c. \<forall>\<^sub>\<approx>x\<in>A. f x = c"
+  then obtain c where c: "\<forall>\<^sub>\<approx>x\<in>A. f x = c"
+    by blast
+  have "\<forall>\<^sub>\<approx>x\<in>A. remove_sings f x = c"
+    using eventually_remove_sings_eq[OF assms(1)] c by eventually_elim auto
+  hence "remove_sings f z = c" if "z \<in> A" for z using that 
+    by (meson assms(2) c eventually_cosparse_open_eq remove_sings_eqI tendsto_eventually)
+  thus "remove_sings f constant_on A"
+    unfolding constant_on_def by blast
+qed
+
 
 text \<open>
   A meromorphic function on a connected domain takes any given value either almost everywhere
@@ -1274,4 +1445,418 @@
     by (auto simp: constant_on_def)
 qed
 
+
+subsection \<open>More on poles and zeros\<close>
+
+lemma zorder_prod:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x meromorphic_on {z}"
+  assumes "eventually (\<lambda>z. (\<Prod>x\<in>A. f x z) \<noteq> 0) (at z)"
+  shows   "zorder (\<lambda>z. \<Prod>x\<in>A. f x z) z = (\<Sum>x\<in>A. zorder (f x) z)"
+  using assms
+proof (induction A rule: infinite_finite_induct)
+  case (insert a A)
+  have "zorder (\<lambda>z. \<Prod>x\<in>insert a A. f x z) z = zorder (\<lambda>z. f a z * (\<Prod>x\<in>A. f x z)) z"
+    using insert.hyps by simp
+  also have "\<dots> = zorder (f a) z + zorder (\<lambda>z. \<Prod>x\<in>A. f x z) z"
+  proof (subst zorder_mult)
+    have "\<forall>\<^sub>F z in at z. f a z \<noteq> 0"
+      using insert.prems(2) by eventually_elim (use insert.hyps in auto)
+    thus "\<exists>\<^sub>F z in at z. f a z \<noteq> 0"
+      using eventually_frequently at_neq_bot by blast
+  next
+    have "\<forall>\<^sub>F z in at z. (\<Prod>x\<in>A. f x z) \<noteq> 0"
+      using insert.prems(2) by eventually_elim (use insert.hyps in auto)
+    thus "\<exists>\<^sub>F z in at z. (\<Prod>x\<in>A. f x z) \<noteq> 0"
+      using eventually_frequently at_neq_bot by blast
+  qed (use insert.prems in \<open>auto intro!: meromorphic_intros\<close>)
+  also have "zorder (\<lambda>z. \<Prod>x\<in>A. f x z) z = (\<Sum>x\<in>A. zorder (f x) z)"
+    by (intro insert.IH) (use insert.prems insert.hyps in \<open>auto elim!: eventually_mono\<close>)
+  also have "zorder (f a) z + \<dots> = (\<Sum>x\<in>insert a A. zorder (f x) z)"
+    using insert.hyps by simp
+  finally show ?case .
+qed auto
+
+lemma zorder_scale:
+  assumes "f meromorphic_on {a * z}" "a \<noteq> 0"
+  shows "zorder (\<lambda>w. f (a * w)) z = zorder f (a * z)"
+proof (cases "eventually (\<lambda>z. f z = 0) (at (a * z))")
+  case True
+  hence ev: "eventually (\<lambda>z. f (a * z) = 0) (at z)"
+  proof (rule eventually_compose_filterlim)
+    show "filterlim ((*) a) (at (a * z)) (at z)"
+    proof (rule filterlim_atI)
+      show "\<forall>\<^sub>F x in at z. a * x \<noteq> a * z"
+        using eventually_neq_at_within[of z z] by eventually_elim (use \<open>a \<noteq> 0\<close> in auto)
+    qed (auto intro!: tendsto_intros)
+  qed
+
+  have "zorder (\<lambda>w. f (a * w)) z = zorder (\<lambda>_. 0) z"
+    by (rule zorder_cong) (use ev in auto)
+  also have "\<dots> = zorder (\<lambda>_. 0) (a * z)"
+    by (simp add: zorder_shift')
+  also have "\<dots> = zorder f (a * z)"
+    by (rule zorder_cong) (use True in auto)
+  finally show ?thesis .
+next
+  case False
+  define G where "G = fps_const a * fps_X"
+  have "zorder (f \<circ> (\<lambda>z. a * z)) z = zorder f (a * z) * int (subdegree G)"
+  proof (rule zorder_compose)
+    show "isolated_singularity_at f (a * z)" "not_essential f (a * z)"
+      using assms(1) by (auto simp: meromorphic_on_altdef)
+  next
+    have "(\<lambda>x. a * x) has_fps_expansion G"
+      unfolding G_def by (intro fps_expansion_intros)
+    thus "(\<lambda>x. a * (z + x) - a * z) has_fps_expansion G"
+      by (simp add: algebra_simps)
+  next
+    show "\<forall>\<^sub>F w in at (a * z). f w \<noteq> 0" using False 
+      by (metis assms(1) has_laurent_expansion_isolated has_laurent_expansion_not_essential
+             meromorphic_on_def non_zero_neighbour not_eventually singletonI)
+  qed (use \<open>a \<noteq> 0\<close> in \<open>auto simp: G_def\<close>)
+  also have "subdegree G = 1"
+    using \<open>a \<noteq> 0\<close> by (simp add: G_def)
+  finally show ?thesis
+    by (simp add: o_def)
+qed
+
+lemma zorder_uminus:
+  assumes "f meromorphic_on {-z}"
+  shows "zorder (\<lambda>w. f (-w)) z = zorder f (-z)"
+  using assms zorder_scale[of f "-1" z] by simp
+
+lemma is_pole_deriv_iff:
+  assumes "f meromorphic_on {z}"
+  shows   "is_pole (deriv f) z \<longleftrightarrow> is_pole f z"
+proof -
+  from assms obtain F where F: "(\<lambda>w. f (z + w)) has_laurent_expansion F"
+    by (auto simp: meromorphic_on_def)
+  have "deriv (\<lambda>w. f (z + w)) has_laurent_expansion fls_deriv F"
+    using F by (rule has_laurent_expansion_deriv)
+  also have "deriv (\<lambda>w. f (z + w)) = (\<lambda>w. deriv f (z + w))"
+    by (simp add: deriv_shift_0' add_ac o_def fun_eq_iff)
+  finally have F': "(\<lambda>w. deriv f (z + w)) has_laurent_expansion fls_deriv F" .
+  have "is_pole (deriv f) z \<longleftrightarrow> fls_subdegree (fls_deriv F) < 0"
+    using is_pole_fls_subdegree_iff[OF F'] by simp
+  also have "\<dots> \<longleftrightarrow> fls_subdegree F < 0"
+    using fls_deriv_subdegree0 fls_subdegree_deriv linorder_less_linear by fastforce
+  also have "\<dots> \<longleftrightarrow> is_pole f z"
+    using F by (simp add: has_laurent_expansion_imp_is_pole_iff)
+  finally show ?thesis .
+qed
+
+lemma isolated_zero_remove_sings_iff [simp]:
+  assumes "isolated_singularity_at f z"
+  shows   "isolated_zero (remove_sings f) z \<longleftrightarrow> isolated_zero f z"
+proof -
+  have *: "(\<forall>\<^sub>F x in at z. remove_sings f x \<noteq> 0) \<longleftrightarrow> (\<forall>\<^sub>F x in at z. f x \<noteq> 0)"
+  proof
+    assume "(\<forall>\<^sub>F x in at z. f x \<noteq> 0)"
+    thus "(\<forall>\<^sub>F x in at z. remove_sings f x \<noteq> 0)"
+      using eventually_remove_sings_eq_at[OF assms]
+      by eventually_elim auto
+  next
+    assume "(\<forall>\<^sub>F x in at z. remove_sings f x \<noteq> 0)"
+    thus "(\<forall>\<^sub>F x in at z. f x \<noteq> 0)"
+      using eventually_remove_sings_eq_at[OF assms]
+      by eventually_elim auto
+  qed
+  show ?thesis
+    unfolding isolated_zero_def using assms * by simp
+qed
+
+lemma zorder_isolated_zero_pos:
+  assumes "isolated_zero f z" "f analytic_on {z}"
+  shows   "zorder f z > 0"
+proof (subst zorder_pos_iff' [OF assms(2)])
+  show "f z = 0"
+    using assms by (simp add: zero_isolated_zero_analytic)
+next
+  have "\<forall>\<^sub>F z in at z. f z \<noteq> 0"
+    using assms by (auto simp: isolated_zero_def)
+  thus "\<exists>\<^sub>F z in at z. f z \<noteq> 0"
+    by (simp add: eventually_frequently)
+qed
+
+lemma zorder_isolated_zero_pos':
+  assumes "isolated_zero f z" "isolated_singularity_at f z"
+  shows   "zorder f z > 0"
+proof -
+  from assms(1) have "f \<midarrow>z\<rightarrow> 0"
+    by (simp add: isolated_zero_def)
+  with assms(2) have "remove_sings f analytic_on {z}"
+    by (intro remove_sings_analytic_on)
+  hence "zorder (remove_sings f) z > 0"
+    using assms by (intro zorder_isolated_zero_pos) auto
+  thus ?thesis
+    using assms by simp
+qed
+
+lemma zero_isolated_zero_nicely_meromorphic:
+  assumes "isolated_zero f z" "f nicely_meromorphic_on {z}"
+  shows "f z = 0"
+proof -
+  have "\<not>is_pole f z"
+    using assms pole_is_not_zero by blast
+  with assms(2) have "f analytic_on {z}"
+    by (simp add: nicely_meromorphic_on_imp_analytic_at)
+  with zero_isolated_zero_analytic assms(1) show ?thesis
+    by blast
+qed
+
+lemma meromorphic_on_imp_not_zero_cosparse:
+  assumes "f meromorphic_on A"
+  shows   "eventually (\<lambda>z. \<not>isolated_zero f z) (cosparse A)"
+proof -
+  have "eventually (\<lambda>z. \<not>is_pole (\<lambda>z. inverse (f z)) z) (cosparse A)"
+    by (intro meromorphic_on_imp_not_pole_cosparse meromorphic_intros assms)
+  thus ?thesis
+    by (simp add: is_pole_inverse_iff)
+qed
+
+lemma nicely_meromorphic_on_inverse [meromorphic_intros]:
+  assumes "f nicely_meromorphic_on A"
+  shows   "(\<lambda>x. inverse (f x)) nicely_meromorphic_on A"
+  unfolding nicely_meromorphic_on_def
+proof (intro conjI ballI)
+  fix z assume z: "z \<in> A"
+  have "is_pole f z \<and> f z = 0 \<or> f \<midarrow>z\<rightarrow> f z"
+    using assms z by (auto simp: nicely_meromorphic_on_def)
+  thus "is_pole (\<lambda>x. inverse (f x)) z \<and> inverse (f z) = 0 \<or>
+        (\<lambda>x. inverse (f x)) \<midarrow>z\<rightarrow> inverse (f z)"
+  proof
+    assume "is_pole f z \<and> f z = 0"
+    hence "isolated_zero (\<lambda>z. inverse (f z)) z \<and> inverse (f z) = 0"
+      by (auto simp: isolated_zero_inverse_iff)
+    hence "(\<lambda>x. inverse (f x)) \<midarrow>z\<rightarrow> inverse (f z)"
+      by (simp add: isolated_zero_def)
+    thus ?thesis ..
+  next
+    assume lim: "f \<midarrow>z\<rightarrow> f z"
+    hence ana: "f analytic_on {z}"
+      using assms is_pole_def nicely_meromorphic_on_imp_analytic_at
+            not_tendsto_and_filterlim_at_infinity trivial_limit_at z by blast
+    show ?thesis
+    proof (cases "isolated_zero f z")
+      case True
+      with lim have "f z = 0"
+        using continuous_within zero_isolated_zero by blast
+      with True have "is_pole (\<lambda>z. inverse (f z)) z \<and> inverse (f z) = 0"
+        by (auto simp: is_pole_inverse_iff)
+      thus ?thesis ..
+    next
+      case False
+      hence "f z \<noteq> 0 \<or> (f z = 0 \<and> eventually (\<lambda>z. f z = 0) (at z))"
+        using non_isolated_zero_imp_eventually_zero[OF ana] by blast
+      thus ?thesis
+      proof (elim disjE conjE)
+        assume "f z \<noteq> 0"
+        hence "(\<lambda>z. inverse (f z)) \<midarrow>z\<rightarrow> inverse (f z)"
+          by (intro tendsto_intros lim)
+        thus ?thesis ..
+      next
+        assume *: "f z = 0" "eventually (\<lambda>z. f z = 0) (at z)"
+        have "eventually (\<lambda>z. inverse (f z) = 0) (at z)"
+          using *(2) by eventually_elim auto
+        hence "(\<lambda>z. inverse (f z)) \<midarrow>z\<rightarrow> 0"
+          by (simp add: tendsto_eventually)
+        with *(1) show ?thesis
+          by auto
+      qed
+    qed
+  qed
+qed (use assms in \<open>auto simp: nicely_meromorphic_on_def intro!: meromorphic_intros\<close>)
+
+lemma is_pole_zero_at_nicely_mero:
+  assumes "f nicely_meromorphic_on A" "is_pole f z" "z \<in> A"
+  shows "f z = 0"
+  by (meson assms at_neq_bot 
+      is_pole_def nicely_meromorphic_on_def 
+      not_tendsto_and_filterlim_at_infinity)
+
+lemma zero_or_pole:
+  assumes mero: "f nicely_meromorphic_on A" 
+    and "z \<in> A" "f z = 0" and event: "\<forall>\<^sub>F x in at z. f x \<noteq> 0"
+  shows "isolated_zero f z \<or> is_pole f z"
+proof -
+  from mero \<open>z\<in>A\<close>
+  have "(is_pole f z \<and> f z=0) \<or> f \<midarrow>z\<rightarrow> f z"
+    unfolding nicely_meromorphic_on_def by simp
+  moreover have "isolated_zero f z" if "f \<midarrow>z\<rightarrow> f z" 
+    unfolding isolated_zero_def
+    using \<open>f z=0\<close> that event tendsto_nhds_iff by auto
+  ultimately show ?thesis by auto
+qed
+
+lemma isolated_zero_fls_subdegree_iff:
+  assumes "(\<lambda>x. f (z + x)) has_laurent_expansion F"
+  shows "isolated_zero f z \<longleftrightarrow> fls_subdegree F > 0"
+  using assms unfolding isolated_zero_def
+  by (metis Lim_at_zero fls_zero_subdegree has_laurent_expansion_eventually_nonzero_iff not_le
+        order.refl tendsto_0_subdegree_iff_0)
+
+lemma zorder_pos_imp_isolated_zero:
+  assumes "f meromorphic_on {z}" "eventually (\<lambda>z. f z \<noteq> 0) (at z)" "zorder f z > 0"
+  shows   "isolated_zero f z"
+  using assms isolated_zero_fls_subdegree_iff
+  by (metis has_laurent_expansion_eventually_nonzero_iff
+      has_laurent_expansion_zorder insertI1
+      meromorphic_on_def)
+
+lemma zorder_neg_imp_is_pole:
+  assumes "f meromorphic_on {z}" "eventually (\<lambda>z. f z \<noteq> 0) (at z)" "zorder f z < 0"
+  shows   "is_pole f z"
+  using assms is_pole_fls_subdegree_iff at_neq_bot eventually_frequently meromorphic_at_iff
+        neg_zorder_imp_is_pole by blast
+
+lemma not_pole_not_isolated_zero_imp_zorder_eq_0:
+  assumes "f meromorphic_on {z}" "\<not>is_pole f z" "\<not>isolated_zero f z" "frequently (\<lambda>z. f z \<noteq> 0) (at z)"
+  shows   "zorder f z = 0"
+proof -
+  have "remove_sings f analytic_on {z}"
+    using assms meromorphic_at_iff not_essential_def remove_sings_analytic_on by blast
+  moreover from this and assms have "remove_sings f z \<noteq> 0"
+    using isolated_zero_def meromorphic_at_iff non_zero_neighbour remove_sings_eq_0_iff by blast
+  moreover have "frequently (\<lambda>z. remove_sings f z \<noteq> 0) (at z)"
+    using assms analytic_at_neq_imp_eventually_neq calculation(1,2)
+      eventually_frequently trivial_limit_at by blast
+  ultimately have "zorder (remove_sings f) z = 0"
+    using zorder_eq_0_iff by blast
+  thus ?thesis
+    using assms(1) meromorphic_at_iff by auto
+qed
+
+lemma not_essential_compose:
+  assumes "not_essential f (g z)" "g analytic_on {z}"
+  shows   "not_essential (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+  case False
+  hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+    by (intro non_isolated_zero_imp_eventually_zero' analytic_intros assms) auto
+  hence "not_essential (\<lambda>x. f (g x)) z \<longleftrightarrow> not_essential (\<lambda>_. f (g z)) z"
+    by (intro not_essential_cong refl)
+       (auto elim!: eventually_mono simp: eventually_at_filter)
+  thus ?thesis
+    by (simp add: not_essential_const)
+next
+  case True
+  hence ev: "eventually (\<lambda>w. g w \<noteq> g z) (at z)"
+    by (auto simp: isolated_zero_def)
+  from assms consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+    by (auto simp: not_essential_def)  
+  have "isCont g z"
+    by (rule analytic_at_imp_isCont) fact
+  hence lim: "g \<midarrow>z\<rightarrow> g z"
+    using isContD by blast
+
+  from assms(1) consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+    unfolding not_essential_def by blast
+  thus ?thesis
+  proof cases
+    fix c assume "f \<midarrow>g z\<rightarrow> c"
+    hence "(\<lambda>x. f (g x)) \<midarrow>z\<rightarrow> c"
+      by (rule filterlim_compose) (use lim ev in \<open>auto simp: filterlim_at\<close>)
+    thus ?thesis
+      by (auto simp: not_essential_def)
+  next
+    assume "is_pole f (g z)"
+    hence "is_pole (\<lambda>x. f (g x)) z"
+      by (rule is_pole_compose) fact+
+    thus ?thesis
+      by (auto simp: not_essential_def)
+  qed
+qed
+
+
+lemma isolated_singularity_at_compose:
+  assumes "isolated_singularity_at f (g z)" "g analytic_on {z}"
+  shows   "isolated_singularity_at (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+  case False
+  hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+    by (intro non_isolated_zero_imp_eventually_zero') (use assms in \<open>auto intro!: analytic_intros\<close>)
+  hence "isolated_singularity_at (\<lambda>x. f (g x)) z \<longleftrightarrow> isolated_singularity_at (\<lambda>_. f (g z)) z"
+    by (intro isolated_singularity_at_cong refl)
+       (auto elim!: eventually_mono simp: eventually_at_filter)
+  thus ?thesis
+    by (simp add: isolated_singularity_at_const)
+next
+  case True
+  from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}"
+    by (auto simp: isolated_singularity_at_def)
+  hence holo_f: "f holomorphic_on ball (g z) r - {g z}"
+    by (subst (asm) analytic_on_open) auto
+  from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'"
+    by (auto simp: analytic_on_def)
+
+  have "continuous_on (ball z r') g"
+    using holomorphic_on_imp_continuous_on r' by blast
+  hence "isCont g z"
+    using r' by (subst (asm) continuous_on_eq_continuous_at) auto
+  hence "g \<midarrow>z\<rightarrow> g z"
+    using isContD by blast
+  hence "eventually (\<lambda>w. g w \<in> ball (g z) r) (at z)"
+    using \<open>r > 0\<close> unfolding tendsto_def by force
+  moreover have "eventually (\<lambda>w. g w \<noteq> g z) (at z)" using True
+    by (auto simp: isolated_zero_def elim!: eventually_mono)
+  ultimately have "eventually (\<lambda>w. g w \<in> ball (g z) r - {g z}) (at z)"
+    by eventually_elim auto
+  then obtain r'' where r'': "r'' > 0" "\<forall>w\<in>ball z r''-{z}. g w \<in> ball (g z) r - {g z}"
+    unfolding eventually_at_filter eventually_nhds_metric ball_def
+    by (auto simp: dist_commute)
+  have "f \<circ> g holomorphic_on ball z (min r' r'') - {z}"
+  proof (rule holomorphic_on_compose_gen)
+    show "g holomorphic_on ball z (min r' r'') - {z}"
+      by (rule holomorphic_on_subset[OF r'(2)]) auto
+    show "f holomorphic_on ball (g z) r - {g z}"
+      by fact
+    show "g ` (ball z (min r' r'') - {z}) \<subseteq> ball (g z) r - {g z}"
+      using r'' by force
+  qed
+  hence "f \<circ> g analytic_on ball z (min r' r'') - {z}"
+    by (subst analytic_on_open) auto
+  thus ?thesis using \<open>r' > 0\<close> \<open>r'' > 0\<close>
+    by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"])
+qed
+
+lemma is_pole_power_int_0:
+  assumes "f analytic_on {x}" "isolated_zero f x" "n < 0"
+  shows   "is_pole (\<lambda>x. f x powi n) x"
+proof -
+  have "f \<midarrow>x\<rightarrow> f x"
+    using assms(1) by (simp add: analytic_at_imp_isCont isContD)
+  with assms show ?thesis
+    unfolding is_pole_def
+    by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_imp_not_constant_on:
+  fixes f :: "'a :: perfect_space \<Rightarrow> 'b :: real_normed_div_algebra"
+  assumes "isolated_zero f x" "x \<in> A" "open A"
+  shows   "\<not>f constant_on A"
+proof
+  assume "f constant_on A"
+  then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+    by (auto simp: constant_on_def)
+  have "eventually (\<lambda>z. z \<in> A - {x}) (at x)"
+    by (intro eventually_at_in_open assms)
+  hence "eventually (\<lambda>z. f z = c) (at x)"
+    by eventually_elim (use c in auto)
+  hence "f \<midarrow>x\<rightarrow> c"
+    using tendsto_eventually by blast
+  moreover from assms have "f \<midarrow>x\<rightarrow> 0"
+    by (simp add: isolated_zero_def)
+  ultimately have [simp]: "c = 0"
+    using tendsto_unique[of "at x" f c 0] by (simp add: at_neq_bot)
+
+  have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+    using assms by (auto simp: isolated_zero_def)
+  moreover have "eventually (\<lambda>x. x \<in> A) (at x)"
+    using assms by (intro eventually_at_in_open') auto
+  ultimately have "eventually (\<lambda>x. False) (at x)"
+    by eventually_elim (use c in auto)
+  thus False
+    by simp
+qed
+
 end