# Theory Meromorphic

```theory Meromorphic
imports Laurent_Convergence Riemann_Mapping
begin

lemma analytic_at_cong:
assumes "eventually (λx. f x = g x) (nhds x)" "x = y"
shows "f analytic_on {x} ⟷ g analytic_on {y}"
proof -
have "g analytic_on {x}" if "f analytic_on {x}" "eventually (λx. f x = g x) (nhds x)" for f g
proof -
have "(λy. f (x + y)) has_fps_expansion fps_expansion f x"
by (rule analytic_at_imp_has_fps_expansion) fact
also have "?this ⟷ (λy. g (x + y)) has_fps_expansion fps_expansion f x"
using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap)
finally show ?thesis
by (rule has_fps_expansion_imp_analytic)
qed
from this[of f g] this[of g f] show ?thesis using assms
by (auto simp: eq_commute)
qed

definition remove_sings :: "(complex ⇒ complex) ⇒ complex ⇒ complex" where
"remove_sings f z = (if ∃c. f ─z→ c then Lim (at z) f else 0)"

lemma remove_sings_eqI [intro]:
assumes "f ─z→ c"
shows   "remove_sings f z = c"
using assms unfolding remove_sings_def by (auto simp: tendsto_Lim)

lemma remove_sings_at_analytic [simp]:
assumes "f analytic_on {z}"
shows   "remove_sings f z = f z"
using assms by (intro remove_sings_eqI) (simp add: analytic_at_imp_isCont isContD)

lemma remove_sings_at_pole [simp]:
assumes "is_pole f z"
shows   "remove_sings f z = 0"
using assms unfolding remove_sings_def is_pole_def
by (meson at_neq_bot not_tendsto_and_filterlim_at_infinity)

lemma eventually_remove_sings_eq_at:
assumes "isolated_singularity_at f z"
shows   "eventually (λw. remove_sings f w = f w) (at z)"
proof -
from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
by (auto simp: isolated_singularity_at_def)
hence *: "f analytic_on {w}" if "w ∈ ball z r - {z}" for w
using r that by (auto intro: analytic_on_subset)
have "eventually (λw. w ∈ ball z r - {z}) (at z)"
using r by (intro eventually_at_in_open) auto
thus ?thesis
by eventually_elim (auto simp: remove_sings_at_analytic *)
qed

lemma eventually_remove_sings_eq_nhds:
assumes "f analytic_on {z}"
shows   "eventually (λw. remove_sings f w = f w) (nhds z)"
proof -
from assms obtain A where A: "open A" "z ∈ A" "f holomorphic_on A"
by (auto simp: analytic_at)
have "eventually (λz. z ∈ A) (nhds z)"
by (intro eventually_nhds_in_open A)
thus ?thesis
proof eventually_elim
case (elim w)
from elim have "f analytic_on {w}"
using A analytic_at by blast
thus ?case by auto
qed
qed

lemma remove_sings_compose:
assumes "filtermap g (at z) = at z'"
shows   "remove_sings (f ∘ g) z = remove_sings f z'"
proof (cases "∃c. f ─z'→ c")
case True
then obtain c where c: "f ─z'→ c"
by auto
from c have "remove_sings f z' = c"
by blast
moreover from c have "remove_sings (f ∘ g) z = c"
using c by (intro remove_sings_eqI) (auto simp: filterlim_def filtermap_compose assms)
ultimately show ?thesis
by simp
next
case False
hence "¬(∃c. (f ∘ g) ─z→ c)"
by (auto simp: filterlim_def filtermap_compose assms)
with False show ?thesis
by (auto simp: remove_sings_def)
qed

lemma remove_sings_cong:
assumes "eventually (λx. f x = g x) (at z)" "z = z'"
shows   "remove_sings f z = remove_sings g z'"
proof (cases "∃c. f ─z→ c")
case True
then obtain c where c: "f ─z→ c" by blast
hence "remove_sings f z = c"
by blast
moreover have "f ─z→ c ⟷ g ─z'→ c"
using assms by (intro filterlim_cong refl) auto
with c have "remove_sings g z' = c"
by (intro remove_sings_eqI) auto
ultimately show ?thesis
by simp
next
case False
have "f ─z→ c ⟷ g ─z'→ c" for c
using assms by (intro filterlim_cong) auto
with False show ?thesis
by (auto simp: remove_sings_def)
qed

lemma deriv_remove_sings_at_analytic [simp]:
assumes "f analytic_on {z}"
shows   "deriv (remove_sings f) z = deriv f z"
apply (rule deriv_cong_ev)
apply (rule eventually_remove_sings_eq_nhds)
using assms by auto

lemma isolated_singularity_at_remove_sings [simp, intro]:
assumes "isolated_singularity_at f z"
shows   "isolated_singularity_at (remove_sings f) z"
using isolated_singularity_at_cong[OF eventually_remove_sings_eq_at[OF assms] refl] assms
by simp

lemma not_essential_remove_sings_iff [simp]:
assumes "isolated_singularity_at f z"
shows   "not_essential (remove_sings f) z ⟷ not_essential f z"
using not_essential_cong[OF eventually_remove_sings_eq_at[OF assms(1)] refl]
by simp

lemma not_essential_remove_sings [intro]:
assumes "isolated_singularity_at f z" "not_essential f z"
shows   "not_essential (remove_sings f) z"
by (subst not_essential_remove_sings_iff) (use assms in auto)

lemma
assumes "isolated_singularity_at f z"
shows is_pole_remove_sings_iff [simp]:
"is_pole (remove_sings f) z ⟷ is_pole f z"
and zorder_remove_sings [simp]:
"zorder (remove_sings f) z = zorder f z"
and zor_poly_remove_sings [simp]:
"zor_poly (remove_sings f) z = zor_poly f z"
and has_laurent_expansion_remove_sings_iff [simp]:
"(λw. remove_sings f (z + w)) has_laurent_expansion F ⟷
(λw. f (z + w)) has_laurent_expansion F"
and tendsto_remove_sings_iff [simp]:
"remove_sings f ─z→ c ⟷ f ─z→ c"
by (intro is_pole_cong eventually_remove_sings_eq_at refl zorder_cong
zor_poly_cong has_laurent_expansion_cong' tendsto_cong assms)+

lemma get_all_poles_from_remove_sings:
fixes f:: "complex ⇒ complex"
defines "ff≡remove_sings f"
assumes f_holo:"f holomorphic_on s - pts" and "finite pts"
"pts⊆s" "open s" and not_ess:"∀x∈pts. not_essential f x"
obtains pts' where
"pts' ⊆ pts" "finite pts'" "ff holomorphic_on s - pts'" "∀x∈pts'. is_pole ff x"
proof -
define pts' where "pts' = {x∈pts. is_pole f x}"

have "pts' ⊆ pts" unfolding pts'_def by auto
then have "finite pts'" using ‹finite pts›
using rev_finite_subset by blast
then have "open (s - pts')" using ‹open s›

have isolated:"isolated_singularity_at f z" if "z∈pts" for z
proof (rule isolated_singularity_at_holomorphic)
show "f holomorphic_on (s-(pts-{z})) - {z}"
by (metis Diff_insert f_holo insert_Diff that)
show " open (s - (pts - {z}))"
by (meson assms(3) assms(5) finite_Diff finite_imp_closed open_Diff)
show "z ∈ s - (pts - {z})"
using assms(4) that by auto
qed

have "ff holomorphic_on s - pts'"
proof (rule no_isolated_singularity')
show "(ff ⤏ ff z) (at z within s - pts')" if "z ∈ pts-pts'" for z
proof -
have "at z within s - pts' = at z"
apply (rule at_within_open)
using ‹open (s - pts')› that ‹pts⊆s›  by auto
moreover have "ff ─z→ ff z"
unfolding ff_def
proof (subst tendsto_remove_sings_iff)
show "isolated_singularity_at f z"
apply (rule isolated)
using that by auto
have "not_essential f z"
using not_ess that by auto
moreover have "¬is_pole f z"
using that unfolding pts'_def by auto
ultimately have "∃c. f ─z→ c"
unfolding not_essential_def by auto
then show "f ─z→ remove_sings f z"
using remove_sings_eqI by blast
qed
ultimately show ?thesis by auto
qed
have "ff holomorphic_on s - pts"
using f_holo
proof (elim holomorphic_transform)
fix x assume "x ∈ s - pts"
then have "f analytic_on {x}"
using assms(3) assms(5) f_holo
by (meson finite_imp_closed
holomorphic_on_imp_analytic_at open_Diff)
from remove_sings_at_analytic[OF this]
show "f x = ff x" unfolding ff_def by auto
qed
then show "ff holomorphic_on s - pts' - (pts - pts')"
apply (elim holomorphic_on_subset)
by blast
show "open (s - pts')"
by (simp add: ‹open (s - pts')›)
show "finite (pts - pts')"
qed
moreover have "∀x∈pts'. is_pole ff x"
unfolding pts'_def
using ff_def is_pole_remove_sings_iff isolated by blast
moreover note ‹pts' ⊆ pts› ‹finite pts'›
ultimately show ?thesis using that by auto
qed

lemma remove_sings_eq_0_iff:
assumes "not_essential f w"
shows "remove_sings f w = 0 ⟷ is_pole f w ∨ f ─w→ 0"
proof (cases "is_pole f w")
case True
then show ?thesis by simp
next
case False
then obtain c where c:"f ─w→ c"
using ‹not_essential f w› unfolding not_essential_def by auto
then show ?thesis
using False remove_sings_eqI by auto
qed

definition meromorphic_on:: "[complex ⇒ complex, complex set, complex set] ⇒ bool"
("_ (meromorphic'_on) _ _" [50,50,50]50) where
"f meromorphic_on D pts ≡
open D ∧ pts ⊆ D ∧ (∀z∈pts. isolated_singularity_at f z ∧ not_essential f z) ∧
(∀z∈D. ¬(z islimpt pts)) ∧ (f holomorphic_on D-pts)"

lemma meromorphic_imp_holomorphic: "f meromorphic_on D pts ⟹ f holomorphic_on (D - pts)"
unfolding meromorphic_on_def by auto

lemma meromorphic_imp_closedin_pts:
assumes "f meromorphic_on D pts"
shows "closedin (top_of_set D) pts"
by (meson assms closedin_limpt meromorphic_on_def)

lemma meromorphic_imp_open_diff':
assumes "f meromorphic_on D pts" "pts' ⊆ pts"
shows "open (D - pts')"
proof -
have "D - pts' = D - closure pts'"
proof safe
fix x assume x: "x ∈ D" "x ∈ closure pts'" "x ∉ pts'"
hence "x islimpt pts'"
by (subst islimpt_in_closure) auto
hence "x islimpt pts"
by (rule islimpt_subset) fact
with assms x show False
by (auto simp: meromorphic_on_def)
qed (use closure_subset in auto)
then show ?thesis
using assms meromorphic_on_def by auto
qed

lemma meromorphic_imp_open_diff: "f meromorphic_on D pts ⟹ open (D - pts)"
by (erule meromorphic_imp_open_diff') auto

lemma meromorphic_pole_subset:
assumes merf: "f meromorphic_on D pts"
shows "{x∈D. is_pole f x} ⊆ pts"
by (smt (verit) Diff_iff assms mem_Collect_eq meromorphic_imp_open_diff
meromorphic_on_def not_is_pole_holomorphic subsetI)

named_theorems meromorphic_intros

lemma meromorphic_on_subset:
assumes "f meromorphic_on A pts" "open B" "B ⊆ A" "pts' = pts ∩ B"
shows   "f meromorphic_on B pts'"
unfolding meromorphic_on_def
proof (intro ballI conjI)
fix z assume "z ∈ B"
show "¬z islimpt pts'"
proof
assume "z islimpt pts'"
hence "z islimpt pts"
by (rule islimpt_subset) (use ‹pts' = _› in auto)
thus False using ‹z ∈ B› ‹B ⊆ A› assms(1)
by (auto simp: meromorphic_on_def)
qed
qed (use assms in ‹auto simp: meromorphic_on_def›)

lemma meromorphic_on_superset_pts:
assumes "f meromorphic_on A pts" "pts ⊆ pts'" "pts' ⊆ A" "∀x∈A. ¬x islimpt pts'"
shows   "f meromorphic_on A pts'"
unfolding meromorphic_on_def
proof (intro conjI ballI impI)
fix z assume "z ∈ pts'"
from assms(1) have holo: "f holomorphic_on A - pts" and "open A"
unfolding meromorphic_on_def by blast+
have "open (A - pts)"
by (intro meromorphic_imp_open_diff[OF assms(1)])

show "isolated_singularity_at f z"
proof (cases "z ∈ pts")
case False
thus ?thesis
using ‹open (A - pts)› assms ‹z ∈ pts'›
by (intro isolated_singularity_at_holomorphic[of _ "A - pts"] holomorphic_on_subset[OF holo])
auto
qed (use assms in ‹auto simp: meromorphic_on_def›)

show "not_essential f z"
proof (cases "z ∈ pts")
case False
thus ?thesis
using ‹open (A - pts)› assms ‹z ∈ pts'›
by (intro not_essential_holomorphic[of _ "A - pts"] holomorphic_on_subset[OF holo])
auto
qed (use assms in ‹auto simp: meromorphic_on_def›)
qed (use assms in ‹auto simp: meromorphic_on_def›)

lemma meromorphic_on_no_singularities: "f meromorphic_on A {} ⟷ f holomorphic_on A ∧ open A"
by (auto simp: meromorphic_on_def)

lemma holomorphic_on_imp_meromorphic_on:
"f holomorphic_on A ⟹ pts ⊆ A ⟹ open A ⟹ ∀x∈A. ¬x islimpt pts ⟹ f meromorphic_on A pts"
by (rule meromorphic_on_superset_pts[where pts = "{}"])
(auto simp: meromorphic_on_no_singularities)

lemma meromorphic_on_const [meromorphic_intros]:
assumes "open A" "∀x∈A. ¬x islimpt pts" "pts ⊆ A"
shows   "(λ_. c) meromorphic_on A pts"
by (rule holomorphic_on_imp_meromorphic_on) (use assms in auto)

lemma meromorphic_on_ident [meromorphic_intros]:
assumes "open A" "∀x∈A. ¬x islimpt pts" "pts ⊆ A"
shows   "(λx. x) meromorphic_on A pts"
by (rule holomorphic_on_imp_meromorphic_on) (use assms in auto)

lemma meromorphic_on_id [meromorphic_intros]:
assumes "open A" "∀x∈A. ¬x islimpt pts" "pts ⊆ A"
shows   "id meromorphic_on A pts"
using meromorphic_on_ident assms unfolding id_def .

assumes f_ness: "not_essential f z" and g_ness: "not_essential g z"
assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
shows "not_essential (λw. f w + g w) z"
proof -
have "(λw. f (z + w) + g (z + w)) has_laurent_expansion laurent_expansion f z + laurent_expansion g z"
by (intro not_essential_has_laurent_expansion laurent_expansion_intros assms)
hence "not_essential (λw. f (z + w) + g (z + w)) 0"
using has_laurent_expansion_not_essential_0 by blast
thus ?thesis
qed

lemma meromorphic_on_uminus [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λz. -f z) meromorphic_on A pts"
unfolding meromorphic_on_def
by (use assms in ‹auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros›)

assumes "f meromorphic_on A pts" "g meromorphic_on A pts"
shows   "(λz. f z + g z) meromorphic_on A pts"
unfolding meromorphic_on_def
by (use assms in ‹auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros›)

assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2"
shows   "(λz. f z + g z) meromorphic_on A (pts1 ∪ pts2)"
proof (rule meromorphic_intros)
show "f meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(1)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
show "g meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(2)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
qed

assumes "f meromorphic_on A pts"
shows   "(λz. f z + c) meromorphic_on A pts"
unfolding meromorphic_on_def
by (use assms in ‹auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros›)

lemma meromorphic_on_minus_const [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λz. f z - c) meromorphic_on A pts"
using meromorphic_on_add_const[OF assms,of "-c"] by simp

lemma meromorphic_on_diff [meromorphic_intros]:
assumes "f meromorphic_on A pts" "g meromorphic_on A pts"
shows   "(λz. f z - g z) meromorphic_on A pts"
using meromorphic_on_add[OF assms(1) meromorphic_on_uminus[OF assms(2)]] by simp

lemma meromorphic_on_diff':
assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2"
shows   "(λz. f z - g z) meromorphic_on A (pts1 ∪ pts2)"
proof (rule meromorphic_intros)
show "f meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(1)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
show "g meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(2)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
qed

lemma meromorphic_on_mult [meromorphic_intros]:
assumes "f meromorphic_on A pts" "g meromorphic_on A pts"
shows   "(λz. f z * g z) meromorphic_on A pts"
unfolding meromorphic_on_def
by (use assms in ‹auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros›)

lemma meromorphic_on_mult':
assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2"
shows   "(λz. f z * g z) meromorphic_on A (pts1 ∪ pts2)"
proof (rule meromorphic_intros)
show "f meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(1)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
show "g meromorphic_on A (pts1 ∪ pts2)"
by (rule meromorphic_on_superset_pts[OF assms(2)])
(use assms in ‹auto simp: meromorphic_on_def islimpt_Un›)
qed

lemma meromorphic_on_imp_not_essential:
assumes "f meromorphic_on A pts" "z ∈ A"
shows   "not_essential f z"
proof (cases "z ∈ pts")
case False
thus ?thesis
using not_essential_holomorphic[of f "A - pts" z] meromorphic_imp_open_diff[OF assms(1)] assms
by (auto simp: meromorphic_on_def)
qed (use assms in ‹auto simp: meromorphic_on_def›)

lemma meromorphic_imp_analytic: "f meromorphic_on D pts ⟹ f analytic_on (D - pts)"
unfolding meromorphic_on_def
apply (subst analytic_on_open)
using meromorphic_imp_open_diff meromorphic_on_id apply blast
apply auto
done

lemma not_islimpt_isolated_zeros:
assumes mero: "f meromorphic_on A pts" and "z ∈ A"
shows "¬z islimpt {w∈A. isolated_zero f w}"
proof
assume islimpt: "z islimpt {w∈A. isolated_zero f w}"
have holo: "f holomorphic_on A - pts" and "open A"
using assms by (auto simp: meromorphic_on_def)
have open': "open (A - (pts - {z}))"
by (intro meromorphic_imp_open_diff'[OF mero]) auto
then obtain r where r: "r > 0" "ball z r ⊆ A - (pts - {z})"
using meromorphic_imp_open_diff[OF mero] ‹z ∈ A› openE by blast

have "not_essential f z"
using assms by (rule meromorphic_on_imp_not_essential)
then consider c where "f ─z→ c" | "is_pole f z"
unfolding not_essential_def by blast
thus False
proof cases
assume "is_pole f z"
hence "eventually (λw. f w ≠ 0) (at z)"
by (rule non_zero_neighbour_pole)
hence "¬z islimpt {w. f w = 0}"
moreover have "z islimpt {w. f w = 0}"
using islimpt by (rule islimpt_subset) (auto simp: isolated_zero_def)
next
fix c assume c: "f ─z→ c"
define g where "g = (λw. if w = z then c else f w)"
have holo': "g holomorphic_on A - (pts - {z})" unfolding g_def
by (intro removable_singularity holomorphic_on_subset[OF holo] open' c) auto

have eq_zero: "g w = 0" if "w ∈ ball z r" for w
proof (rule analytic_continuation[where f = g])
show "open (ball z r)" "connected (ball z r)" "{w∈ball z r. isolated_zero f w} ⊆ ball z r"
by auto
have "z islimpt {w∈A. isolated_zero f w} ∩ ball z r"
using islimpt ‹r > 0› by (intro islimpt_Int_eventually eventually_at_in_open') auto
also have "… = {w∈ball z r. isolated_zero f w}"
using r by auto
finally show "z islimpt {w∈ball z r. isolated_zero f w}"
by simp
next
fix w assume w: "w ∈ {w∈ball z r. isolated_zero f w}"
show "g w = 0"
proof (cases "w = z")
case False
thus ?thesis using w by (auto simp: g_def isolated_zero_def)
next
case True
have "z islimpt {z. f z = 0}"
using islimpt by (rule islimpt_subset) (auto simp: isolated_zero_def)
thus ?thesis
using w by (simp add: isolated_zero_altdef True)
qed
qed (use r that in ‹auto intro!: holomorphic_on_subset[OF holo'] simp: isolated_zero_def›)

have "infinite ({w∈A. isolated_zero f w} ∩ ball z r)"
using islimpt ‹r > 0› unfolding islimpt_eq_infinite_ball by blast
hence "{w∈A. isolated_zero f w} ∩ ball z r ≠ {}"
by force
then obtain z0 where z0: "z0 ∈ A" "isolated_zero f z0" "z0 ∈ ball z r"
by blast
have "∀⇩F y in at z0. y ∈ ball z r - (if z = z0 then {} else {z}) - {z0}"
using r z0 by (intro eventually_at_in_open) auto
hence "eventually (λw. f w = 0) (at z0)"
proof eventually_elim
case (elim w)
show ?case
using eq_zero[of w] elim by (auto simp: g_def split: if_splits)
qed
hence "eventually (λw. f w = 0) (at z0)"
by (auto simp: g_def eventually_at_filter elim!: eventually_mono split: if_splits)
moreover from z0 have "eventually (λw. f w ≠ 0) (at z0)"
ultimately have "eventually (λ_. False) (at z0)"
by eventually_elim auto
thus False
by simp
qed
qed

lemma closedin_isolated_zeros:
assumes "f meromorphic_on A pts"
shows   "closedin (top_of_set A) {z∈A. isolated_zero f z}"
unfolding closedin_limpt using not_islimpt_isolated_zeros[OF assms] by auto

lemma meromorphic_on_deriv':
assumes "f meromorphic_on A pts" "open A"
assumes "⋀x. x ∈ A - pts ⟹ (f has_field_derivative f' x) (at x)"
shows   "f' meromorphic_on A pts"
unfolding meromorphic_on_def
proof (intro conjI ballI)
have "open (A - pts)"
by (intro meromorphic_imp_open_diff[OF assms(1)])
thus "f' holomorphic_on A - pts"
by (rule derivative_is_holomorphic) (use assms in auto)
next
fix z assume "z ∈ pts"
hence "z ∈ A"
using assms(1) by (auto simp: meromorphic_on_def)
from ‹z ∈ pts› obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
using assms(1) by (auto simp: meromorphic_on_def isolated_singularity_at_def)

have "open (ball z r ∩ (A - (pts - {z})))"
by (intro open_Int assms meromorphic_imp_open_diff'[OF assms(1)]) auto
then obtain r' where r': "r' > 0" "ball z r' ⊆ ball z r ∩ (A - (pts - {z}))"
using r ‹z ∈ A› by (subst (asm) open_contains_ball) fastforce

have "open (ball z r' - {z})"
by auto
hence "f' holomorphic_on ball z r' - {z}"
by (rule derivative_is_holomorphic[of _ f]) (use r' in ‹auto intro!: assms(3)›)
moreover have "open (ball z r' - {z})"
by auto
ultimately show "isolated_singularity_at f' z"
unfolding isolated_singularity_at_def using ‹r' > 0›
by (auto simp: analytic_on_open intro!: exI[of _ r'])
next
fix z assume z: "z ∈ pts"
hence z': "not_essential f z" "z ∈ A"
using assms by (auto simp: meromorphic_on_def)
from z'(1) show "not_essential f' z"
proof (rule not_essential_deriv')
show "z ∈ A - (pts - {z})"
using ‹z ∈ A› by blast
show "open (A - (pts - {z}))"
by (intro meromorphic_imp_open_diff'[OF assms(1)]) auto
qed (use assms in auto)
qed (use assms in ‹auto simp: meromorphic_on_def›)

lemma meromorphic_on_deriv [meromorphic_intros]:
assumes "f meromorphic_on A pts" "open A"
shows   "deriv f meromorphic_on A pts"
proof (intro meromorphic_on_deriv'[OF assms(1)])
have *: "open (A - pts)"
by (intro meromorphic_imp_open_diff[OF assms(1)])
show "(f has_field_derivative deriv f x) (at x)" if "x ∈ A - pts" for x
using assms(1) by (intro holomorphic_derivI[OF _ * that]) (auto simp: meromorphic_on_def)
qed fact

lemma meromorphic_on_imp_analytic_at:
assumes "f meromorphic_on A pts" "z ∈ A - pts"
shows   "f analytic_on {z}"
using assms by (metis analytic_at meromorphic_imp_open_diff meromorphic_on_def)

lemma meromorphic_compact_finite_pts:
assumes "f meromorphic_on D pts" "compact S" "S ⊆ D"
shows "finite (S ∩ pts)"
proof -
{ assume "infinite (S ∩ pts)"
then obtain z where "z ∈ S" and z: "z islimpt (S ∩ pts)"
using assms by (metis compact_eq_Bolzano_Weierstrass inf_le1)
then have False
using assms by (meson in_mono inf_le2 islimpt_subset meromorphic_on_def) }
then show ?thesis by metis
qed

lemma meromorphic_imp_countable:
assumes "f meromorphic_on D pts"
shows "countable pts"
proof -
obtain K :: "nat ⇒ complex set" where K: "D = (⋃n. K n)" "⋀n. compact (K n)"
using assms unfolding meromorphic_on_def by (metis open_Union_compact_subsets)
then have "pts = (⋃n. K n ∩ pts)"
using assms meromorphic_on_def by auto
moreover have "⋀n. finite (K n ∩ pts)"
by (metis K(1) K(2) UN_I assms image_iff meromorphic_compact_finite_pts rangeI subset_eq)
ultimately show ?thesis
by (metis countableI_type countable_UN countable_finite)
qed

lemma meromorphic_imp_connected_diff':
assumes "f meromorphic_on D pts" "connected D" "pts' ⊆ pts"
shows "connected (D - pts')"
proof (rule connected_open_diff_countable)
show "countable pts'"
by (rule countable_subset [OF assms(3)]) (use assms(1) in ‹auto simp: meromorphic_imp_countable›)
qed (use assms in ‹auto simp: meromorphic_on_def›)

lemma meromorphic_imp_connected_diff:
assumes "f meromorphic_on D pts" "connected D"
shows "connected (D - pts)"
using meromorphic_imp_connected_diff'[OF assms order.refl] .

lemma meromorphic_on_compose [meromorphic_intros]:
assumes f: "f meromorphic_on A pts" and g: "g holomorphic_on B"
assumes "open B" and "g ` B ⊆ A"
shows   "(λx. f (g x)) meromorphic_on B (isolated_points_of (g -` pts ∩ B))"
unfolding meromorphic_on_def
proof (intro ballI conjI)
fix z assume z: "z ∈ isolated_points_of (g -` pts ∩ B)"
hence z': "z ∈ B" "g z ∈ pts"
using isolated_points_of_subset by blast+
have g': "g analytic_on {z}"
using g z' ‹open B› analytic_at by blast

show "isolated_singularity_at (λx. f (g x)) z"
by (rule isolated_singularity_at_compose[OF _ g']) (use f z' in ‹auto simp: meromorphic_on_def›)
show "not_essential (λx. f (g x)) z"
by (rule not_essential_compose[OF _ g']) (use f z' in ‹auto simp: meromorphic_on_def›)
next
fix z assume z: "z ∈ B"
hence "g z ∈ A"
using assms by auto
hence "¬g z islimpt pts"
using f by (auto simp: meromorphic_on_def)
hence ev: "eventually (λw. w ∉ pts) (at (g z))"
by (auto simp: islimpt_conv_frequently_at frequently_def)
have g': "g analytic_on {z}"
by (rule holomorphic_on_imp_analytic_at[OF g]) (use assms z in auto)

(* TODO: There's probably a useful lemma somewhere in here to extract... *)
have "eventually (λw. w ∉ isolated_points_of (g -` pts ∩ B)) (at z)"
proof (cases "isolated_zero (λw. g w - g z) z")
case True
have "eventually (λw. w ∉ pts) (at (g z))"
using ev by (auto simp: islimpt_conv_frequently_at frequently_def)
moreover have "g ─z→ g z"
using analytic_at_imp_isCont[OF g'] isContD by blast
hence lim: "filterlim g (at (g z)) (at z)"
using True by (auto simp: filterlim_at isolated_zero_def)
have "eventually (λw. g w ∉ pts) (at z)"
using ev lim by (rule eventually_compose_filterlim)
thus ?thesis
by eventually_elim (auto simp: isolated_points_of_def)
next
case False
have "eventually (λw. g w - g z = 0) (nhds z)"
using False by (rule non_isolated_zero) (auto intro!: analytic_intros g')
hence "eventually (λw. g w = g z ∧ w ∈ B) (nhds z)"
using eventually_nhds_in_open[OF ‹open B› ‹z ∈ B›]
by eventually_elim auto
then obtain X where X: "open X" "z ∈ X" "X ⊆ B" "∀x∈X. g x = g z"
unfolding eventually_nhds by blast

have "z0 ∉ isolated_points_of (g -` pts ∩ B)" if "z0 ∈ X" for z0
proof (cases "g z ∈ pts")
case False
with that have "g z0 ∉ pts"
using X by metis
thus ?thesis
by (auto simp: isolated_points_of_def)
next
case True
have "eventually (λw. w ∈ X) (at z0)"
by (intro eventually_at_in_open') fact+
hence "eventually (λw. w ∈ g -` pts ∩ B) (at z0)"
by eventually_elim (use X True in fastforce)
hence "frequently (λw. w ∈ g -` pts ∩ B) (at z0)"
by (meson at_neq_bot eventually_frequently)
thus "z0 ∉ isolated_points_of (g -` pts ∩ B)"
unfolding isolated_points_of_def by (auto simp: frequently_def)
qed
moreover have "eventually (λx. x ∈ X) (at z)"
by (intro eventually_at_in_open') fact+
ultimately show ?thesis
by (auto elim!: eventually_mono)
qed
thus "¬z islimpt isolated_points_of (g -` pts ∩ B)"
by (auto simp: islimpt_conv_frequently_at frequently_def)
next
have "f ∘ g analytic_on (⋃z∈B - isolated_points_of (g -` pts ∩ B). {z})"
unfolding analytic_on_UN
proof
fix z assume z: "z ∈ B - isolated_points_of (g -` pts ∩ B)"
hence "z ∈ B" by blast
have g': "g analytic_on {z}"
by (rule holomorphic_on_imp_analytic_at[OF g]) (use assms z in auto)
show "f ∘ g analytic_on {z}"
proof (cases "g z ∈ pts")
case False
show ?thesis
proof (rule analytic_on_compose)
show "f analytic_on g ` {z}" using False z assms
by (auto intro!: meromorphic_on_imp_analytic_at[OF f])
qed fact
next
case True
show ?thesis
proof (cases "isolated_zero (λw. g w - g z) z")
case False
hence "eventually (λw. g w - g z = 0) (nhds z)"
by (rule non_isolated_zero) (auto intro!: analytic_intros g')
hence "f ∘ g analytic_on {z} ⟷ (λ_. f (g z)) analytic_on {z}"
by (intro analytic_at_cong) (auto elim!: eventually_mono)
thus ?thesis
by simp
next
case True
hence ev: "eventually (λw. g w ≠ g z) (at z)"
by (auto simp: isolated_zero_def)

have "¬g z islimpt pts"
using ‹g z ∈ pts› f by (auto simp: meromorphic_on_def)
hence "eventually (λw. w ∉ pts) (at (g z))"
by (auto simp: islimpt_conv_frequently_at frequently_def)
moreover have "g ─z→ g z"
using analytic_at_imp_isCont[OF g'] isContD by blast
with ev have "filterlim g (at (g z)) (at z)"
by (auto simp: filterlim_at)
ultimately have "eventually (λw. g w ∉ pts) (at z)"
using eventually_compose_filterlim by blast
hence "z ∈ isolated_points_of (g -` pts ∩ B)"
using ‹g z ∈ pts› ‹z ∈ B›
by (auto simp: isolated_points_of_def elim!: eventually_mono)
with z show ?thesis by simp
qed
qed
qed
also have "… = B - isolated_points_of (g -` pts ∩ B)"
by blast
finally show "(λx. f (g x)) holomorphic_on B - isolated_points_of (g -` pts ∩ B)"
unfolding o_def using analytic_imp_holomorphic by blast
qed (auto simp: isolated_points_of_def ‹open B›)

lemma meromorphic_on_compose':
assumes f: "f meromorphic_on A pts" and g: "g holomorphic_on B"
assumes "open B" and "g ` B ⊆ A" and "pts' = (isolated_points_of (g -` pts ∩ B))"
shows   "(λx. f (g x)) meromorphic_on B pts'"
using meromorphic_on_compose[OF assms(1-4)] assms(5) by simp

lemma meromorphic_on_inverse': "inverse meromorphic_on UNIV 0"
unfolding meromorphic_on_def
by (auto intro!: holomorphic_intros singularity_intros not_essential_inverse
isolated_singularity_at_inverse simp: islimpt_finite)

lemma meromorphic_on_inverse [meromorphic_intros]:
assumes mero: "f meromorphic_on A pts"
shows   "(λz. inverse (f z)) meromorphic_on A (pts ∪ {z∈A. isolated_zero f z})"
proof -
have "open A"
using mero by (auto simp: meromorphic_on_def)
have open': "open (A - pts)"
by (intro meromorphic_imp_open_diff[OF mero])
have holo: "f holomorphic_on A - pts"
using assms by (auto simp: meromorphic_on_def)
have ana: "f analytic_on A - pts"
using open' holo by (simp add: analytic_on_open)

show ?thesis
unfolding meromorphic_on_def
proof (intro conjI ballI)
fix z assume z: "z ∈ pts ∪ {z∈A. isolated_zero f z}"
have "isolated_singularity_at f z ∧ not_essential f z"
proof (cases "z ∈ pts")
case False
have "f holomorphic_on A - pts - {z}"
by (intro holomorphic_on_subset[OF holo]) auto
hence "isolated_singularity_at f z"
by (rule isolated_singularity_at_holomorphic)
(use z False in ‹auto intro!: meromorphic_imp_open_diff[OF mero]›)
moreover have "not_essential f z"
using z False
by (intro not_essential_holomorphic[OF holo] meromorphic_imp_open_diff[OF mero]) auto
ultimately show ?thesis by blast
qed (use assms in ‹auto simp: meromorphic_on_def›)
thus "isolated_singularity_at (λz. inverse (f z)) z" "not_essential (λz. inverse (f z)) z"
by (auto intro!: isolated_singularity_at_inverse not_essential_inverse)
next
fix z assume "z ∈ A"
hence "¬ z islimpt {z∈A. isolated_zero f z}"
by (rule not_islimpt_isolated_zeros[OF mero])
thus "¬ z islimpt pts ∪ {z ∈ A. isolated_zero f z}" using ‹z ∈ A›
using mero by (auto simp: islimpt_Un meromorphic_on_def)
next
show "pts ∪ {z ∈ A. isolated_zero f z} ⊆ A"
using mero by (auto simp: meromorphic_on_def)
next
have "(λz. inverse (f z)) analytic_on (⋃w∈A - (pts ∪ {z ∈ A. isolated_zero f z}) . {w})"
unfolding analytic_on_UN
proof (intro ballI)
fix w assume w: "w ∈ A - (pts ∪ {z ∈ A. isolated_zero f z})"
show "(λz. inverse (f z)) analytic_on {w}"
proof (cases "f w = 0")
case False
thus ?thesis using w
by (intro analytic_intros analytic_on_subset[OF ana]) auto
next
case True
have "eventually (λw. f w = 0) (nhds w)"
using True w by (intro non_isolated_zero analytic_on_subset[OF ana]) auto
hence "(λz. inverse (f z)) analytic_on {w} ⟷ (λ_. 0) analytic_on {w}"
using w by (intro analytic_at_cong refl) auto
thus ?thesis
by simp
qed
qed
also have "… = A - (pts ∪ {z ∈ A. isolated_zero f z})"
by blast
finally have "(λz. inverse (f z)) analytic_on …" .
moreover have "open (A - (pts ∪ {z ∈ A. isolated_zero f z}))"
using closedin_isolated_zeros[OF mero] open' ‹open A›
by (metis (no_types, lifting) Diff_Diff_Int Diff_Un closedin_closed open_Diff open_Int)
ultimately show "(λz. inverse (f z)) holomorphic_on A - (pts ∪ {z ∈ A. isolated_zero f z})"
by (subst (asm) analytic_on_open) auto
qed (use assms in ‹auto simp: meromorphic_on_def islimpt_Un
intro!: holomorphic_intros singularity_intros›)
qed

lemma meromorphic_on_inverse'' [meromorphic_intros]:
assumes "f meromorphic_on A pts" "{z∈A. f z = 0} ⊆ pts"
shows   "(λz. inverse (f z)) meromorphic_on A pts"
proof -
have "(λz. inverse (f z)) meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
by (intro meromorphic_on_inverse assms)
also have "(pts ∪ {z ∈ A. isolated_zero f z}) = pts"
using assms(2) by (auto simp: isolated_zero_def)
finally show ?thesis .
qed

lemma meromorphic_on_divide [meromorphic_intros]:
assumes "f meromorphic_on A pts" and "g meromorphic_on A pts"
shows   "(λz. f z / g z) meromorphic_on A (pts ∪ {z∈A. isolated_zero g z})"
proof -
have mero1: "(λz. inverse (g z)) meromorphic_on A (pts ∪ {z∈A. isolated_zero g z})"
by (intro meromorphic_intros assms)
have sparse: "∀x∈A. ¬ x islimpt pts ∪ {z∈A. isolated_zero g z}" and "pts ⊆ A"
using mero1 by (auto simp: meromorphic_on_def)
have mero2: "f meromorphic_on A (pts ∪ {z∈A. isolated_zero g z})"
by (rule meromorphic_on_superset_pts[OF assms(1)]) (use sparse ‹pts ⊆ A› in auto)
have "(λz. f z * inverse (g z)) meromorphic_on A (pts ∪ {z∈A. isolated_zero g z})"
by (intro meromorphic_on_mult mero1 mero2)
thus ?thesis
qed

lemma meromorphic_on_divide' [meromorphic_intros]:
assumes "f meromorphic_on A pts" "g meromorphic_on A pts" "{z∈A. g z = 0} ⊆ pts"
shows   "(λz. f z / g z) meromorphic_on A pts"
proof -
have "(λz. f z * inverse (g z)) meromorphic_on A pts"
by (intro meromorphic_intros assms)
thus ?thesis
qed

lemma meromorphic_on_cmult_left [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λx. c * f x) meromorphic_on A pts"
using assms by (intro meromorphic_intros) (auto simp: meromorphic_on_def)

lemma meromorphic_on_cmult_right [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λx. f x * c) meromorphic_on A pts"
using assms by (intro meromorphic_intros) (auto simp: meromorphic_on_def)

lemma meromorphic_on_scaleR [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λx. c *⇩R f x) meromorphic_on A pts"
using assms unfolding scaleR_conv_of_real
by (intro meromorphic_intros) (auto simp: meromorphic_on_def)

lemma meromorphic_on_sum [meromorphic_intros]:
assumes "⋀y. y ∈ I ⟹ f y meromorphic_on A pts"
assumes "I ≠ {} ∨ open A ∧ pts ⊆ A ∧ (∀x∈A. ¬x islimpt pts)"
shows   "(λx. ∑y∈I. f y x) meromorphic_on A pts"
proof -
have *: "open A ∧ pts ⊆ A ∧ (∀x∈A. ¬x islimpt pts)"
using assms(2)
proof
assume "I ≠ {}"
then obtain x where "x ∈ I"
by blast
from assms(1)[OF this] show ?thesis
by (auto simp: meromorphic_on_def)
qed auto
show ?thesis
using assms(1)
by (induction I rule: infinite_finite_induct) (use * in ‹auto intro!: meromorphic_intros›)
qed

lemma meromorphic_on_prod [meromorphic_intros]:
assumes "⋀y. y ∈ I ⟹ f y meromorphic_on A pts"
assumes "I ≠ {} ∨ open A ∧ pts ⊆ A ∧ (∀x∈A. ¬x islimpt pts)"
shows   "(λx. ∏y∈I. f y x) meromorphic_on A pts"
proof -
have *: "open A ∧ pts ⊆ A ∧ (∀x∈A. ¬x islimpt pts)"
using assms(2)
proof
assume "I ≠ {}"
then obtain x where "x ∈ I"
by blast
from assms(1)[OF this] show ?thesis
by (auto simp: meromorphic_on_def)
qed auto
show ?thesis
using assms(1)
by (induction I rule: infinite_finite_induct) (use * in ‹auto intro!: meromorphic_intros›)
qed

lemma meromorphic_on_power [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λx. f x ^ n) meromorphic_on A pts"
proof -
have "(λx. ∏i∈{..<n}. f x) meromorphic_on A pts"
by (intro meromorphic_intros assms(1)) (use assms in ‹auto simp: meromorphic_on_def›)
thus ?thesis
by simp
qed

lemma meromorphic_on_power_int [meromorphic_intros]:
assumes "f meromorphic_on A pts"
shows   "(λz. f z powi n) meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
proof -
have inv: "(λx. inverse (f x)) meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
by (intro meromorphic_intros assms)
have *: "f meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
by (intro meromorphic_on_superset_pts [OF assms(1)])
(use inv in ‹auto simp: meromorphic_on_def›)
show ?thesis
proof (cases "n ≥ 0")
case True
have "(λx. f x ^ nat n) meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
by (intro meromorphic_intros *)
thus ?thesis
using True by (simp add: power_int_def)
next
case False
have "(λx. inverse (f x) ^ nat (-n)) meromorphic_on A (pts ∪ {z ∈ A. isolated_zero f z})"
by (intro meromorphic_intros assms)
thus ?thesis
using False by (simp add: power_int_def)
qed
qed

lemma meromorphic_on_power_int' [meromorphic_intros]:
assumes "f meromorphic_on A pts" "n ≥ 0 ∨ (∀z∈A. isolated_zero f z ⟶ z ∈ pts)"
shows   "(λz. f z powi n) meromorphic_on A pts"
proof (cases "n ≥ 0")
case True
have "(λz. f z ^ nat n) meromorphic_on A pts"
by (intro meromorphic_intros assms)
thus ?thesis
using True by (simp add: power_int_def)
next
case False
have "(λz. f z powi n) meromorphic_on A (pts ∪ {z∈A. isolated_zero f z})"
by (rule meromorphic_on_power_int) fact
also from assms(2) False have "pts ∪ {z∈A. isolated_zero f z} = pts"
by auto
finally show ?thesis .
qed

lemma has_laurent_expansion_on_imp_meromorphic_on:
assumes "open A"
assumes laurent: "⋀z. z ∈ A ⟹ ∃F. (λw. f (z + w)) has_laurent_expansion F"
shows   "f meromorphic_on A {z∈A. ¬f analytic_on {z}}"
unfolding meromorphic_on_def
proof (intro conjI ballI)
fix z assume "z ∈ {z∈A. ¬f analytic_on {z}}"
then obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
using laurent[of z] by blast
from F show "not_essential f z" "isolated_singularity_at f z"
using has_laurent_expansion_not_essential has_laurent_expansion_isolated by blast+
next
fix z assume z: "z ∈ A"
obtain F where F: "(λw. f (z + w)) has_laurent_expansion F"
using laurent[of z] ‹z ∈ A› by blast
from F have "isolated_singularity_at f z"
using has_laurent_expansion_isolated z by blast
then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
unfolding isolated_singularity_at_def by blast
have "f analytic_on {w}" if "w ∈ ball z r - {z}" for w
by (rule analytic_on_subset[OF r(2)]) (use that in auto)
hence "eventually (λw. f analytic_on {w}) (at z)"
using eventually_at_in_open[of "ball z r" z] ‹r > 0› by (auto elim!: eventually_mono)
hence "¬z islimpt {w. ¬f analytic_on {w}}"
by (auto simp: islimpt_conv_frequently_at frequently_def)
thus "¬z islimpt {w∈A. ¬f analytic_on {w}}"
using islimpt_subset[of z "{w∈A. ¬f analytic_on {w}}" "{w. ¬f analytic_on {w}}"] by blast
next
have "f analytic_on A - {w∈A. ¬f analytic_on {w}}"
by (subst analytic_on_analytic_at) auto
thus "f holomorphic_on A - {w∈A. ¬f analytic_on {w}}"
by (meson analytic_imp_holomorphic)
qed (use assms in auto)

lemma meromorphic_on_imp_has_laurent_expansion:
assumes "f meromorphic_on A pts" "z ∈ A"
shows   "(λw. f (z + w)) has_laurent_expansion laurent_expansion f z"
proof (cases "z ∈ pts")
case True
thus ?thesis
using assms by (intro not_essential_has_laurent_expansion) (auto simp: meromorphic_on_def)
next
case False
have "f holomorphic_on (A - pts)"
using assms by (auto simp: meromorphic_on_def)
moreover have "z ∈ A - pts" "open (A - pts)"
using assms(2) False by (auto intro!: meromorphic_imp_open_diff[OF assms(1)])
ultimately have "f analytic_on {z}"
unfolding analytic_at by blast
thus ?thesis
using isolated_singularity_at_analytic not_essential_analytic
not_essential_has_laurent_expansion by blast
qed

lemma
assumes "isolated_singularity_at f z" "f ─z→ c"
shows   eventually_remove_sings_eq_nhds':
"eventually (λw. remove_sings f w = (if w = z then c else f w)) (nhds z)"
and   remove_sings_analytic_at_singularity: "remove_sings f analytic_on {z}"
proof -
have "eventually (λw. w ≠ z) (at z)"
by (auto simp: eventually_at_filter)
hence "eventually (λw. remove_sings f w = (if w = z then c else f w)) (at z)"
using eventually_remove_sings_eq_at[OF assms(1)]
by eventually_elim auto
moreover have "remove_sings f z = c"
using assms by auto
ultimately show ev: "eventually (λw. remove_sings f w = (if w = z then c else f w)) (nhds z)"

have "(λw. if w = z then c else f w) analytic_on {z}"
by (intro removable_singularity' assms)
also have "?this ⟷ remove_sings f analytic_on {z}"
using ev by (intro analytic_at_cong) (auto simp: eq_commute)
finally show … .
qed

lemma remove_sings_meromorphic_on:
assumes "f meromorphic_on A pts" "⋀z. z ∈ pts - pts' ⟹ ¬is_pole f z" "pts' ⊆ pts"
shows   "remove_sings f meromorphic_on A pts'"
unfolding meromorphic_on_def
proof safe
have "remove_sings f analytic_on {z}" if "z ∈ A - pts'" for z
proof (cases "z ∈ pts")
case False
hence *: "f analytic_on {z}"
using assms meromorphic_imp_open_diff[OF assms(1)] that
by (force simp: meromorphic_on_def analytic_at)
have "remove_sings f analytic_on {z} ⟷ f analytic_on {z}"
by (intro analytic_at_cong eventually_remove_sings_eq_nhds * refl)
thus ?thesis using * by simp
next
case True
have isol: "isolated_singularity_at f z"
using True using assms by (auto simp: meromorphic_on_def)
from assms(1) have "not_essential f z"
using True by (auto simp: meromorphic_on_def)
with assms(2) True that obtain c where "f ─z→ c"
by (auto simp: not_essential_def)
thus "remove_sings f analytic_on {z}"
by (intro remove_sings_analytic_at_singularity isol)
qed
hence "remove_sings f analytic_on A - pts'"
by (subst analytic_on_analytic_at) auto
thus "remove_sings f holomorphic_on A - pts'"
using meromorphic_imp_open_diff'[OF assms(1,3)] by (subst (asm) analytic_on_open)
qed (use assms islimpt_subset[OF _ assms(3)] in ‹auto simp: meromorphic_on_def›)

lemma remove_sings_holomorphic_on:
assumes "f meromorphic_on A pts" "⋀z. z ∈ pts ⟹ ¬is_pole f z"
shows   "remove_sings f holomorphic_on A"
using remove_sings_meromorphic_on[OF assms(1), of "{}"] assms(2)
by (auto simp: meromorphic_on_no_singularities)

lemma meromorphic_on_Ex_iff:
"(∃pts. f meromorphic_on A pts) ⟷
open A ∧ (∀z∈A. ∃F. (λw. f (z + w)) has_laurent_expansion F)"
proof safe
fix pts assume *: "f meromorphic_on A pts"
from * show "open A"
by (auto simp: meromorphic_on_def)
show "∃F. (λw. f (z + w)) has_laurent_expansion F" if "z ∈ A" for z
using that *
by (intro exI[of _ "laurent_expansion f z"] meromorphic_on_imp_has_laurent_expansion)
qed (blast intro!: has_laurent_expansion_on_imp_meromorphic_on)

lemma is_pole_inverse_holomorphic_pts:
fixes pts::"complex set" and f::"complex ⇒ complex"
defines "g ≡ λx. (if x∈pts then 0 else inverse (f x))"
assumes mer: "f meromorphic_on D pts"
and non_z: "⋀z. z ∈ D - pts ⟹ f z ≠ 0"
and all_poles:"∀x. is_pole f x ⟷ x∈pts"
shows "g holomorphic_on D"
proof -
have "open D" and f_holo: "f holomorphic_on (D-pts)"
using mer by (auto simp: meromorphic_on_def)
have "∃r. r>0 ∧ f analytic_on ball z r - {z}
∧ (∀x ∈ ball z r - {z}. f x≠0)" if "z∈pts" for z
proof -
have "isolated_singularity_at f z" "is_pole f z"
using mer meromorphic_on_def that all_poles by blast+
then obtain r1 where "r1>0" and fan: "f analytic_on ball z r1 - {z}"
by (meson isolated_singularity_at_def)
obtain r2 where "r2>0" "∀x ∈ ball z r2 - {z}. f x≠0"
using non_zero_neighbour_pole[OF ‹is_pole f z›]
unfolding eventually_at by (metis Diff_iff UNIV_I dist_commute insertI1 mem_ball)
define r where "r = min r1 r2"
have "r>0" by (simp add: ‹0 < r2› ‹r1>0› r_def)
moreover have "f analytic_on ball z r - {z}"
using r_def by (force intro: analytic_on_subset [OF fan])
moreover have "∀x ∈ ball z r - {z}. f x≠0"
by (simp add: ‹∀x∈ball z r2 - {z}. f x ≠ 0› r_def)
ultimately show ?thesis by auto
qed
then obtain get_r where r_pos:"get_r z>0"
and r_ana:"f analytic_on ball z (get_r z) - {z}"
and r_nz:"∀x ∈ ball z (get_r z) - {z}. f x≠0"
if "z∈pts" for z
by metis
define p_balls where "p_balls ≡ ⋃z∈pts. ball z (get_r z)"
have g_ball:"g holomorphic_on ball z (get_r z)" if "z∈pts" for z
proof -
have "(λx. if x = z then 0 else inverse (f x)) holomorphic_on ball z (get_r z)"
proof (rule is_pole_inverse_holomorphic)
show "f holomorphic_on ball z (get_r z) - {z}"
using analytic_imp_holomorphic r_ana that by blast
show "is_pole f z"
using mer meromorphic_on_def that all_poles by force
show "∀x∈ball z (get_r z) - {z}. f x ≠ 0"
using r_nz that by metis
qed auto
then show ?thesis unfolding g_def
by (smt (verit, ccfv_SIG) Diff_iff Elementary_Metric_Spaces.open_ball
all_poles analytic_imp_holomorphic empty_iff
holomorphic_transform insert_iff not_is_pole_holomorphic
open_delete r_ana that)
qed
then have "g holomorphic_on p_balls"
proof -
have "g analytic_on p_balls"
unfolding p_balls_def analytic_on_UN
using g_ball by (simp add: analytic_on_open)
moreover have "open p_balls" using p_balls_def by blast
ultimately show ?thesis
qed
moreover have "g holomorphic_on D-pts"
proof -
have "(λz. inverse (f z)) holomorphic_on D - pts"
using f_holo holomorphic_on_inverse non_z by blast
then show ?thesis
by (metis DiffD2 g_def holomorphic_transform)
qed
moreover have "open p_balls"
using p_balls_def by blast
ultimately have "g holomorphic_on (p_balls ∪ (D-pts))"
by (simp add: holomorphic_on_Un meromorphic_imp_open_diff[OF mer])
moreover have "D ⊆ p_balls ∪ (D-pts)"
unfolding p_balls_def using ‹⋀z. z ∈ pts ⟹ 0 < get_r z› by force
ultimately show "g holomorphic_on D" by (meson holomorphic_on_subset)
qed

lemma meromorphic_imp_analytic_on:
assumes "f meromorphic_on D pts"
shows "f analytic_on (D - pts)"
by (metis assms analytic_on_open meromorphic_imp_open_diff meromorphic_on_def)

lemma meromorphic_imp_constant_on:
assumes merf: "f meromorphic_on D pts"
and "f constant_on (D - pts)"
and "∀x∈pts. is_pole f x"
shows "f constant_on D"
proof -
obtain c where c:"⋀z. z ∈ D-pts ⟹ f z = c"
by (meson assms constant_on_def)

have "f z = c" if "z ∈ D" for z
proof (cases "is_pole f z")
case True
then obtain r0 where "r0 > 0" and r0: "f analytic_on ball z r0 - {z}" and pol: "is_pole f z"
using merf unfolding meromorphic_on_def isolated_singularity_at_def
by (metis ‹z ∈ D› insert_Diff insert_Diff_if insert_iff merf
meromorphic_imp_open_diff not_is_pole_holomorphic)
have "open D"
using merf meromorphic_on_def by auto
then obtain r where "r > 0" "ball z r ⊆ D" "r ≤ r0"
by (smt (verit, best) ‹0 < r0› ‹z ∈ D› openE order_subst2 subset_ball)
have r: "f analytic_on ball z r - {z}"
by (meson Diff_mono ‹r ≤ r0› analytic_on_subset order_refl r0 subset_ball)
have "ball z r - {z} ⊆ -pts"
using merf r unfolding meromorphic_on_def
by (meson ComplI Elementary_Metric_Spaces.open_ball
analytic_imp_holomorphic assms(3) not_is_pole_holomorphic open_delete subsetI)
with ‹ball z r ⊆ D› have "ball z r - {z} ⊆ D-pts"
by fastforce
with c have c': "⋀u. u ∈ ball z r - {z} ⟹ f u = c"
by blast
have False if "∀⇩F x in at z. cmod c + 1 ≤ cmod (f x)"
proof -
have "∀⇩F x in at z within ball z r - {z}. cmod c + 1 ≤ cmod (f x)"
by (smt (verit, best) Diff_UNIV Diff_eq_empty_iff eventually_at_topological insert_subset that)
with ‹r > 0› show ?thesis
apply (simp add: c' eventually_at_filter topological_space_class.eventually_nhds open_dist)
by (metis dist_commute min_less_iff_conj perfect_choose_dist)
qed
with pol show ?thesis
by (auto simp: is_pole_def filterlim_at_infinity_conv_norm_at_top filterlim_at_top)
next
case False
then show ?thesis by (meson DiffI assms(3) c that)
qed
then show ?thesis
qed

lemma meromorphic_isolated:
assumes merf: "f meromorphic_on D pts" and "p∈pts"
obtains r where "r>0" "ball p r ⊆ D" "ball p r ∩ pts = {p}"
proof -
have "∀z∈D. ∃e>0. finite (pts ∩ ball z e)"
using merf unfolding meromorphic_on_def islimpt_eq_infinite_ball
by auto
then obtain r0 where r0:"r0>0" "finite (pts ∩ ball p r0)"
by (metis assms(2) in_mono merf meromorphic_on_def)
moreover define pts' where "pts' = pts ∩ ball p r0 - {p}"
ultimately have "finite pts'"
by simp

define r1 where "r1=(if pts'={} then r0 else
min (Min {dist p' p |p'. p'∈pts'}/2) r0)"
have "r1>0 ∧ pts ∩ ball p r1 - {p} = {}"
proof (cases "pts'={}")
case True
then show ?thesis
using pts'_def r0(1) r1_def by presburger
next
case False
define S where "S={dist p' p |p'. p'∈pts'}"

have nempty:"S ≠ {}"
using False S_def by blast
have finite:"finite S"
using ‹finite pts'› S_def by simp

have "r1>0"
proof -
have "r1=min (Min S/2) r0"
using False unfolding S_def r1_def by auto
moreover have "Min S∈S"
using ‹S≠{}› ‹finite S›  Min_in by auto
then have "Min S>0" unfolding S_def
using pts'_def by force
ultimately show ?thesis using ‹r0>0› by auto
qed
moreover have "pts ∩ ball p r1 - {p} = {}"
proof (rule ccontr)
assume "pts ∩ ball p r1 - {p} ≠ {}"
then obtain p' where "p'∈pts ∩ ball p r1 - {p}" by blast
moreover have "r1≤r0" using r1_def by auto
ultimately have "p'∈pts'" unfolding pts'_def
by auto
then have "dist p' p≥Min S"
using S_def eq_Min_iff local.finite by blast
moreover have "dist p' p < Min S"
using ‹p'∈pts ∩ ball p r1 - {p}› False unfolding r1_def
apply (fold S_def)
by (smt (verit, ccfv_threshold) DiffD1 Int_iff dist_commute
dist_triangle_half_l mem_ball)
ultimately show False by auto
qed
ultimately show ?thesis by auto
qed
then have "r1>0" and r1_pts:"pts ∩ ball p r1 - {p} = {}" by auto

obtain r2 where "r2>0" "ball p r2 ⊆ D"
by (metis assms(2) merf meromorphic_on_def openE subset_eq)
define r where "r=min r1 r2"
have "r > 0" unfolding r_def
by (simp add: ‹0 < r1› ‹0 < r2›)
moreover have "ball p r ⊆ D"
using ‹ball p r2 ⊆ D› r_def by auto
moreover have "ball p r ∩ pts = {p}"
using assms(2) ‹r>0› r1_pts
unfolding r_def by auto
ultimately show ?thesis using that by auto
qed

lemma meromorphic_pts_closure:
assumes merf: "f meromorphic_on D pts"
shows "pts ⊆ closure (D - pts)"
proof -
have "p islimpt (D - pts)" if "p∈pts" for p
proof -
obtain r where "r>0" "ball p r ⊆ D" "ball p r ∩ pts = {p}"
using meromorphic_isolated[OF merf ‹p∈pts›] by auto
from ‹r>0›
have "p islimpt ball p r - {p}"
by (meson open_ball ball_subset_cball in_mono islimpt_ball
islimpt_punctured le_less open_contains_ball_eq)
moreover have " ball p r - {p} ⊆ D - pts"
using ‹ball p r ∩ pts = {p}› ‹ball p r ⊆ D› by fastforce
ultimately show ?thesis
using islimpt_subset by auto
qed
then show ?thesis by (simp add: islimpt_in_closure subset_eq)
qed

lemma nconst_imp_nzero_neighbour:
assumes merf: "f meromorphic_on D pts"
and f_nconst:"¬(∀w∈D-pts. f w=0)"
and "z∈D" and "connected D"
shows "(∀⇩F w in at z. f w ≠ 0 ∧ w ∈ D - pts)"
proof -
obtain β where β:"β ∈ D - pts" "f β≠0"
using f_nconst by auto

have ?thesis if "z∉pts"
proof -
have "∀⇩F w in at z. f w ≠ 0 ∧ w ∈ D - pts"
apply (rule non_zero_neighbour_alt[of f "D-pts" z  β])
subgoal using merf meromorphic_on_def by blast
subgoal using merf meromorphic_imp_open_diff by auto
subgoal using assms(4) merf meromorphic_imp_connected_diff by blast
subgoal by (simp add: assms(3) that)
using β by auto
then show ?thesis by (auto elim:eventually_mono)
qed
moreover have ?thesis if "z∈pts" "¬ f ─z→ 0"
proof -
have "∀⇩F w in at z. w ∈ D - pts"
using merf[unfolded meromorphic_on_def islimpt_iff_eventually] ‹z∈D›
using eventually_at_in_open' eventually_elim2 by fastforce
moreover have "∀⇩F w in at z. f w ≠ 0"
proof (cases  "is_pole f z")
case True
then show ?thesis using non_zero_neighbour_pole by auto
next
case False
moreover have "not_essential f z"
using merf meromorphic_on_def that(1) by fastforce
ultimately obtain c where "c≠0" "f ─z→ c"
by (metis ‹¬ f ─z→ 0› not_essential_def)
then show ?thesis
using tendsto_imp_eventually_ne by auto
qed
ultimately show ?thesis by eventually_elim auto
qed
moreover have ?thesis if "z∈pts" "f ─z→ 0"
proof -
define ff where "ff=(λx. if x=z then 0 else f x)"
define A where "A=D - (pts - {z})"

have "f holomorphic_on A - {z}"
by (metis A_def Diff_insert analytic_imp_holomorphic
insert_Diff merf meromorphic_imp_analytic_on that(1))
moreover have "open A"
using A_def merf meromorphic_imp_open_diff' by force
ultimately have "ff holomorphic_on A"
using ‹f ─z→ 0› unfolding ff_def
by (rule removable_singularity)
moreover have "connected A"
proof -
have "connected (D - pts)"
using assms(4) merf meromorphic_imp_connected_diff by auto
moreover have "D - pts ⊆ A"
unfolding A_def by auto
moreover have "A ⊆ closure (D - pts)" unfolding A_def
by (smt (verit, ccfv_SIG) Diff_empty Diff_insert
closure_subset insert_Diff_single insert_absorb
insert_subset merf meromorphic_pts_closure that(1))
ultimately show ?thesis using connected_intermediate_closure
by auto
qed
moreover have "z ∈ A" using A_def assms(3) by blast
moreover have "ff z = 0" unfolding ff_def by auto
moreover have "β ∈ A " using A_def β(1) by blast
moreover have "ff β ≠ 0" using β(1) β(2) ff_def that(1) by auto
ultimately obtain r where "0 < r"
"ball z r ⊆ A" "⋀x. x ∈ ball z r - {z} ⟹ ff x ≠ 0"
using ‹open A› isolated_zeros[of ff A z β] by auto
then show ?thesis unfolding eventually_at ff_def
by (intro exI[of _ r]) (auto simp: A_def dist_commute ball_def)
qed
ultimately show ?thesis by auto
qed

lemma nconst_imp_nzero_neighbour':
assumes merf: "f meromorphic_on D pts"
and f_nconst:"¬(∀w∈D-pts. f w=0)"
and "z∈D" and "connected D"
shows "∀⇩F w in at z. f w ≠ 0"
using nconst_imp_nzero_neighbour[OF assms]
by (auto elim:eventually_mono)

lemma meromorphic_compact_finite_zeros:
assumes merf:"f meromorphic_on D pts"
and "compact S" "S ⊆ D" "connected D"
and f_nconst:"¬(∀w∈D-pts. f w=0)"
shows "finite ({x∈S. f x=0})"
proof -
have "finite ({x∈S. f x=0 ∧ x ∉ pts})"
proof (rule ccontr)
assume "infinite {x ∈ S. f x = 0 ∧ x ∉ pts}"
then obtain z where "z∈S" and z_lim:"z islimpt {x ∈ S. f x = 0
∧ x ∉ pts}"
using ‹compact S› unfolding compact_eq_Bolzano_Weierstrass
by auto

from z_lim
have "∃⇩F x in at z. f x = 0 ∧ x ∈ S ∧ x ∉ pts"
unfolding islimpt_iff_eventually not_eventually by simp
moreover have "∀⇩F w in at z. f w ≠ 0 ∧ w ∈ D - pts"
using nconst_imp_nzero_neighbour[OF merf f_nconst _ ‹connected D›]
‹z∈S› ‹S ⊆ D›
by auto
ultimately have "∃⇩F x in at z. False"
then show False by auto
qed
moreover have "finite (S ∩ pts)"
using meromorphic_compact_finite_pts[OF merf ‹compact S› ‹S ⊆ D›] .
ultimately have "finite ({x∈S. f x=0 ∧ x ∉ pts} ∪ (S ∩ pts))"
unfolding finite_Un by auto
then show ?thesis by (elim rev_finite_subset) auto
qed

lemma meromorphic_onI [intro?]:
assumes "open A" "pts ⊆ A"
assumes "f holomorphic_on A - pts" "⋀z. z ∈ A ⟹ ¬z islimpt pts"
assumes "⋀z. z ∈ pts ⟹ isolated_singularity_at f z"
assumes "⋀z. z ∈ pts ⟹ not_essential f z"
shows   "f meromorphic_on A pts"
using assms unfolding meromorphic_on_def by blast

lemma Polygamma_plus_of_nat:
assumes "∀k<m. z ≠ -of_nat k"
shows   "Polygamma n (z + of_nat m) =
Polygamma n z + (-1) ^ n * fact n * (∑k<m. 1 / (z + of_nat k) ^ Suc n)"
using assms
proof (induction m)
case (Suc m)
have "Polygamma n (z + of_nat (Suc m)) = Polygamma n (z + of_nat m + 1)"