Quelle  Complex_Singularities.thy

theory Complex_Singularities
  imports Conformal_Mappings
begin

subsection ‹Non-essential singular points›

lemma at_to_0': "NO_MATCH 0 z ==> at z = filtermap (λx. x + z) (at 0)"
  for z :: "'a::real_normed_vector"
  by (rule at_to_0)

lemma nhds_to_0: "nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)"
proof -
  have "(λxa. xa - - x) = (+) x"
    by auto
  thus ?thesis
    using filtermap_nhds_shift[of "-x" 0] by simp
qed

lemma nhds_to_0': "NO_MATCH 0 x ==> nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)"
  by (rule nhds_to_0)


definition🍋‹tag important›
  is_pole :: "('a::topological_space ==> 'b::real_normed_vector) ==> 'a ==> bool" 
  where "is_pole f a = (LIM x (at a). f x :> at_infinity)"

lemma is_pole_cong:
  assumes "eventually (λx. f x = g x) (at a)" "a=b"
  shows "is_pole f a ⟷ is_pole g b"
  unfolding is_pole_def using assms by (intro filterlim_cong,auto)

lemma is_pole_transform:
  assumes "is_pole f a" "eventually (λx. f x = g x) (at a)" "a=b"
  shows "is_pole g b"
  using is_pole_cong assms by auto

lemma is_pole_shift_iff:
  fixes f :: "('a::real_normed_vector ==> 'b::real_normed_vector)"
  shows "is_pole (f ∘ (+) d) a = is_pole f (a + d)"
  by (metis add_diff_cancel_right' filterlim_shift_iff is_pole_def)

lemma is_pole_tendsto:
  fixes f:: "('a::topological_space ==> 'b::real_normed_div_algebra)"
  shows "is_pole f x ==> ((inverse o f) ---> 0) (at x)"
  unfolding is_pole_def
  by (auto simp add: filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)

lemma is_pole_shift_0:
  fixes f :: "('a::real_normed_vector ==> 'b::real_normed_vector)"
  shows "is_pole f z ⟷ is_pole (λx. f (z + x)) 0"
  unfolding is_pole_def by (subst at_to_0) (auto simp: filterlim_filtermap add_ac)

lemma is_pole_shift_0':
  fixes f :: "('a::real_normed_vector ==> 'b::real_normed_vector)"
  shows "NO_MATCH 0 z ==> is_pole f z ⟷ is_pole (λx. f (z + x)) 0"
  by (metis is_pole_shift_0)

lemma is_pole_compose_iff:
  assumes "filtermap g (at x) = (at y)"
  shows   "is_pole (f ∘ g) x ⟷ is_pole f y"
  unfolding is_pole_def filterlim_def filtermap_compose assms ..

lemma is_pole_inverse_holomorphic:
  assumes "open s"
    and f_holo: "f holomorphic_on (s-{z})"
    and pole: "is_pole f z"
    and non_z: "∀x∈s-{z}. f x≠0"
  shows "(λx. if x=z then 0 else inverse (f x)) holomorphic_on s"
proof -
  define g where "g ≡ λx. if x=z then 0 else inverse (f x)"
  have "isCont g z" unfolding isCont_def  using is_pole_tendsto[OF pole]
    by (simp add: g_def cong: LIM_cong)
  moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
  hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
    by (auto elim!:continuous_on_inverse simp add: non_z)
  hence "continuous_on (s-{z}) g" unfolding g_def
    using continuous_on_eq by fastforce
  ultimately have "continuous_on s g" using open_delete[OF ‹open s›] ‹open s›
    by (auto simp add: continuous_on_eq_continuous_at)
  moreover have "(inverse o f) holomorphic_on (s-{z})"
    unfolding comp_def using f_holo
    by (auto elim!:holomorphic_on_inverse simp add: non_z)
  hence "g holomorphic_on (s-{z})"
    using g_def holomorphic_transform by force
  ultimately show ?thesis unfolding g_def using ‹open s›
    by (auto elim!: no_isolated_singularity)
qed

lemma not_is_pole_holomorphic:
  assumes "open A" "x ∈ A" "f holomorphic_on A"
  shows   "¬is_pole f x"
proof -
  have "continuous_on A f" 
    by (intro holomorphic_on_imp_continuous_on) fact
  with assms have "isCont f x" 
    by (simp add: continuous_on_eq_continuous_at)
  hence "f ←-x→ f x" 
    by (simp add: isCont_def)
  thus "¬is_pole f x" 
    unfolding is_pole_def
    using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto
qed

lemma is_pole_inverse_power: "n > 0 ==> is_pole (λz::complex. 1 / (z - a) ^ n) a"
  unfolding is_pole_def inverse_eq_divide [symmetric]
  by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
     (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)

lemma is_pole_cmult_iff [simp]:
  assumes "c ≠ 0"
  shows "is_pole (λz. c * f z :: 'a :: real_normed_field) z ⟷ is_pole f z"
proof
  assume "is_pole (λz. c * f z) z"
  with ‹c≠0› have "is_pole (λz. inverse c * (c * f z)) z" 
    unfolding is_pole_def
    by (force intro: tendsto_mult_filterlim_at_infinity)
  thus "is_pole f z"
    using ‹c≠0› by (simp add: field_simps)
next
  assume "is_pole f z"
  with ‹c≠0› show "is_pole (λz. c * f z) z"  
    by (auto intro!: tendsto_mult_filterlim_at_infinity simp: is_pole_def)
qed

lemma is_pole_uminus_iff [simp]: "is_pole (λz. -f z :: 'a :: real_normed_field) z ⟷ is_pole f z"
  using is_pole_cmult_iff[of "-1" f] by (simp del: is_pole_cmult_iff)

lemma is_pole_inverse: "is_pole (λz::complex. 1 / (z - a)) a"
  using is_pole_inverse_power[of 1 a] by simp

lemma is_pole_divide:
  fixes f :: "'a :: t2_space ==> 'b :: real_normed_field"
  assumes "isCont f z" "filterlim g (at 0) (at z)" "f z ≠ 0"
  shows   "is_pole (λz. f z / g z) z"
proof -
  have "filterlim (λz. f z * inverse (g z)) at_infinity (at z)"
    using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
      tendsto_mult_filterlim_at_infinity by blast
  thus ?thesis by (simp add: field_split_simps is_pole_def)
qed

lemma is_pole_basic:
  assumes "f holomorphic_on A" "open A" "z ∈ A" "f z ≠ 0" "n > 0"
  shows   "is_pole (λw. f w / (w-z) ^ n) z"
proof (rule is_pole_divide)
  have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact
  with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at)
  have "filterlim (λw. (w-z) ^ n) (nhds 0) (at z)"
    using assms by (auto intro!: tendsto_eq_intros)
  thus "filterlim (λw. (w-z) ^ n) (at 0) (at z)"
    by (intro filterlim_atI tendsto_eq_intros)
       (use assms in ‹auto simp: eventually_at_filter›)
qed fact+

lemma is_pole_basic':
  assumes "f holomorphic_on A" "open A" "0 ∈ A" "f 0 ≠ 0" "n > 0"
  shows   "is_pole (λw. f w / w ^ n) 0"
  using is_pole_basic[of f A 0] assms by simp

lemma is_pole_compose: 
  assumes "is_pole f w" "g ←-z→ w" "eventually (λz. g z ≠ w) (at z)"
  shows   "is_pole (λx. f (g x)) z"
  using assms(1) unfolding is_pole_def
  by (rule filterlim_compose) (use assms in ‹auto simp: filterlim_at›)

lemma is_pole_plus_const_iff:
  "is_pole f z ⟷ is_pole (λx. f x + c) z"
proof 
  assume "is_pole f z"
  then have "filterlim f at_infinity (at z)" unfolding is_pole_def .
  moreover have "((λ_. c) ---> c) (at z)" by auto
  ultimately have " LIM x (at z). f x + c :> at_infinity"
    using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto
  then show "is_pole (λx. f x + c) z" unfolding is_pole_def .
next
  assume "is_pole (λx. f x + c) z"
  then have "filterlim (λx. f x + c) at_infinity (at z)" 
    unfolding is_pole_def .
  moreover have "((λ_. -c) ---> -c) (at z)" by auto
  ultimately have "LIM x (at z). f x :> at_infinity"
    using tendsto_add_filterlim_at_infinity'[of "(λx. f x + c)"
        "at z" "(λ_. - c)" "-c"] 
    by auto
  then show "is_pole f z" unfolding is_pole_def .
qed

lemma is_pole_minus_const_iff:
  "is_pole (λx. f x - c) z ⟷ is_pole f z"
  using is_pole_plus_const_iff [of f z "-c"] by simp

lemma is_pole_alt:
  "is_pole f x = (∀B>0. ∃U. open U ∧ x∈U ∧ (∀y∈U. y≠x ⟶ norm (f y)≥B))"
  unfolding is_pole_def
  unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological
  by auto

lemma is_pole_mult_analytic_nonzero1:
  assumes "is_pole g x" "f analytic_on {x}" "f x ≠ 0"
  shows   "is_pole (λx. f x * g x) x"
  unfolding is_pole_def
proof (rule tendsto_mult_filterlim_at_infinity)
  show "f ←-x→ f x"
    using assms by (simp add: analytic_at_imp_isCont isContD)
qed (use assms in ‹auto simp: is_pole_def›)

lemma is_pole_mult_analytic_nonzero2:
  assumes "is_pole f x" "g analytic_on {x}" "g x ≠ 0"
  shows   "is_pole (λx. f x * g x) x"
proof -
  have g: "g analytic_on {x}"
    using assms by auto
  show ?thesis
    using is_pole_mult_analytic_nonzero1 [OF ‹is_pole f x› g] ‹g x ≠ 0›
    by (simp add: mult.commute)
qed

lemma is_pole_mult_analytic_nonzero1_iff:
  assumes "f analytic_on {x}" "f x ≠ 0"
  shows   "is_pole (λx. f x * g x) x ⟷ is_pole g x"
proof
  assume "is_pole g x"
  thus "is_pole (λx. f x * g x) x"
    by (intro is_pole_mult_analytic_nonzero1 assms)
next
  assume "is_pole (λx. f x * g x) x"
  hence "is_pole (λx. inverse (f x) * (f x * g x)) x"
    by (rule is_pole_mult_analytic_nonzero1)
       (use assms in ‹auto intro!: analytic_intros›)
  also have "?this ⟷ is_pole g x"
  proof (rule is_pole_cong)
    have "eventually (λx. f x ≠ 0) (at x)"
      using assms by (simp add: analytic_at_neq_imp_eventually_neq)
    thus "eventually (λx. inverse (f x) * (f x * g x) = g x) (at x)"
      by eventually_elim auto
  qed auto
  finally show "is_pole g x" .
qed

lemma is_pole_mult_analytic_nonzero2_iff:
  assumes "g analytic_on {x}" "g x ≠ 0"
  shows   "is_pole (λx. f x * g x) x ⟷ is_pole f x"
  by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+

lemma frequently_const_imp_not_is_pole:
  fixes z :: "'a::first_countable_topology"
  assumes "frequently (λw. f w = c) (at z)"
  shows   "¬ is_pole f z"
proof
  assume "is_pole f z"
  from assms have "z islimpt {w. f w = c}"
    by (simp add: islimpt_conv_frequently_at)
  then obtain g where g: "∧n. g n ∈ {w. f w = c} - {z}" "g <---- z"
    unfolding islimpt_sequential by blast
  then have "(f ∘ g) <---- c"
    by (simp add: tendsto_eventually)
  moreover have "filterlim g (at z) sequentially"
    using g by (auto simp: filterlim_at)
  then have "filterlim (f ∘ g) at_infinity sequentially"
    unfolding o_def
    using ‹is_pole f z› filterlim_compose is_pole_def by blast
  ultimately show False
    using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
qed

subsection ‹Isolated singularities›

text ‹The proposition
  🍋‹∃x. ((f::complex==>complex) ---> x) (at z) ∨ is_pole f z›
 can be interpreted as the complex function 🍋‹f› has a non-essential singularity at 🍋‹z›
 (i.e. the singularity is either removable or a pole).›
definition not_essential:: "[complex ==> complex, complex] ==> bool" where
  "not_essential f z = (∃x. f←-z→x ∨ is_pole f z)"

definition isolated_singularity_at:: "[complex ==> complex, complex] ==> bool" where
  "isolated_singularity_at f z = (∃r>0. f analytic_on ball z r-{z})"

lemma not_essential_cong:
  assumes "eventually (λx. f x = g x) (at z)" "z = z'"
  shows   "not_essential f z ⟷ not_essential g z'"
  unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce

lemma not_essential_compose_iff:
  assumes "filtermap g (at z) = at z'"
  shows   "not_essential (f ∘ g) z = not_essential f z'"
  unfolding not_essential_def filterlim_def filtermap_compose assms is_pole_compose_iff[OF assms]
  by blast

lemma isolated_singularity_at_cong:
  assumes "eventually (λx. f x = g x) (at z)" "z = z'"
  shows   "isolated_singularity_at f z ⟷ isolated_singularity_at g z'"
proof -
  have "isolated_singularity_at g z"
    if "isolated_singularity_at f z" "eventually (λx. f x = g x) (at z)" for f g
  proof -
    from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
      by (auto simp: isolated_singularity_at_def)
    from that(2) obtain r' where r': "r' > 0" "∀x∈ball z r'-{z}. f x = g x"
      unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute)

    have "f holomorphic_on ball z r - {z}"
      using r(2) by (subst (asm) analytic_on_open) auto
    hence "f holomorphic_on ball z (min r r') - {z}"
      by (rule holomorphic_on_subset) auto
    also have "?this ⟷ g holomorphic_on ball z (min r r') - {z}"
      using r' by (intro holomorphic_cong) auto
    also have "… ⟷ g analytic_on ball z (min r r') - {z}"
      by (subst analytic_on_open) auto
    finally show ?thesis
      unfolding isolated_singularity_at_def
      by (intro exI[of _ "min r r'"]) (use ‹r > 0› ‹r' > 0› in auto)
  qed
  from this[of f g] this[of g f] assms show ?thesis
    by (auto simp: eq_commute)
qed
  
lemma removable_singularity:
  assumes "f holomorphic_on A - {x}" "open A"
  assumes "f ←-x→ c"
  shows   "(λy. if y = x then c else f y) holomorphic_on A" (is "?g holomorphic_on _")
proof -
  have "continuous_on A ?g"
    unfolding continuous_on_def
  proof
    fix y assume y: "y ∈ A"
    show "(?g ---> ?g y) (at y within A)"
    proof (cases "y = x")
      case False
      have "continuous_on (A - {x}) f"
        using assms(1) by (meson holomorphic_on_imp_continuous_on)
      hence "(f ---> ?g y) (at y within A - {x})"
        using False y by (auto simp: continuous_on_def)
      also have "?this ⟷ (?g ---> ?g y) (at y within A - {x})"
        by (intro filterlim_cong refl) (auto simp: eventually_at_filter)
      also have "at y within A - {x} = at y within A"
        using y assms False
        by (intro at_within_nhd[of _ "A - {x}"]) auto
      finally show ?thesis .
    next
      case [simp]: True
      have "f ←-x→ c"
        by fact
      also have "?this ⟷ (?g ---> ?g y) (at y)"
        by (simp add: LIM_equal)
      finally show ?thesis
        by (meson Lim_at_imp_Lim_at_within)
    qed
  qed
  moreover {
    have "?g holomorphic_on A - {x}"
      using assms(1) holomorphic_transform by fastforce
  }
  ultimately show ?thesis
    using assms by (simp add: no_isolated_singularity)
qed

lemma removable_singularity':
  assumes "isolated_singularity_at f z"
  assumes "f ←-z→ c"
  shows   "(λy. if y = z then c else f y) analytic_on {z}"
proof -
  from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
    by (auto simp: isolated_singularity_at_def)
  have "(λy. if y = z then c else f y) holomorphic_on ball z r"
  proof (rule removable_singularity)
    show "f holomorphic_on ball z r - {z}"
      using r(2) by (subst (asm) analytic_on_open) auto
  qed (use assms in auto)
  thus ?thesis
    using r(1) unfolding analytic_at by (intro exI[of _ "ball z r"]) auto
qed

named_theorems singularity_intros "introduction rules for singularities"

lemma holomorphic_factor_unique:
  fixes f:: "complex ==> complex" and z::complex and r::real and m n::int
  assumes "r>0" "g z≠0" "h z≠0"
    and asm: "∀w∈ball z r-{z}. f w = g w * (w-z) powi n ∧ g w≠0 ∧ f w = h w * (w-z) powi m ∧ h w≠0"
    and g_holo: "g holomorphic_on ball z r" and h_holo: "h holomorphic_on ball z r"
  shows "n=m"
proof -
  have [simp]: "at z within ball z r ≠ bot" using ‹r>0›
      by (auto simp add: at_within_ball_bot_iff)
  have False when "n>m"
  proof -
    have "(h ---> 0) (at z within ball z r)"
    proof (rule Lim_transform_within[OF _ ‹r>0›, where f="λw. (w-z) powi (n - m) * g w"])
      have "∀w∈ball z r-{z}. h w = (w-z)powi(n-m) * g w"
        using ‹n>m› asm ‹r>0› by (simp add: field_simps power_int_diff) force
      then show "[x' ∈ ball z r; 0 < dist x' z;dist x' z < r]
            ==> (x' - z) powi (n - m) * g x' = h x'" for x' by auto
    next
      define F where "F ≡ at z within ball z r"
      define f' where "f' ≡ λx. (x - z) powi (n-m)"
      have "f' z=0" using ‹n>m› unfolding f'_def by auto
      moreover have "continuous F f'" unfolding f'_def F_def continuous_def
        using ‹n>m›
          by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
      ultimately have "(f' ---> 0) F" unfolding F_def
        by (simp add: continuous_within)
      moreover have "(g ---> g z) F"
        unfolding F_def
        using ‹r>0› centre_in_ball continuous_on_def g_holo holomorphic_on_imp_continuous_on by blast
      ultimately show " ((λw. f' w * g w) ---> 0) F" using tendsto_mult by fastforce
    qed
    moreover have "(h ---> h z) (at z within ball z r)"
      using holomorphic_on_imp_continuous_on[OF h_holo]
      by (auto simp add: continuous_on_def ‹r>0›)
    ultimately have "h z=0" by (auto intro!: tendsto_unique)
    thus False using ‹h z≠0› by auto
  qed
  moreover have False when "m>n"
  proof -
    have "(g ---> 0) (at z within ball z r)"
    proof (rule Lim_transform_within[OF _ ‹r>0›, where f="λw. (w-z) powi (m - n) * h w"])
      have "∀w∈ball z r -{z}. g w = (w-z) powi (m-n) * h w" using ‹m>n› asm
        by (simp add: field_simps power_int_diff) force
      then show "[x' ∈ ball z r; 0 < dist x' z;dist x' z < r]
            ==> (x' - z) powi (m - n) * h x' = g x'" for x' by auto
    next
      define F where "F ≡ at z within ball z r"
      define f' where "f' ≡λx. (x - z) powi (m-n)"
      have "f' z=0" using ‹m>n› unfolding f'_def by auto
      moreover have "continuous F f'" unfolding f'_def F_def continuous_def
        using ‹m>n›
        by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
      ultimately have "(f' ---> 0) F" unfolding F_def
        by (simp add: continuous_within)
      moreover have "(h ---> h z) F"
        using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] ‹r>0›
        unfolding F_def by auto
      ultimately show " ((λw. f' w * h w) ---> 0) F" using tendsto_mult by fastforce
    qed
    moreover have "(g ---> g z) (at z within ball z r)"
      using holomorphic_on_imp_continuous_on[OF g_holo]
      by (auto simp add: continuous_on_def ‹r>0›)
    ultimately have "g z=0" by (auto intro!: tendsto_unique)
    thus False using ‹g z≠0› by auto
  qed
  ultimately show "n=m" by fastforce
qed

lemma holomorphic_factor_puncture:
  assumes f_iso: "isolated_singularity_at f z"
      and "not_essential f z" 🍋 ‹🍋‹f› has either a removable singularity or a pole at ??‹z›\›
      and non_zero: "∃🪙Fw in (at z). f w≠0" 🍋 ‹🍋‹f› will not be constantly zero in a neighbour of 🍋‹z›\›
  shows "∃!n::int. ∃g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
          ∧ (∀w∈cball z r-{z}. f w = g w * (w-z) powi n ∧ g w≠0)"
proof -
  define P where "P = (λf n g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
          ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w≠0))"
  have imp_unique: "∃!n::int. ∃g r. P f n g r" when "∃n g r. P f n g r"
  proof (rule ex_ex1I[OF that])
    fix n1 n2 :: int
    assume g1_asm: "∃g1 r1. P f n1 g1 r1" and g2_asm: "∃g2 r2. P f n2 g2 r2"
    define fac where "fac ≡ λn g r. ∀w∈cball z r-{z}. f w = g w * (w-z) powi n ∧ g w ≠ 0"
    obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z≠0"
        and "fac n1 g1 r1" using g1_asm unfolding P_def fac_def by auto
    obtain g2 r2 where "0 < r2" and g2_holo: "g2 holomorphic_on cball z r2" and "g2 z≠0"
        and "fac n2 g2 r2" using g2_asm unfolding P_def fac_def by auto
    define r where "r ≡ min r1 r2"
    have "r>0" using ‹r1>0› ‹r2>0› unfolding r_def by auto
    moreover have "∀w∈ball z r-{z}. f w = g1 w * (w-z) powi n1 ∧ g1 w≠0
        ∧ f w = g2 w * (w-z) powi n2 ∧ g2 w≠0"
      using ‹fac n1 g1 r1› ‹fac n2 g2 r2›   unfolding fac_def r_def
      by fastforce
    ultimately show "n1=n2" 
      using g1_holo g2_holo ‹g1 z≠0› ‹g2 z≠0›
      apply (elim holomorphic_factor_unique)
      by (auto simp add: r_def)
  qed

  have P_exist: "∃ n g r. P h n g r" when
      "∃z'. (h ---> z') (at z)" "isolated_singularity_at h z"  "∃🪙Fw in (at z). h w≠0"
    for h
  proof -
    from that(2) obtain r where "r>0" and r: "h analytic_on ball z r - {z}"
      unfolding isolated_singularity_at_def by auto
    obtain z' where "(h ---> z') (at z)" using ‹∃z'. (h ---> z') (at z)› by auto
    define h' where "h'=(λx. if x=z then z' else h x)"
    have "h' holomorphic_on ball z r"
    proof (rule no_isolated_singularity'[of "{z}"])
      show "∧w. w ∈ {z} ==> (h' ---> h' w) (at w within ball z r)"
        by (simp add: LIM_cong Lim_at_imp_Lim_at_within ‹h ←-z→ z'› h'_def)
      show "h' holomorphic_on ball z r - {z}"
        using r analytic_imp_holomorphic h'_def holomorphic_transform by fastforce
    qed auto
    have ?thesis when "z'=0"
    proof -
      have "h' z=0" using that unfolding h'_def by auto
      moreover have "¬ h' constant_on ball z r"
        using ‹∃🪙Fw in (at z). h w≠0› unfolding constant_on_def frequently_def eventually_at h'_def
        by (metis ‹0 🚫› centre_in_ball dist_commute mem_ball that)
      moreover note ‹h' holomorphic_on ball z r›
      ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 ⊆ ball z r" and
          g: "g holomorphic_on ball z r1"
          "∧w. w ∈ ball z r1 ==> h' w = (w-z) ^ n * g w"
          "∧w. w ∈ ball z r1 ==> g w ≠ 0"
        using holomorphic_factor_zero_nonconstant[of _ "ball z r" z thesis,simplified,
                OF ‹h' holomorphic_on ball z r› ‹r>0› ‹h' z=0› ‹¬ h' constant_on ball z r›]
        by (auto simp add: dist_commute)
      define rr where "rr=r1/2"
      have "P h' n g rr"
        unfolding P_def rr_def
        using ‹n>0› ‹r1>0› g by (auto simp add: powr_nat)
      then have "P h n g rr"
        unfolding h'_def P_def by auto
      then show ?thesis unfolding P_def by blast
    qed
    moreover have ?thesis when "z'≠0"
    proof -
      have "h' z≠0" using that unfolding h'_def by auto
      obtain r1 where "r1>0" "cball z r1 ⊆ ball z r" "∀x∈cball z r1. h' x≠0"
      proof -
        have "isCont h' z" "h' z≠0"
          by (auto simp add: Lim_cong_within ‹h ←-z→ z'› ‹z'≠0› continuous_at h'_def)
        then obtain r2 where r2: "r2>0" "∀x∈ball z r2. h' x≠0"
          using continuous_at_avoid[of z h' 0 ] unfolding ball_def by auto
        define r1 where "r1=min r2 r / 2"
        have "0 < r1" "cball z r1 ⊆ ball z r"
          using ‹r2>0› ‹r>0› unfolding r1_def by auto
        moreover have "∀x∈cball z r1. h' x ≠ 0"
          using r2 unfolding r1_def by simp
        ultimately show ?thesis using that by auto
      qed
      then have "P h' 0 h' r1" using ‹h' holomorphic_on ball z r› unfolding P_def by auto
      then have "P h 0 h' r1" unfolding P_def h'_def by auto
      then show ?thesis unfolding P_def by blast
    qed
    ultimately show ?thesis by auto
  qed

  have ?thesis when "∃x. (f ---> x) (at z)"
    apply (rule_tac imp_unique[unfolded P_def])
    using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
  moreover have ?thesis when "is_pole f z"
  proof (rule imp_unique[unfolded P_def])
    obtain e where [simp]: "e>0" and e_holo: "f holomorphic_on ball z e - {z}" and e_nz: "∀x∈ball z e-{z}. f x≠0"
    proof -
      have "∀🪙F z in at z. f z ≠ 0"
        using ‹is_pole f z› filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def
        by auto
      then obtain e1 where e1: "e1>0" "∀x∈ball z e1-{z}. f x≠0"
        using that eventually_at[of "λx. f x≠0" z UNIV,simplified] by (auto simp add: dist_commute)
      obtain e2 where e2: "e2>0" "f holomorphic_on ball z e2 - {z}"
        using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto
      show ?thesis
        using e1 e2 by (force intro: that[of "min e1 e2"])
    qed

    define h where "h ≡ λx. inverse (f x)"
    have "∃n g r. P h n g r"
    proof -
      have "(λx. inverse (f x)) analytic_on ball z e - {z}"
        by (metis e_holo e_nz open_ball analytic_on_open holomorphic_on_inverse open_delete)
      moreover have "h ←-z→ 0"
        using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
      moreover have "∃🪙Fw in (at z). h w≠0"
        using non_zero by (simp add: h_def)
      ultimately show ?thesis
        using P_exist[of h] ‹e > 0›
        unfolding isolated_singularity_at_def h_def
        by blast
    qed
    then obtain n g r
      where "0 < r" and
            g_holo: "g holomorphic_on cball z r" and "g z≠0" and
            g_fac: "(∀w∈cball z r-{z}. h w = g w * (w-z) powi n ∧ g w ≠ 0)"
      unfolding P_def by auto
    have "P f (-n) (inverse o g) r"
    proof -
      have "f w = inverse (g w) * (w-z) powi (- n)" when "w∈cball z r - {z}" for w
        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib power_int_minus that)
      then show ?thesis
        unfolding P_def comp_def
        using ‹r>0› g_holo g_fac ‹g z≠0› by (auto intro: holomorphic_intros)
    qed
    then show "∃x g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z ≠ 0
                  ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi x ∧ g w ≠ 0)"
      unfolding P_def by blast
  qed
  ultimately show ?thesis 
    using ‹not_essential f z› unfolding not_essential_def by presburger
qed

lemma not_essential_transform:
  assumes "not_essential g z"
  assumes "∀🪙F w in (at z). g w = f w"
  shows "not_essential f z"
  using assms unfolding not_essential_def
  by (simp add: filterlim_cong is_pole_cong)

lemma isolated_singularity_at_transform:
  assumes "isolated_singularity_at g z"
  assumes "∀🪙F w in (at z). g w = f w"
  shows "isolated_singularity_at f z"
  using assms isolated_singularity_at_cong by blast

lemma not_essential_powr[singularity_intros]:
  assumes "LIM w (at z). f w :> (at x)"
  shows "not_essential (λw. (f w) powi n) z"
proof -
  define fp where "fp=(λw. (f w) powi n)"
  have ?thesis when "n>0"
  proof -
    have "(λw. (f w) ^ (nat n)) ←-z→ x ^ nat n"
      using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    then have "fp ←-z→ x ^ nat n" unfolding fp_def
      by (smt (verit) LIM_cong power_int_def that)
    then show ?thesis unfolding not_essential_def fp_def by auto
  qed
  moreover have ?thesis when "n=0"
  proof -
    have "∀🪙F x in at z. fp x = 1"
      using that filterlim_at_within_not_equal[OF assms] by (auto simp: fp_def)
    then have "fp ←-z→ 1"
      by (simp add: tendsto_eventually)
    then show ?thesis unfolding fp_def not_essential_def by auto
  qed
  moreover have ?thesis when "n<0"
  proof (cases "x=0")
    case True
    have "(λx. f x ^ nat (- n)) ←-z→ 0"
      using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    moreover have "∀🪙F x in at z. f x ^ nat (- n) ≠ 0"
      by (smt (verit) True assms eventually_at_topological filterlim_at power_eq_0_iff)
    ultimately have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
      by (metis filterlim_atI filterlim_compose filterlim_inverse_at_infinity)
    then have "LIM w (at z). fp w :> at_infinity"
    proof (elim filterlim_mono_eventually)
      show "∀🪙F x in at z. inverse (f x ^ nat (- n)) = fp x"
        using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
        by (smt (verit) eventuallyI power_int_def power_inverse that)
    qed auto
    then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
  next
    case False
    let ?xx= "inverse (x ^ (nat (-n)))"
    have "(λw. inverse ((f w) ^ (nat (-n)))) ←-z→?xx"
      using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    then have "fp ←-z→ ?xx"
      by (smt (verit, best) LIM_cong fp_def power_int_def power_inverse that)
    then show ?thesis unfolding fp_def not_essential_def by auto
  qed
  ultimately show ?thesis by linarith
qed

lemma isolated_singularity_at_powr[singularity_intros]:
  assumes "isolated_singularity_at f z" "∀🪙F w in (at z). f w≠0"
  shows "isolated_singularity_at (λw. (f w) powi n) z"
proof -
  obtain r1 where "r1>0" "f analytic_on ball z r1 - {z}"
    using assms(1) unfolding isolated_singularity_at_def by auto
  then have r1: "f holomorphic_on ball z r1 - {z}"
    using analytic_on_open[of "ball z r1-{z}" f] by blast
  obtain r2 where "r2>0" and r2: "∀w. w ≠ z ∧ dist w z < r2 ⟶ f w ≠ 0"
    using assms(2) unfolding eventually_at by auto
  define r3 where "r3=min r1 r2"
  have "(λw. (f w) powi n) holomorphic_on ball z r3 - {z}"
    by (intro holomorphic_on_power_int) (use r1 r2 in ‹auto simp: dist_commute r3_def›)
  moreover have "r3>0" unfolding r3_def using ‹0 🚫› ‹0 🚫› by linarith
  ultimately show ?thesis
    by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
qed

lemma non_zero_neighbour:
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "∃🪙Fw in (at z). f w≠0"
    shows "∀🪙F w in (at z). f w≠0"
proof -
  obtain fn fp fr
    where [simp]: "fp z ≠ 0" and "fr > 0"
      and fr: "fp holomorphic_on cball z fr"
              "∧w. w ∈ cball z fr - {z} ==> f w = fp w * (w-z) powi fn ∧ fp w ≠ 0"
    using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
  have "f w ≠ 0" when " w ≠ z" "dist w z < fr" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w ≠ 0"
      using fr that by (auto simp add: dist_commute)
    moreover have "(w-z) powi fn ≠0"
      unfolding powr_eq_0_iff using ‹w≠z› by auto
    ultimately show ?thesis by auto
  qed
  then show ?thesis using ‹fr>0› unfolding eventually_at by auto
qed

lemma non_zero_neighbour_pole:
  assumes "is_pole f z"
  shows "∀🪙F w in (at z). f w≠0"
  using assms filterlim_at_infinity_imp_eventually_ne[of f "at z" 0]
  unfolding is_pole_def by auto

lemma non_zero_neighbour_alt:
  assumes holo: "f holomorphic_on S"
      and "open S" "connected S" "z ∈ S"  "β ∈ S" "f β ≠ 0"
    shows "∀🪙F w in (at z). f w≠0 ∧ w∈S"
proof (cases "f z = 0")
  case True
  from isolated_zeros[OF holo ‹open S› ‹connected S› ‹z ∈ S› True ‹β ∈ S› ‹f β ≠ 0›]
  obtain r where "0 < r" "ball z r ⊆ S" "∀w ∈ ball z r - {z}.f w ≠ 0" by metis
  then show ?thesis
    by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
next
  case False
  obtain r1 where r1: "r1>0" "∀y. dist z y < r1 ⟶ f y ≠ 0"
    using continuous_at_avoid[of z f, OF _ False] assms continuous_on_eq_continuous_at
      holo holomorphic_on_imp_continuous_on by blast
  obtain r2 where r2: "r2>0" "ball z r2 ⊆ S"
    using assms openE by blast
  show ?thesis unfolding eventually_at
    by (metis (no_types) dist_commute order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
qed

lemma not_essential_times[singularity_intros]:
  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 -
  define fg where "fg = (λw. f w * g w)"
  have ?thesis when "¬ ((∃🪙Fw in (at z). f w≠0) ∧ (∃🪙Fw in (at z). g w≠0))"
  proof -
    have "∀🪙Fw in (at z). fg w=0"
      using fg_def frequently_elim1 not_eventually that by fastforce
    from tendsto_cong[OF this] have "fg ←-z→0" by auto
    then show ?thesis unfolding not_essential_def fg_def by auto
  qed
  moreover have ?thesis when f_nconst: "∃🪙Fw in (at z). f w≠0" and g_nconst: "∃🪙Fw in (at z). g w≠0"
  proof -
    obtain fn fp fr where [simp]: "fp z ≠ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "∀w∈cball z fr - {z}. f w = fp w * (w-z) powi fn ∧ fp w ≠ 0"
      using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
    obtain gn gp gr where [simp]: "gp z ≠ 0" and "gr > 0"
          and gr: "gp holomorphic_on cball z gr"
                  "∀w∈cball z gr - {z}. g w = gp w * (w-z) powi gn ∧ gp w ≠ 0"
      using holomorphic_factor_puncture[OF g_iso g_ness g_nconst] by auto

    define r1 where "r1=(min fr gr)"
    have "r1>0" unfolding r1_def using  ‹fr>0› ‹gr>0› by auto
    have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w≠0"
      when "w∈ball z r1 - {z}" for w
    proof -
      have "f w = fp w * (w-z) powi fn" "fp w≠0"
        using fr that unfolding r1_def by auto
      moreover have "g w = gp w * (w-z) powi gn" "gp w ≠ 0"
        using gr that unfolding r1_def by auto
      ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w≠0"
        using that by (auto simp add: fg_def power_int_add)
    qed

    obtain [intro]: "fp ←-z→fp z" "gp ←-z→gp z"
        using fr(1) ‹fr>0› gr(1) ‹gr>0›
        by (metis centre_in_ball continuous_at continuous_on_interior
            holomorphic_on_imp_continuous_on interior_cball)
    have ?thesis when "fn+gn>0"
    proof -
      have "(λw. (fp w * gp w) * (w-z) ^ (nat (fn+gn))) ←-z→0"
        using that by (auto intro!:tendsto_eq_intros)
      then have "fg ←-z→ 0"
        using Lim_transform_within[OF _ ‹r1>0›]
        by (smt (verit, best) Diff_iff dist_commute fg_times mem_ball power_int_def singletonD that zero_less_dist_iff)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    moreover have ?thesis when "fn+gn=0"
    proof -
      have "(λw. fp w * gp w) ←-z→fp z*gp z"
        using that by (auto intro!:tendsto_eq_intros)
      then have "fg ←-z→ fp z*gp z"
        apply (elim Lim_transform_within[OF _ ‹r1>0›])
        apply (subst fg_times)
        by (auto simp add: dist_commute that)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    moreover have ?thesis when "fn+gn<0"
    proof -
      have "LIM x at z. (x - z) ^ nat (- (fn + gn)) :> at 0"
        using eventually_at_topological that
        by (force intro!: tendsto_eq_intros filterlim_atI)
      moreover have "∃c. (λc. fp c * gp c) ←-z→ c ∧ 0 ≠ c"
        using ‹fp ←-z→ fp z› ‹gp ←-z→ gp z› tendsto_mult by fastforce
      ultimately have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
        using filterlim_divide_at_infinity by blast
      then have "is_pole fg z" unfolding is_pole_def
        apply (elim filterlim_transform_within[OF _ _ ‹r1>0›])
        using that
        by (simp_all add: dist_commute fg_times of_int_of_nat divide_simps power_int_def del: minus_add_distrib)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    ultimately show ?thesis unfolding not_essential_def fg_def by fastforce
  qed
  ultimately show ?thesis by auto
qed

lemma not_essential_inverse[singularity_intros]:
  assumes f_ness: "not_essential f z"
  assumes f_iso: "isolated_singularity_at f z"
  shows "not_essential (λw. inverse (f w)) z"
proof -
  define vf where "vf = (λw. inverse (f w))"
  have ?thesis when "¬(∃🪙Fw in (at z). f w≠0)"
  proof -
    have "∀🪙Fw in (at z). f w=0"
      using not_eventually that by fastforce
    then have "vf ←-z→0" 
      unfolding vf_def by (simp add: tendsto_eventually)
    then show ?thesis 
      unfolding not_essential_def vf_def by auto
  qed
  moreover have ?thesis when "is_pole f z"
    by (metis (mono_tags, lifting) filterlim_at filterlim_inverse_at_iff is_pole_def
        not_essential_def that)
  moreover have ?thesis when "∃x. f←-z→x " and f_nconst: "∃🪙Fw in (at z). f w≠0"
  proof -
    from that obtain fz where fz: "f←-z→fz" by auto
    have ?thesis when "fz=0"

    proof -
      have "(λw. inverse (vf w)) ←-z→0"
        using fz that unfolding vf_def by auto
      moreover have "∀🪙F w in at z. inverse (vf w) ≠ 0"
        using non_zero_neighbour[OF f_iso f_ness f_nconst]
        unfolding vf_def by auto
      ultimately show ?thesis unfolding not_essential_def vf_def
         using filterlim_atI filterlim_inverse_at_iff is_pole_def by blast
    qed
    moreover have ?thesis when "fz≠0"
      using fz not_essential_def tendsto_inverse that by blast
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis using f_ness unfolding not_essential_def by auto
qed

lemma isolated_singularity_at_inverse[singularity_intros]:
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
  shows "isolated_singularity_at (λw. inverse (f w)) z"
proof -
  define vf where "vf = (λw. inverse (f w))"
  have ?thesis when "¬(∃🪙Fw in (at z). f w≠0)"
  proof -
    have "∀🪙Fw in (at z). f w=0"
      using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
    then have "∀🪙Fw in (at z). vf w=0"
      unfolding vf_def by auto
    then obtain d1 where "d1>0" and d1: "∀x. x ≠ z ∧ dist x z < d1 ⟶ vf x = 0"
      unfolding eventually_at by auto
    then have "vf holomorphic_on ball z d1-{z}"
      using holomorphic_transform[of "λ_. 0"]
      by (metis Diff_iff dist_commute holomorphic_on_const insert_iff mem_ball)
    then have "vf analytic_on ball z d1 - {z}"
      by (simp add: analytic_on_open open_delete)
    then show ?thesis 
      using ‹d1>0› unfolding isolated_singularity_at_def vf_def by auto
  qed
  moreover have ?thesis when f_nconst: "∃🪙Fw in (at z). f w≠0"
  proof -
    have "∀🪙F w in at z. f w ≠ 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] .
    then obtain d1 where d1: "d1>0" "∀x. x ≠ z ∧ dist x z < d1 ⟶ f x ≠ 0"
      unfolding eventually_at by auto
    obtain d2 where "d2>0" and d2: "f analytic_on ball z d2 - {z}"
      using f_iso unfolding isolated_singularity_at_def by auto
    define d3 where "d3=min d1 d2"
    have "d3>0" unfolding d3_def using ‹d1>0› ‹d2>0› by auto
    moreover
    have "f analytic_on ball z d3 - {z}"
      by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
    then have "vf analytic_on ball z d3 - {z}"
      unfolding vf_def
      by (intro analytic_on_inverse; simp add: d1(2) d3_def dist_commute)
    ultimately show ?thesis 
      unfolding isolated_singularity_at_def vf_def by auto
  qed
  ultimately show ?thesis by auto
qed

lemma not_essential_divide[singularity_intros]:
  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 "not_essential (λw. f w * inverse (g w)) z"
    by (simp add: f_iso f_ness g_iso g_ness isolated_singularity_at_inverse
        not_essential_inverse not_essential_times)
  then show ?thesis by (simp add: field_simps)
qed

lemma
  assumes f_iso: "isolated_singularity_at f z"
      and g_iso: "isolated_singularity_at g z"
    shows isolated_singularity_at_times[singularity_intros]:
              "isolated_singularity_at (λw. f w * g w) z"
      and isolated_singularity_at_add[singularity_intros]:
              "isolated_singularity_at (λw. f w + g w) z"
proof -
  obtain d1 d2 where "d1>0" "d2>0"
      and d1: "f analytic_on ball z d1 - {z}" and d2: "g analytic_on ball z d2 - {z}"
    using f_iso g_iso unfolding isolated_singularity_at_def by auto
  define d3 where "d3=min d1 d2"
  have "d3>0" unfolding d3_def using ‹d1>0› ‹d2>0› by auto

  have fan: "f analytic_on ball z d3 - {z}"
    by (smt (verit, best) Diff_iff analytic_on_analytic_at d1 d3_def mem_ball)
  have gan: "g analytic_on ball z d3 - {z}"
    by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
  have "(λw. f w * g w) analytic_on ball z d3 - {z}"
    using analytic_on_mult fan gan by blast
  then show "isolated_singularity_at (λw. f w * g w) z"
    using ‹d3>0› unfolding isolated_singularity_at_def by auto
  have "(λw. f w + g w) analytic_on ball z d3 - {z}"
    using analytic_on_add fan gan by blast
  then show "isolated_singularity_at (λw. f w + g w) z"
    using ‹d3>0› unfolding isolated_singularity_at_def by auto
qed

lemma isolated_singularity_at_uminus[singularity_intros]:
  assumes f_iso: "isolated_singularity_at f z"
  shows "isolated_singularity_at (λw. - f w) z"
  using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast

lemma isolated_singularity_at_id[singularity_intros]:
     "isolated_singularity_at (λw. w) z"
  unfolding isolated_singularity_at_def by (simp add: gt_ex)

lemma isolated_singularity_at_minus[singularity_intros]:
  assumes "isolated_singularity_at f z" and "isolated_singularity_at g z"
  shows "isolated_singularity_at (λw. f w - g w) z"
  unfolding diff_conv_add_uminus
  using assms isolated_singularity_at_add isolated_singularity_at_uminus by blast

lemma isolated_singularity_at_divide[singularity_intros]:
  assumes "isolated_singularity_at f z"
      and "isolated_singularity_at g z"
      and "not_essential g z"
    shows "isolated_singularity_at (λw. f w / g w) z"
  unfolding divide_inverse
  by (simp add: assms isolated_singularity_at_inverse isolated_singularity_at_times)

lemma isolated_singularity_at_const[singularity_intros]:
    "isolated_singularity_at (λw. c) z"
  unfolding isolated_singularity_at_def by (simp add: gt_ex)

lemma isolated_singularity_at_holomorphic:
  assumes "f holomorphic_on s-{z}" "open s" "z∈s"
  shows "isolated_singularity_at f z"
  using assms unfolding isolated_singularity_at_def
  by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)

lemma isolated_singularity_at_altdef:
  "isolated_singularity_at f z ⟷ eventually (λz. f analytic_on {z}) (at z)"
proof
  assume "isolated_singularity_at f z"
  then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
    unfolding isolated_singularity_at_def by blast
  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r(1) by (intro eventually_at_in_open) auto
  thus "eventually (λz. f analytic_on {z}) (at z)"
    by eventually_elim (use r analytic_on_subset in auto)
next
  assume "eventually (λz. f analytic_on {z}) (at z)"
  then obtain A where A: "open A" "z ∈ A" "∧w. w ∈ A - {z} ==> f analytic_on {w}"
    unfolding eventually_at_topological by blast
  then show "isolated_singularity_at f z"
    by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic)
qed

lemma isolated_singularity_at_shift:
  assumes "isolated_singularity_at (λx. f (x + w)) z"
  shows   "isolated_singularity_at f (z + w)"
proof -
  from assms obtain r where r: "r > 0" and ana: "(λx. f (x + w)) analytic_on ball z r - {z}"
    unfolding isolated_singularity_at_def by blast
  have "((λx. f (x + w)) ∘ (λx. x - w)) analytic_on (ball (z + w) r - {z + w})"
    by (rule analytic_on_compose_gen[OF _ ana])
       (auto simp: dist_norm algebra_simps intro!: analytic_intros)
  hence "f analytic_on (ball (z + w) r - {z + w})"
    by (simp add: o_def)
  thus ?thesis using r
    unfolding isolated_singularity_at_def by blast
qed

lemma isolated_singularity_at_shift_iff:
  "isolated_singularity_at f (z + w) ⟷ isolated_singularity_at (λx. f (x + w)) z"
  using isolated_singularity_at_shift[of f w z]
        isolated_singularity_at_shift[of "λx. f (x + w)" "-w" "w + z"]
  by (auto simp: algebra_simps)

lemma isolated_singularity_at_shift_0:
  "NO_MATCH 0 z ==> isolated_singularity_at f z ⟷ isolated_singularity_at (λx. f (z + x)) 0"
  using isolated_singularity_at_shift_iff[of f 0 z] by (simp add: add_ac)

lemma not_essential_shift:
  assumes "not_essential (λx. f (x + w)) z"
  shows   "not_essential f (z + w)"
proof -
  from assms consider c where "(λx. f (x + w)) ←-z→ c" | "is_pole (λx. f (x + w)) z"
    unfolding not_essential_def by blast
  thus ?thesis
  proof cases
    case (1 c)
    hence "f ←-z + w→ c"
      by (smt (verit, ccfv_SIG) LIM_cong add.assoc filterlim_at_to_0)
    thus ?thesis
      by (auto simp: not_essential_def)
  next
    case 2
    hence "is_pole f (z + w)"
      by (subst is_pole_shift_iff [symmetric]) (auto simp: o_def add_ac)
    thus ?thesis
      by (auto simp: not_essential_def)
  qed
qed

lemma not_essential_shift_iff: "not_essential f (z + w) ⟷ not_essential (λx. f (x + w)) z"
  using not_essential_shift[of f w z]
        not_essential_shift[of "λx. f (x + w)" "-w" "w + z"]
  by (auto simp: algebra_simps)

lemma not_essential_shift_0:
  "NO_MATCH 0 z ==> not_essential f z ⟷ not_essential (λx. f (z + x)) 0"
  using not_essential_shift_iff[of f 0 z] by (simp add: add_ac)

lemma not_essential_holomorphic:
  assumes "f holomorphic_on A" "x ∈ A" "open A"
  shows   "not_essential f x"
  by (metis assms at_within_open continuous_on holomorphic_on_imp_continuous_on not_essential_def)

lemma not_essential_analytic:
  assumes "f analytic_on {z}"
  shows   "not_essential f z"
  using analytic_at assms not_essential_holomorphic by blast

lemma not_essential_id [singularity_intros]: "not_essential (λw. w) z"
  by (simp add: not_essential_analytic)

lemma is_pole_imp_not_essential [intro]: "is_pole f z ==> not_essential f z"
  by (auto simp: not_essential_def)

lemma tendsto_imp_not_essential [intro]: "f ←-z→ c ==> not_essential f z"
  by (auto simp: not_essential_def)

lemma eventually_not_pole:
  assumes "isolated_singularity_at f z"
  shows   "eventually (λw. ¬is_pole f w) (at z)"
proof -
  from assms obtain r where "r > 0" and r: "f analytic_on ball z r - {z}"
    by (auto simp: isolated_singularity_at_def)
  then have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    by (intro eventually_at_in_open) auto
  thus "eventually (λw. ¬is_pole f w) (at z)"
    by (metis (no_types, lifting) analytic_at analytic_on_analytic_at eventually_mono not_is_pole_holomorphic r)
qed

lemma not_islimpt_poles:
  assumes "isolated_singularity_at f z"
  shows   "¬z islimpt {w. is_pole f w}"
  using eventually_not_pole [OF assms]
  by (auto simp: islimpt_conv_frequently_at frequently_def)

lemma analytic_at_imp_no_pole: "f analytic_on {z} ==> ¬is_pole f z"
  using analytic_at not_is_pole_holomorphic by blast

lemma not_essential_const [singularity_intros]: "not_essential (λ_. c) z"
  by blast

lemma not_essential_uminus [singularity_intros]:
  assumes f_ness: "not_essential f z"
  assumes f_iso: "isolated_singularity_at f z"
  shows "not_essential (λw. -f w) z"
proof -
  have "not_essential (λw. -1 * f w) z"
    by (intro assms singularity_intros)
  thus ?thesis by simp
qed

lemma isolated_singularity_at_analytic:
  assumes "f analytic_on {z}"
  shows   "isolated_singularity_at f z"
  by (meson Diff_subset analytic_at assms holomorphic_on_subset isolated_singularity_at_holomorphic)

lemma isolated_singularity_sum [singularity_intros]:
  assumes "∧x. x ∈ A ==> isolated_singularity_at (f x) z"
  shows   "isolated_singularity_at (λw. ∑x∈A. f x w) z"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)

lemma isolated_singularity_prod [singularity_intros]:
  assumes "∧x. x ∈ A ==> isolated_singularity_at (f x) z"
  shows   "isolated_singularity_at (λw. ∏x∈A. f x w) z"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)

lemma isolated_singularity_sum_list [singularity_intros]:
  assumes "∧f. f ∈ set fs ==> isolated_singularity_at f z"
  shows   "isolated_singularity_at (λw. ∑f←fs. f w) z"
  using assms by (induction fs) (auto intro!: singularity_intros)

lemma isolated_singularity_prod_list [singularity_intros]:
  assumes "∧f. f ∈ set fs ==> isolated_singularity_at f z"
  shows   "isolated_singularity_at (λw. ∏f←fs. f w) z"
  using assms by (induction fs) (auto intro!: singularity_intros)

lemma isolated_singularity_sum_mset [singularity_intros]:
  assumes "∧f. f ∈# F ==> isolated_singularity_at f z"
  shows   "isolated_singularity_at (λw. ∑f∈#F. f w) z"
  using assms by (induction F) (auto intro!: singularity_intros)

lemma isolated_singularity_prod_mset [singularity_intros]:
  assumes "∧f. f ∈# F ==> isolated_singularity_at f z"
  shows   "isolated_singularity_at (λw. ∏f∈#F. f w) z"
  using assms by (induction F) (auto intro!: singularity_intros)

lemma analytic_nhd_imp_isolated_singularity:
  assumes "f analytic_on A - {x}" "x ∈ A" "open A"
  shows   "isolated_singularity_at f x"
  unfolding isolated_singularity_at_def using assms
  using analytic_imp_holomorphic isolated_singularity_at_def isolated_singularity_at_holomorphic by blast

lemma isolated_singularity_at_iff_analytic_nhd:
  "isolated_singularity_at f x ⟷ (∃A. x ∈ A ∧ open A ∧ f analytic_on A - {x})"
  by (meson open_ball analytic_nhd_imp_isolated_singularity
            centre_in_ball isolated_singularity_at_def)

subsection ‹The order of non-essential singularities (i.e. removable singularities or poles)›

definition🍋‹tag important› zorder :: "(complex ==> complex) ==> complex ==> int" where
  "zorder f z = (THE n. (∃h r. r>0 ∧ h holomorphic_on cball z r ∧ h z≠0
                   ∧ (∀w∈cball z r - {z}. f w = h w * (w-z) powi n
                   ∧ h w ≠0)))"

definition🍋‹tag important› zor_poly
    :: "[complex ==> complex, complex] ==> complex ==> complex" where
  "zor_poly f z = (SOME h. ∃r. r > 0 ∧ h holomorphic_on cball z r ∧ h z ≠ 0
                   ∧ (∀w∈cball z r - {z}. f w = h w * (w-z) powi (zorder f z)
                   ∧ h w ≠0))"

lemma zorder_exist:
  fixes f:: "complex ==> complex" and z::complex
  defines "n ≡ zorder f z" and "g ≡ zor_poly f z"
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "∃🪙Fw in (at z). f w≠0"
  shows "g z≠0 ∧ (∃r. r>0 ∧ g holomorphic_on cball z r
    ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w ≠0))"
proof -
  define P where "P = (λn g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
          ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w≠0))"
  have "∃!k. ∃g r. P k g r"
    using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
  then have "∃g r. P n g r"
    unfolding n_def P_def zorder_def by (rule theI')
  then have "∃r. P n g r"
    unfolding P_def zor_poly_def g_def n_def by (rule someI_ex)
  then obtain r1 where "P n g r1" 
    by auto
  then show ?thesis 
    unfolding P_def by auto
qed

lemma zorder_shift:
  shows  "zorder f z = zorder (λu. f (u + z)) 0"
  unfolding zorder_def
  apply (rule arg_cong [of concl: The])
  apply (auto simp: fun_eq_iff Ball_def dist_norm)
  subgoal for x h r
    apply (rule_tac x="h o (+)z" in exI)
    apply (rule_tac x="r" in exI)
    apply (intro conjI holomorphic_on_compose holomorphic_intros)
       apply (simp_all flip: cball_translation)
    apply (simp add: add.commute)
    done
  subgoal for x h r
    apply (rule_tac x="h o (λu. u-z)" in exI)
    apply (rule_tac x="r" in exI)
    apply (intro conjI holomorphic_on_compose holomorphic_intros)
       apply (simp_all flip: cball_translation_subtract)
    by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
  done

lemma zorder_shift': "NO_MATCH 0 z ==> zorder f z = zorder (λu. f (u + z)) 0"
  by (rule zorder_shift)

lemma
  fixes f:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "∃🪙Fw in (at z). f w≠0"
    shows zorder_inverse: "zorder (λw. inverse (f w)) z = - zorder f z"
      and zor_poly_inverse: "∀🪙Fw in (at z). zor_poly (λw. inverse (f w)) z w
                                                = inverse (zor_poly f z w)"
proof -
  define vf where "vf = (λw. inverse (f w))"
  define fn vfn where
    "fn = zorder f z"  and "vfn = zorder vf z"
  define fp vfp where
    "fp = zor_poly f z" and "vfp = zor_poly vf z"

  obtain fr where [simp]: "fp z ≠ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "∀w∈cball z fr - {z}. f w = fp w * (w-z) powi fn ∧ fp w ≠ 0"
    using zorder_exist[OF f_iso f_ness f_nconst,folded fn_def fp_def]
    by auto
  have fr_inverse: "vf w = (inverse (fp w)) * (w-z) powi (-fn)"
        and fr_nz: "inverse (fp w) ≠ 0"
    when "w∈ball z fr - {z}" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w ≠ 0"
      using fr(2) that by auto
    then show "vf w = (inverse (fp w)) * (w-z) powi (-fn)" "inverse (fp w)≠0"
      by (simp_all add: power_int_minus vf_def)
  qed
  obtain vfr where [simp]: "vfp z ≠ 0" and "vfr>0" and vfr: "vfp holomorphic_on cball z vfr"
      "(∀w∈cball z vfr - {z}. vf w = vfp w * (w-z) powi vfn ∧ vfp w ≠ 0)"
  proof -
    have "isolated_singularity_at vf z"
      using isolated_singularity_at_inverse[OF f_iso f_ness] unfolding vf_def .
    moreover have "not_essential vf z"
      using not_essential_inverse[OF f_ness f_iso] unfolding vf_def .
    moreover have "∃🪙F w in at z. vf w ≠ 0"
      using f_nconst unfolding vf_def by (auto elim: frequently_elim1)
    ultimately show ?thesis using zorder_exist[of vf z, folded vfn_def vfp_def] that by auto
  qed

  define r1 where "r1 = min fr vfr"
  have "r1>0" using ‹fr>0› ‹vfr>0› unfolding r1_def by simp
  show "vfn = - fn"
  proof (rule holomorphic_factor_unique)
    have 🍋: "∧w. [fp w = 0; dist z w < fr] ==> False"
      using fr_nz by force
    then show "∀w∈ball z r1 - {z}.
               vf w = vfp w * (w-z) powi vfn ∧
               vfp w ≠ 0 ∧ vf w = inverse (fp w) * (w-z) powi (- fn) ∧
               inverse (fp w) ≠ 0"
      using fr_inverse r1_def vfr(2)
      by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball)
    show "vfp holomorphic_on ball z r1"
      using r1_def vfr(1) by auto
    show "(λw. inverse (fp w)) holomorphic_on ball z r1"
      by (metis 🍋 ball_subset_cball fr(1) holomorphic_on_inverse holomorphic_on_subset mem_ball min.cobounded2 min.commute r1_def subset_ball)
  qed (use ‹r1>0› in auto)
  have "vfp w = inverse (fp w)" when "w∈ball z r1-{z}" for w
  proof -
    have "w ∈ ball z fr - {z}" "w ∈ cball z vfr - {z}"  "w≠z"
      using that unfolding r1_def by auto
    then show ?thesis
      by (metis ‹vfn = - fn› power_int_not_zero right_minus_eq  fr_inverse vfr(2)
          vector_space_over_itself.scale_right_imp_eq) 
  qed
  then show "∀🪙Fw in (at z). vfp w = inverse (fp w)"
    unfolding eventually_at by (metis DiffI dist_commute mem_ball singletonD ‹r1>0›)
qed

lemma zor_poly_shift:
  assumes iso1: "isolated_singularity_at f z"
    and ness1: "not_essential f z"
    and nzero1: "∃🪙F w in at z. f w ≠ 0"
  shows "∀🪙F w in nhds z. zor_poly f z w = zor_poly (λu. f (z + u)) 0 (w-z)"
proof -
  obtain r1 where "r1>0" "zor_poly f z z ≠ 0" and
      holo1: "zor_poly f z holomorphic_on cball z r1" and
      rball1: "∀w∈cball z r1 - {z}.
           f w = zor_poly f z w * (w-z) powi (zorder f z) ∧
           zor_poly f z w ≠ 0"
    using zorder_exist[OF iso1 ness1 nzero1] by blast

  define ff where "ff=(λu. f (z + u))"
  have "isolated_singularity_at ff 0"
    unfolding ff_def
    using iso1 isolated_singularity_at_shift_iff[of f 0 z]
    by (simp add: algebra_simps)
  moreover have "not_essential ff 0"
    unfolding ff_def
    using ness1 not_essential_shift_iff[of f 0 z]
    by (simp add: algebra_simps)
  moreover have "∃🪙F w in at 0. ff w ≠ 0"
    unfolding ff_def using nzero1
    by (smt (verit, ccfv_SIG) add.commute eventually_at_to_0
        eventually_mono not_frequently)
  ultimately 
  obtain r2 where "r2>0" "zor_poly ff 0 0 ≠ 0"
          and holo2: "zor_poly ff 0 holomorphic_on cball 0 r2" 
          and rball2: "∀w∈cball 0 r2 - {0}.
               ff w = zor_poly ff 0 w * w powi (zorder ff 0) ∧ zor_poly ff 0 w ≠ 0"
    using zorder_exist[of ff 0] by auto

  define r where "r=min r1 r2"
  have "r>0" using ‹r1>0› ‹r2>0› unfolding r_def by auto

  have "zor_poly f z w = zor_poly ff 0 (w-z)"
    if "w∈ball z r - {z}" for w
  proof -
    define n where "n ≡ zorder f z"

    have "f w = zor_poly f z w * (w-z) powi n"
      using n_def r_def rball1 that by auto
    moreover have "f w = zor_poly ff 0 (w-z) * (w-z) powi n"
    proof -
      have "w-z∈cball 0 r2 - {0}"
        using r_def that by (auto simp: dist_complex_def)
      then have "ff (w-z) = zor_poly ff 0 (w-z) * (w-z) powi (zorder ff 0)"
        using rball2 by blast
      moreover have "of_int (zorder ff 0) = n"
        unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
      ultimately show ?thesis unfolding ff_def by auto
    qed
    ultimately have "zor_poly f z w * (w-z) powi n = zor_poly ff 0 (w-z) * (w-z) powi n"
      by auto
    moreover have "(w-z) powi n ≠0"
      using that by auto
    ultimately show ?thesis
      using mult_cancel_right by blast
  qed
  then have "∀🪙F w in at z. zor_poly f z w = zor_poly ff 0 (w-z)"
    unfolding eventually_at
    by (metis DiffI ‹0 🚫› dist_commute mem_ball singletonD)
  moreover have "isCont (zor_poly f z) z"
    using holo1[THEN holomorphic_on_imp_continuous_on]
    by (simp add: ‹0 🚫› continuous_on_interior)
  moreover 
  have "isCont (zor_poly ff 0) 0"
    using ‹0 🚫› continuous_on_interior holo2 holomorphic_on_imp_continuous_on
    by fastforce
  then have "isCont (λw. zor_poly ff 0 (w-z)) z"
      unfolding isCont_iff by simp
  ultimately show "∀🪙F w in nhds z. zor_poly f z w = zor_poly ff 0 (w-z)"
    by (elim at_within_isCont_imp_nhds;auto)
qed

lemma
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
      and f_ness: "not_essential f z" and g_ness: "not_essential g z"
      and fg_nconst: "∃🪙Fw in (at z). f w * g w≠ 0"
  shows zorder_times: "zorder (λw. f w * g w) z = zorder f z + zorder g z" and
        zor_poly_times: "∀🪙Fw in (at z). zor_poly (λw. f w * g w) z w
                                                  = zor_poly f z w *zor_poly g z w"
proof -
  define fg where "fg = (λw. f w * g w)"
  define fn gn fgn where
    "fn = zorder f z" and "gn = zorder g z" and "fgn = zorder fg z"
  define fp gp fgp where
    "fp = zor_poly f z" and "gp = zor_poly g z" and "fgp = zor_poly fg z"
  have f_nconst: "∃🪙Fw in (at z). f w ≠ 0" and g_nconst: "∃🪙Fw in (at z).g w≠ 0"
    using fg_nconst by (auto elim!:frequently_elim1)
  obtain fr where [simp]: "fp z ≠ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "∀w∈cball z fr - {z}. f w = fp w * (w-z) powi fn ∧ fp w ≠ 0"
    using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto
  obtain gr where [simp]: "gp z ≠ 0" and "gr > 0"
          and gr: "gp holomorphic_on cball z gr"
                  "∀w∈cball z gr - {z}. g w = gp w * (w-z) powi gn ∧ gp w ≠ 0"
    using zorder_exist[OF g_iso g_ness g_nconst,folded gn_def gp_def] by auto
  define r1 where "r1=min fr gr"
  have "r1>0" unfolding r1_def using ‹fr>0› ‹gr>0› by auto
  have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w≠0"
    when "w∈ball z r1 - {z}" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w ≠ 0"
      using fr(2) r1_def that by auto
    moreover have "g w = gp w * (w-z) powi gn" "gp w ≠ 0"
      using gr(2) that unfolding r1_def by auto
    ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w≠0"
      using that unfolding fg_def by (auto simp add: power_int_add)
  qed

  obtain fgr where [simp]: "fgp z ≠ 0" and "fgr > 0"
          and fgr: "fgp holomorphic_on cball z fgr"
                   "∀w∈cball z fgr - {z}. fg w = fgp w * (w-z) powi fgn ∧ fgp w ≠ 0"
  proof -
    have "isolated_singularity_at fg z"
      unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] .
    moreover have "not_essential fg z"
      by (simp add: f_iso f_ness fg_def g_iso g_ness not_essential_times)
    moreover have "∃🪙F w in at z. fg w ≠ 0"
      using fg_def fg_nconst by blast
    ultimately show ?thesis 
      using that zorder_exist[of fg z] fgn_def fgp_def by fastforce
  qed
  define r2 where "r2 = min fgr r1"
  have "r2>0" using ‹r1>0› ‹fgr>0› unfolding r2_def by simp
  show "fgn = fn + gn "
  proof (rule holomorphic_factor_unique)
    show "∀w ∈ ball z r2 - {z}. fg w = fgp w * (w - z) powi fgn ∧ fgp w ≠ 0 ∧ fg w = fp w * gp w * (w - z) powi (fn + gn) ∧ fp w * gp w ≠ 0"
      using fg_times fgp_nz fgr(2) r2_def by fastforce
  next
    show "fgp holomorphic_on ball z r2"
      using fgr(1) r2_def by auto
  next
    show "(λw. fp w * gp w) holomorphic_on ball z r2"
      by (metis ball_subset_cball fr(1) gr(1) holomorphic_on_mult holomorphic_on_subset
          min.cobounded1 min.cobounded2 r1_def r2_def subset_ball)
  qed (auto simp add: ‹0 🚫›)

  have "fgp w = fp w *gp w" when w: "w ∈ ball z r2-{z}" for w
  proof -
    have "w ∈ ball z r1 - {z}" "w ∈ cball z fgr - {z}" "w≠z" 
      using w unfolding r2_def by auto
    then show ?thesis
      by (metis ‹fgn = fn + gn› eq_iff_diff_eq_0 fg_times fgr(2) power_int_eq_0_iff
          mult_right_cancel)
  qed
  then show "∀🪙Fw in (at z). fgp w = fp w * gp w"
    using ‹r2>0› unfolding eventually_at by (auto simp add: dist_commute)
qed

lemma
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
      and f_ness: "not_essential f z" and g_ness: "not_essential g z"
      and fg_nconst: "∃🪙Fw in (at z). f w * g w≠ 0"
  shows zorder_divide: "zorder (λw. f w / g w) z = zorder f z - zorder g z" and
        zor_poly_divide: "∀🪙Fw in (at z). zor_poly (λw. f w / g w) z w
                                       = zor_poly f z w / zor_poly g z w"
proof -
  have f_nconst: "∃🪙Fw in (at z). f w ≠ 0" and g_nconst: "∃🪙Fw in (at z).g w≠ 0"
    using fg_nconst by (auto elim!:frequently_elim1)
  define vg where "vg=(λw. inverse (g w))"
  have 1: "isolated_singularity_at vg z"
    by (simp add: g_iso g_ness isolated_singularity_at_inverse vg_def)
  moreover have 2: "not_essential vg z"
    by (simp add: g_iso g_ness not_essential_inverse vg_def)
  moreover have 3: "∃🪙F w in at z. f w * vg w ≠ 0"
    using fg_nconst vg_def by auto
  ultimately have "zorder (λw. f w * vg w) z = zorder f z + zorder vg z"
    using zorder_times[OF f_iso _ f_ness] by blast
  then show "zorder (λw. f w / g w) z = zorder f z - zorder g z"
    using zorder_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def
    by (auto simp add: field_simps)
  have "∀🪙F w in at z. zor_poly (λw. f w * vg w) z w = zor_poly f z w * zor_poly vg z w"
    using zor_poly_times[OF f_iso _ f_ness,of vg] 1 2 3 by blast
  then show "∀🪙Fw in (at z). zor_poly (λw. f w / g w) z w = zor_poly f z w / zor_poly g z w"
    using zor_poly_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def
    by eventually_elim (auto simp add: field_simps)
qed

lemma zorder_exist_zero:
  fixes f:: "complex ==> complex" and z::complex
  defines "n ≡ zorder f z" and "g ≡ zor_poly f z"
  assumes  holo: "f holomorphic_on S" and "open S" "connected S" "z∈S"
      and non_const: "∃w∈S. f w ≠ 0"
  shows "(if f z=0 then n > 0 else n=0) ∧ (∃r. r>0 ∧ cball z r ⊆ S ∧ g holomorphic_on cball z r
    ∧ (∀w∈cball z r. f w = g w * (w-z) ^ nat n ∧ g w ≠0))"
proof -
  obtain r where "g z ≠ 0" and r: "r>0" "cball z r ⊆ S" "g holomorphic_on cball z r"
            "(∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
  proof -
    have "g z ≠ 0 ∧ (∃r>0. g holomorphic_on cball z r
            ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0))"
    proof (rule zorder_exist[of f z,folded g_def n_def])
      show "isolated_singularity_at f z"
        using ‹open S› ‹z∈S› holo holomorphic_on_imp_analytic_at isolated_singularity_at_analytic 
        by force 
      show "not_essential f z" unfolding not_essential_def
        using ‹open S› ‹z∈S› at_within_open continuous_on holo holomorphic_on_imp_continuous_on
        by fastforce
      have "∀🪙F w in at z. f w ≠ 0 ∧ w∈S"
        using assms(4,5,6) holo non_const non_zero_neighbour_alt by blast
      then show "∃🪙F w in at z. f w ≠ 0"
        by (auto elim: eventually_frequentlyE)
    qed
    then obtain r1 where "g z ≠ 0" "r1>0" and r1: "g holomorphic_on cball z r1"
            "(∀w∈cball z r1 - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
      by auto
    obtain r2 where r2: "r2>0" "cball z r2 ⊆ S"
      using assms(4,6) open_contains_cball_eq by blast
    define r3 where "r3 ≡ min r1 r2"
    have "r3>0" "cball z r3 ⊆ S" using ‹r1>0› r2 unfolding r3_def by auto
    moreover have "g holomorphic_on cball z r3"
      using r1(1) unfolding r3_def by auto
    moreover have "(∀w∈cball z r3 - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
      using r1(2) unfolding r3_def by auto
    ultimately show ?thesis using that[of r3] ‹g z≠0› by auto
  qed

  have fz_lim: "f←- z → f z"
    by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
  have gz_lim: "g ←-z→g z"
    using r
    by (meson Elementary_Metric_Spaces.open_ball analytic_at analytic_at_imp_isCont 
        ball_subset_cball centre_in_ball holomorphic_on_subset isContD)
  have if_0: "if f z=0 then n > 0 else n=0"
  proof -
    have "(λw. g w * (w-z) powi n) ←-z→ f z"
      using fz_lim Lim_transform_within_open[where s="ball z r"] r by fastforce
    then have "(λw. (g w * (w-z) powi n) / g w) ←-z→ f z/g z"
      using gz_lim ‹g z ≠ 0› tendsto_divide by blast
    then have powi_tendsto: "(λw. (w-z) powi n) ←-z→ f z/g z"
      using Lim_transform_within_open[where s="ball z r"] r by fastforce

    have ?thesis when "n≥0" "f z=0"
    proof -
      have "(λw. (w-z) ^ nat n) ←-z→ f z/g z"
        using Lim_transform_within[OF powi_tendsto, where d=r]
        by (meson power_int_def r(1) that(1))
      then have *: "(λw. (w-z) ^ nat n) ←-z→ 0" using ‹f z=0› by simp
      moreover have False when "n=0"
      proof -
        have "(λw. (w-z) ^ nat n) ←-z→ 1"
          using ‹n=0› by auto
        then show False using * using LIM_unique zero_neq_one by blast
      qed
      ultimately show ?thesis using that by fastforce
    qed
    moreover have ?thesis when "n≥0" "f z≠0"
    proof -
      have False when "n>0"
      proof -
        have "(λw. (w-z) ^ nat n) ←-z→ f z/g z"
          using Lim_transform_within[OF powi_tendsto, where d=r]
          by (meson ‹0 ≤ n› power_int_def r(1))
        moreover have "(λw. (w-z) ^ nat n) ←-z→ 0"
          using ‹n>0› by (auto intro!:tendsto_eq_intros)
        ultimately show False 
          using ‹f z≠0› ‹g z≠0› LIM_unique divide_eq_0_iff by blast
      qed
      then show ?thesis using that by force
    qed
    moreover have False when "n<0"
    proof -
      have "(λw. inverse ((w-z) ^ nat (- n))) ←-z→ f z/g z"
        by (smt (verit) LIM_cong power_int_def power_inverse powi_tendsto that)
      moreover
      have "(λw.((w-z) ^ nat (- n))) ←-z→ 0"
        using that by (auto intro!:tendsto_eq_intros)
      ultimately
      have "(λx. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) ←-z→ 0" 
        using tendsto_mult by fastforce
      then have "(λx. 1::complex) ←-z→ 0"
        using Lim_transform_within_open by fastforce
      then show False 
        using LIM_const_eq by fastforce
    qed
    ultimately show ?thesis by fastforce
  qed
  moreover have "f w = g w * (w-z) ^ nat n ∧ g w ≠0" when "w∈cball z r" for w
  proof (cases "w=z")
    case True
    then have "f ←-z→f w"
      using fz_lim by blast
    then have "(λw. g w * (w-z) ^ nat n) ←-z→f w"
    proof (elim Lim_transform_within[OF _ ‹r>0›])
      fix x assume "0 < dist x z" "dist x z < r"
      then have "x ∈ cball z r - {z}" "x≠z"
        unfolding cball_def by (auto simp add: dist_commute)
      then have "f x = g x * (x - z) powi n"
        using r(4)[rule_format,of x] by simp
      also have "... = g x * (x - z) ^ nat n"
        by (smt (verit, best) if_0 int_nat_eq power_int_of_nat)
      finally show "f x = g x * (x - z) ^ nat n" .
    qed
    moreover have "(λw. g w * (w-z) ^ nat n) ←-z→ g w * (w-z) ^ nat n"
      using True by (auto intro!:tendsto_eq_intros gz_lim)
    ultimately have "f w = g w * (w-z) ^ nat n" using LIM_unique by blast
    then show ?thesis using ‹g z≠0› True by auto
  next
    case False
    then have "f w = g w * (w-z) powi n" "g w ≠ 0"
      using r(4) that by auto
    then show ?thesis
      by (smt (verit, best) False if_0 int_nat_eq power_int_of_nat)
  qed
  ultimately show ?thesis using r by auto
qed

lemma zorder_exist_pole:
  fixes f:: "complex ==> complex" and z::complex
  defines "n≡zorder f z" and "g≡zor_poly f z"
  assumes  holo: "f holomorphic_on S-{z}" and "open S" "z∈S" and "is_pole f z"
  shows "n < 0 ∧ g z≠0 ∧ (∃r. r>0 ∧ cball z r ⊆ S ∧ g holomorphic_on cball z r
    ∧ (∀w∈cball z r - {z}. f w = g w / (w-z) ^ nat (- n) ∧ g w ≠0))"
proof -
  obtain r where "g z ≠ 0" and r: "r>0" "cball z r ⊆ S" "g holomorphic_on cball z r"
            "(∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
  proof -
    have "g z ≠ 0 ∧ (∃r>0. g holomorphic_on cball z r
            ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0))"
    proof (rule zorder_exist[of f z,folded g_def n_def])
      show "isolated_singularity_at f z" unfolding isolated_singularity_at_def
        using holo assms(4,5)
        by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
      show "not_essential f z" unfolding not_essential_def
        using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on
        by fastforce
      from non_zero_neighbour_pole[OF ‹is_pole f z›] show "∃🪙F w in at z. f w ≠ 0"
        by (auto elim: eventually_frequentlyE)
    qed
    then obtain r1 where "g z ≠ 0" "r1>0" and r1: "g holomorphic_on cball z r1"
            "(∀w∈cball z r1 - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
      by auto
    obtain r2 where r2: "r2>0" "cball z r2 ⊆ S"
      using assms(4,5) open_contains_cball_eq by metis
    define r3 where "r3=min r1 r2"
    have "r3>0" "cball z r3 ⊆ S" using ‹r1>0› r2 unfolding r3_def by auto
    moreover have "g holomorphic_on cball z r3"
      using r1(1) unfolding r3_def by auto
    moreover have "(∀w∈cball z r3 - {z}. f w = g w * (w-z) powi n ∧ g w ≠ 0)"
      using r1(2) unfolding r3_def by auto
    ultimately show ?thesis 
      using that[of r3] ‹g z≠0› by auto
  qed

  have "n<0"
  proof (rule ccontr)
    assume " ¬ n < 0"
    define c where "c=(if n=0 then g z else 0)"
    have [simp]: "g ←-z→ g z"
      using r
      by (metis centre_in_ball continuous_on_interior holomorphic_on_imp_continuous_on
          interior_cball isContD)
    have "∀x ∈ ball z r. x ≠ z ⟶ f x = g x * (x - z) ^ nat n"
      by (simp add: ‹¬ n 🚫› linorder_not_le power_int_def r)
    then have "∀🪙F x in at z. f x = g x * (x - z) ^ nat n"
      using centre_in_ball eventually_at_topological r(1) by blast
    moreover have "(λx. g x * (x - z) ^ nat n) ←-z→ c"
    proof (cases "n=0")
      case True
      then show ?thesis unfolding c_def by simp
    next
      case False
      then have "(λx. (x - z) ^ nat n) ←-z→ 0" using ‹¬ n 🚫›
        by (auto intro!:tendsto_eq_intros)
      from tendsto_mult[OF _ this,of g "g z",simplified]
      show ?thesis unfolding c_def using False by simp
    qed
    ultimately have "f ←-z→c" using tendsto_cong by fast
    then show False using ‹is_pole f z› at_neq_bot not_tendsto_and_filterlim_at_infinity
      unfolding is_pole_def by blast
  qed
  moreover have "∀w∈cball z r - {z}. f w = g w / (w-z) ^ nat (- n) ∧ g w ≠0"
    using r(4) ‹n🚫›
    by (smt (verit) inverse_eq_divide mult.right_neutral power_int_def power_inverse times_divide_eq_right)
  ultimately show ?thesis 
    using r ‹g z≠0› by auto
qed

lemma zorder_eqI:
  assumes "open S" "z ∈ S" "g holomorphic_on S" "g z ≠ 0"
  assumes fg_eq: "∧w. [w ∈ S;w≠z] ==> f w = g w * (w-z) powi n"
  shows   "zorder f z = n"
proof -
  have "continuous_on S g" by (rule holomorphic_on_imp_continuous_on) fact
  moreover have "open (-{0::complex})" by auto
  ultimately have "open ((g -` (-{0})) ∩ S)"
    unfolding continuous_on_open_vimage[OF ‹open S›] by blast
  moreover from assms have "z ∈ (g -` (-{0})) ∩ S" by auto
  ultimately obtain r where r: "r > 0" "cball z r ⊆ S ∩ (g -` (-{0}))"
    unfolding open_contains_cball by blast

  let ?gg= "(λw. g w * (w-z) powi n)"
  define P where "P = (λn g r. 0 < r ∧ g holomorphic_on cball z r ∧ g z≠0
          ∧ (∀w∈cball z r - {z}. f w = g w * (w-z) powi n ∧ g w≠0))"
  have "P n g r"
    unfolding P_def using r assms(3,4,5) by auto
  then have "∃g r. P n g r" by auto
  moreover have unique: "∃!n. ∃g r. P n g r" unfolding P_def
  proof (rule holomorphic_factor_puncture)
    have "ball z r-{z} ⊆ S" using r using ball_subset_cball by blast
    then have "?gg holomorphic_on ball z r-{z}"
      using ‹g holomorphic_on S› r by (auto intro!: holomorphic_intros)
    then have "f holomorphic_on ball z r - {z}"
      by (smt (verit, best) DiffD2 ‹ball z r-{z} ⊆ S› fg_eq holomorphic_cong singleton_iff subset_iff)
    then show "isolated_singularity_at f z" unfolding isolated_singularity_at_def
      using analytic_on_open open_delete r(1) by blast
  next
    have "not_essential ?gg z"
    proof (intro singularity_intros)
      show "not_essential g z"
        by (meson ‹continuous_on S g› assms continuous_on_eq_continuous_at
            isCont_def not_essential_def)
      show " ∀🪙F w in at z. w - z ≠ 0" by (simp add: eventually_at_filter)
      then show "LIM w at z. w - z :> at 0"
        unfolding filterlim_at by (auto intro: tendsto_eq_intros)
      show "isolated_singularity_at g z"
        by (meson Diff_subset open_ball analytic_on_holomorphic
            assms holomorphic_on_subset isolated_singularity_at_def openE)
    qed
    moreover
    have "∀🪙F w in at z. g w * (w-z) powi n = f w"
      unfolding eventually_at_topological using assms fg_eq by force
    ultimately show "not_essential f z"
      using not_essential_transform by blast
    show "∃🪙F w in at z. f w ≠ 0" unfolding frequently_at
    proof (intro strip)
      fix d::real assume "0 < d"
      define z' where "z' ≡ z+min d r / 2"
      have "z' ≠ z" " dist z' z < d "
        unfolding z'_def using ‹d>0› ‹r>0› by (auto simp add: dist_norm)
      moreover have "f z' ≠ 0"
      proof (subst fg_eq[OF _ ‹z'≠z›])
        have "z' ∈ cball z r"
          unfolding z'_def using ‹r>0› ‹d>0› by (auto simp add: dist_norm)
        then show "z' ∈ S" using r(2) by blast
        show "g z' * (z' - z) powi n ≠ 0"
          using P_def ‹P n g r› ‹z' ∈ cball z r› ‹z' ≠ z› by auto
      qed
      ultimately show "∃x∈UNIV. x ≠ z ∧ dist x z < d ∧ f x ≠ 0" by auto
    qed
  qed
  ultimately have "(THE n. ∃g r. P n g r) = n"
    by (rule_tac the1_equality)
  then show ?thesis unfolding zorder_def P_def by blast
qed

lemma simple_zeroI:
  assumes "open S" "z ∈ S" "g holomorphic_on S" "g z ≠ 0"
  assumes "∧w. w ∈ S ==> f w = g w * (w-z)"
  shows   "zorder f z = 1"
  using assms zorder_eqI by force

lemma higher_deriv_power:
  shows   "(deriv ^^ j) (λw. (w-z) ^ n) w =
             pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j)"
proof (induction j arbitrary: w)
  case 0
  thus ?case by auto
next
  case (Suc j w)
  have "(deriv ^^ Suc j) (λw. (w-z) ^ n) w = deriv ((deriv ^^ j) (λw. (w-z) ^ n)) w"
    by simp
  also have "(deriv ^^ j) (λw. (w-z) ^ n) =
               (λw. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j))"
    using Suc by (intro Suc.IH ext)
  also {
    have "(… has_field_derivative of_nat (n - j) *
               pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - Suc j)) (at w)"
      using Suc.prems by (auto intro!: derivative_eq_intros)
    also have "of_nat (n - j) * pochhammer (of_nat (Suc n - j)) j =
                 pochhammer (of_nat (Suc n - Suc j)) (Suc j)"
      by (cases "Suc j ≤ n", subst pochhammer_rec)
         (use Suc.prems in ‹simp_all add: algebra_simps Suc_diff_le pochhammer_0_left›)
    finally have "deriv (λw. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j)) w =
                    … * (w-z) ^ (n - Suc j)"
      by (rule DERIV_imp_deriv)
  }
  finally show ?case .
qed

lemma zorder_zero_eqI:
  assumes  f_holo: "f holomorphic_on S" and "open S" "z ∈ S"
  assumes zero: "∧i. i < nat n ==> (deriv ^^ i) f z = 0"
  assumes nz: "(deriv ^^ nat n) f z ≠ 0" and "n≥0"
  shows   "zorder f z = n"
proof -
  obtain r where [simp]: "r>0" and "ball z r ⊆ S"
    using ‹open S› ‹z∈S› openE by blast
  have nz': "∃w∈ball z r. f w ≠ 0"
  proof (rule ccontr)
    assume "¬ (∃w∈ball z r. f w ≠ 0)"
    then have "eventually (λu. f u = 0) (nhds z)"
      using open_ball ‹0 🚫› centre_in_ball eventually_nhds by blast
    then have "(deriv ^^ nat n) f z = (deriv ^^ nat n) (λ_. 0) z"
      by (intro higher_deriv_cong_ev) auto
    also have "(deriv ^^ nat n) (λ_. 0) z = 0"
      by (induction n) simp_all
    finally show False using nz by contradiction
  qed

  define zn g where "zn = zorder f z" and "g = zor_poly f z"
  obtain e where e_if: "if f z = 0 then 0 < zn else zn = 0" and
            [simp]: "e>0" and "cball z e ⊆ ball z r" and
            g_holo: "g holomorphic_on cball z e" and
            e_fac: "(∀w∈cball z e. f w = g w * (w-z) ^ nat zn ∧ g w ≠ 0)"
  proof -
    have "f holomorphic_on ball z r"
      using f_holo ‹ball z r ⊆ S› by auto
    from that zorder_exist_zero[of f "ball z r" z,simplified,OF this nz',folded zn_def g_def]
    show thesis by blast
  qed
  then obtain "zn ≥ 0" "g z ≠ 0"
    by (metis centre_in_cball less_le_not_le order_refl)

  define A where "A ≡ (λi. of_nat (i choose (nat zn)) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z)"
  have deriv_A: "(deriv ^^ i) f z = (if zn ≤ int i then A i else 0)" for i
  proof -
    have "eventually (λw. w ∈ ball z e) (nhds z)"
      using ‹cball z e ⊆ ball z r› ‹e>0› by (intro eventually_nhds_in_open) auto
    hence "eventually (λw. f w = (w-z) ^ (nat zn) * g w) (nhds z)"
      using e_fac eventually_mono by fastforce
    hence "(deriv ^^ i) f z = (deriv ^^ i) (λw. (w-z) ^ nat zn * g w) z"
      by (intro higher_deriv_cong_ev) auto
    also have "… = (∑j=0..i. of_nat (i choose j) *
                       (deriv ^^ j) (λw. (w-z) ^ nat zn) z * (deriv ^^ (i - j)) g z)"
      using g_holo ‹e>0›
      by (intro higher_deriv_mult[of _ "ball z e"]) (auto intro!: holomorphic_intros)
    also have "… = (∑j=0..i. if j = nat zn then
                    of_nat (i choose nat zn) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z else 0)"
    proof (intro sum.cong refl, goal_cases)
      case (1 j)
      have "(deriv ^^ j) (λw. (w-z) ^ nat zn) z =
              pochhammer (of_nat (Suc (nat zn) - j)) j * 0 ^ (nat zn - j)"
        by (subst higher_deriv_power) auto
      also have "… = (if j = nat zn then fact j else 0)"
        by (auto simp: not_less pochhammer_0_left pochhammer_fact)
      also have "of_nat (i choose j) * … * (deriv ^^ (i - j)) g z =
                   (if j = nat zn then of_nat (i choose (nat zn)) * fact (nat zn)
                        * (deriv ^^ (i - nat zn)) g z else 0)"
        by simp
      finally show ?case .
    qed
    also have "… = (if i ≥ zn then A i else 0)"
      by (auto simp: A_def)
    finally show "(deriv ^^ i) f z = …" .
  qed

  have False when "n
    using deriv_A[of "nat n"] that ‹n≥0› by (simp add: nz) 
  moreover have "n≤zn"
  proof -
    have "g z ≠ 0"
      by (simp add: ‹g z ≠ 0›)
    then have "(deriv ^^ nat zn) f z ≠ 0"
      using deriv_A[of "nat zn"] by(auto simp add: A_def)
    then have "nat zn ≥ nat n" using zero[of "nat zn"] by linarith
    moreover have "zn≥0" using e_if by (auto split: if_splits)
    ultimately show ?thesis using nat_le_eq_zle by blast
  qed
  ultimately show ?thesis unfolding zn_def by fastforce
qed

lemma
  assumes "eventually (λz. f z = g z) (at z)" "z = z'"
  shows zorder_cong: "zorder f z = zorder g z'" and zor_poly_cong: "zor_poly f z = zor_poly g z'"
proof -
  define P where "P = (λff n h r. 0 < r ∧ h holomorphic_on cball z r ∧ h z≠0
                    ∧ (∀w∈cball z r - {z}. ff w = h w * (w-z) powi n ∧ h w≠0))"
  have "(∃r. P f n h r) = (∃r. P g n h r)" for n h
  proof -
    have *: "∃r. P g n h r" if "∃r. P f n h r" and "eventually (λx. f x = g x) (at z)" for f g
    proof -
      from that(1) obtain r1 where r1_P: "P f n h r1" by auto
      from that(2) obtain r2 where "r2>0" and r2_dist: "∀x. x ≠ z ∧ dist x z ≤ r2 ⟶ f x = g x"
        unfolding eventually_at_le by auto
      define r where "r=min r1 r2"
      have "r>0" "h z≠0" using r1_P ‹r2>0› unfolding r_def P_def by auto
      moreover have "h holomorphic_on cball z r"
        using r1_P unfolding P_def r_def by auto
      moreover have "g w = h w * (w-z) powi n ∧ h w ≠ 0" when "w∈cball z r - {z}" for w
      proof -
        have "f w = h w * (w-z) powi n ∧ h w ≠ 0"
          using r1_P that unfolding P_def r_def by auto
        moreover have "f w=g w"
          using r2_dist that by (simp add: dist_commute r_def)
        ultimately show ?thesis by simp
      qed
      ultimately show ?thesis unfolding P_def by auto
    qed
    from assms have eq': "eventually (λz. g z = f z) (at z)"
      by (simp add: eq_commute)
    show ?thesis
      using "*" assms(1) eq' by blast
  qed
  then show "zorder f z = zorder g z'" "zor_poly f z = zor_poly g z'"
      using ‹z=z'› unfolding P_def zorder_def zor_poly_def by auto
qed

lemma zorder_times_analytic':
  assumes "isolated_singularity_at f z" "not_essential f z"
  assumes "g analytic_on {z}" "frequently (λz. f z * g z ≠ 0) (at z)"
  shows   "zorder (λx. f x * g x) z = zorder f z + zorder g z"
  using assms isolated_singularity_at_analytic not_essential_analytic zorder_times by blast

lemma zorder_cmult:
  assumes "c ≠ 0"
  shows   "zorder (λz. c * f z) z = zorder f z"
proof -
  define P where
    "P = (λf n h r. 0 < r ∧ h holomorphic_on cball z r ∧
                    h z ≠ 0 ∧ (∀w∈cball z r - {z}. f w = h w * (w-z) powi n ∧ h w ≠ 0))"
  have *: "P (λx. c * f x) n (λx. c * h x) r" 
    if "P f n h r" "c ≠ 0" for f n h r c
    using that unfolding P_def by (auto intro!: holomorphic_intros)
  have "(∃h r. P (λx. c * f x) n h r) ⟷ (∃h r. P f n h r)" for n
    using *[of f n _ _ c] *[of "λx. c * f x" n _ _ "inverse c"] ‹c ≠ 0›
    by (fastforce simp: field_simps)
  hence "(THE n. ∃h r. P (λx. c * f x) n h r) = (THE n. ∃h r. P f n h r)"
    by simp
  thus ?thesis
    by (simp add: zorder_def P_def)
qed

lemma zorder_uminus [simp]: "zorder (λz. -f z) z = zorder f z"
  using zorder_cmult[of "-1" f] by simp

lemma zorder_nonzero_div_power:
  assumes sz: "open S" "z ∈ S" "f holomorphic_on S" "f z ≠ 0" and "n > 0"
  shows  "zorder (λw. f w / (w-z) ^ n) z = - n"
  by (intro zorder_eqI [OF sz]) (simp add: inverse_eq_divide power_int_minus)

lemma zor_poly_eq:
  assumes "isolated_singularity_at f z" "not_essential f z" "∃🪙F w in at z. f w ≠ 0"
  shows "eventually (λw. zor_poly f z w = f w * (w-z) powi - zorder f z) (at z)"
proof -
  obtain r where r: "r>0"
       "(∀w∈cball z r - {z}. f w = zor_poly f z w * (w-z) powi (zorder f z))"
    using zorder_exist[OF assms] by blast
  then have *: "∀w∈ball z r - {z}. zor_poly f z w = f w * (w-z) powi - zorder f z"
    by (auto simp: field_simps power_int_minus)
  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r eventually_at_ball'[of r z UNIV] by auto
  thus ?thesis by eventually_elim (insert *, auto)
qed

lemma zor_poly_zero_eq:
  assumes "f holomorphic_on S" "open S" "connected S" "z ∈ S" "∃w∈S. f w ≠ 0"
  shows "eventually (λw. zor_poly f z w = f w / (w-z) ^ nat (zorder f z)) (at z)"
proof -
  obtain r where r: "r>0"
       "(∀w∈cball z r - {z}. f w = zor_poly f z w * (w-z) ^ nat (zorder f z))"
    using zorder_exist_zero[OF assms] by auto
  then have *: "∀w∈ball z r - {z}. zor_poly f z w = f w / (w-z) ^ nat (zorder f z)"
    by (auto simp: field_simps powr_minus)
  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r eventually_at_ball'[of r z UNIV] by auto
  thus ?thesis by eventually_elim (insert *, auto)
qed

lemma zor_poly_pole_eq:
  assumes f_iso: "isolated_singularity_at f z" "is_pole f z"
  shows "eventually (λw. zor_poly f z w = f w * (w-z) ^ nat (- zorder f z)) (at z)"
proof -
  obtain e where [simp]: "e>0" and f_holo: "f holomorphic_on ball z e - {z}"
    using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
  obtain r where r: "r>0"
       "(∀w∈cball z r - {z}. f w = zor_poly f z w / (w-z) ^ nat (- zorder f z))"
    using zorder_exist_pole[OF f_holo,simplified,OF ‹is_pole f z›] by auto
  then have *: "∀w∈ball z r - {z}. zor_poly f z w = f w * (w-z) ^ nat (- zorder f z)"
    by (auto simp: field_simps)
  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r eventually_at_ball'[of r z UNIV] by auto
  thus ?thesis by eventually_elim (insert *, auto)
qed

lemma zor_poly_eqI:
  fixes f :: "complex ==> complex" and z0 :: complex
  defines "n ≡ zorder f z0"
  assumes "isolated_singularity_at f z0" "not_essential f z0" "∃🪙F w in at z0. f w ≠ 0"
  assumes lim: "((λx. f (g x) * (g x - z0) powi - n) ---> c) F"
  assumes g: "filterlim g (at z0) F" and "F ≠ bot"
  shows   "zor_poly f z0 z0 = c"
proof -
  from zorder_exist[OF assms(2-4)] obtain r where
    r: "r > 0" "zor_poly f z0 holomorphic_on cball z0 r"
       "∧w. w ∈ cball z0 r - {z0} ==> f w = zor_poly f z0 w * (w - z0) powi n"
    unfolding n_def by blast
  from r(1) have "eventually (λw. w ∈ ball z0 r ∧ w ≠ z0) (at z0)"
    using eventually_at_ball'[of r z0 UNIV] by auto
  hence "eventually (λw. zor_poly f z0 w = f w * (w - z0) powi - n) (at z0)"
    by eventually_elim (insert r, auto simp: field_simps power_int_minus)
  moreover have "continuous_on (ball z0 r) (zor_poly f z0)"
    using r by (intro holomorphic_on_imp_continuous_on) auto
  with r have "isCont (zor_poly f z0) z0"
    by (auto simp: continuous_on_eq_continuous_at)
  hence "(zor_poly f z0 ---> zor_poly f z0 z0) (at z0)"
    unfolding isCont_def .
  ultimately have "((λw. f w * (w - z0) powi - n) ---> zor_poly f z0 z0) (at z0)"
    by (blast intro: Lim_transform_eventually)
  hence "((λx. f (g x) * (g x - z0) powi - n) ---> zor_poly f z0 z0) F"
    by (rule filterlim_compose[OF _ g])
  from tendsto_unique[OF ‹F ≠ bot› this lim] show ?thesis .
qed

lemma zor_poly_zero_eqI:
  fixes f :: "complex ==> complex" and z0 :: complex
  defines "n ≡ zorder f z0"
  assumes "f holomorphic_on A" "open A" "connected A" "z0 ∈ A" "∃z∈A. f z ≠ 0"
  assumes lim: "((λx. f (g x) / (g x - z0) ^ nat n) ---> c) F"
  assumes g: "filterlim g (at z0) F" and "F ≠ bot"
  shows   "zor_poly f z0 z0 = c"
proof -
  from zorder_exist_zero[OF assms(2-6)] obtain r where
    r: "r > 0" "cball z0 r ⊆ A" "zor_poly f z0 holomorphic_on cball z0 r"
       "∧w. w ∈ cball z0 r ==> f w = zor_poly f z0 w * (w - z0) ^ nat n"
    unfolding n_def by blast
  from r(1) have "eventually (λw. w ∈ ball z0 r ∧ w ≠ z0) (at z0)"
    using eventually_at_ball'[of r z0 UNIV] by auto
  hence "eventually (λw. zor_poly f z0 w = f w / (w - z0) ^ nat n) (at z0)"
    by eventually_elim (insert r, auto simp: field_simps)
  moreover have "continuous_on (ball z0 r) (zor_poly f z0)"
    using r by (intro holomorphic_on_imp_continuous_on) auto
  with r(1,2) have "isCont (zor_poly f z0) z0"
    by (auto simp: continuous_on_eq_continuous_at)
  hence "(zor_poly f z0 ---> zor_poly f z0 z0) (at z0)"
    unfolding isCont_def .
  ultimately have "((λw. f w / (w - z0) ^ nat n) ---> zor_poly f z0 z0) (at z0)"
    by (blast intro: Lim_transform_eventually)
  hence "((λx. f (g x) / (g x - z0) ^ nat n) ---> zor_poly f z0 z0) F"
    by (rule filterlim_compose[OF _ g])
  from tendsto_unique[OF ‹F ≠ bot› this lim] show ?thesis .
qed

lemma zor_poly_pole_eqI:
  fixes f :: "complex ==> complex" and z0 :: complex
  defines "n ≡ zorder f z0"
  assumes f_iso: "isolated_singularity_at f z0" and "is_pole f z0"
  assumes lim: "((λx. f (g x) * (g x - z0) ^ nat (-n)) ---> c) F"
  assumes g: "filterlim g (at z0) F" and "F ≠ bot"
  shows   "zor_poly f z0 z0 = c"
proof -
  obtain r where r: "r > 0"  "zor_poly f z0 holomorphic_on cball z0 r"
  proof -
    have "∃🪙F w in at z0. f w ≠ 0"
      using non_zero_neighbour_pole[OF ‹is_pole f z0›] 
      by (auto elim: eventually_frequentlyE)
    moreover have "not_essential f z0" 
      unfolding not_essential_def using ‹is_pole f z0› by simp
    ultimately show ?thesis 
      using that zorder_exist[OF f_iso,folded n_def] by auto
  qed
  from r(1) have "eventually (λw. w ∈ ball z0 r ∧ w ≠ z0) (at z0)"
    using eventually_at_ball'[of r z0 UNIV] by auto
  have "eventually (λw. zor_poly f z0 w = f w * (w - z0) ^ nat (-n)) (at z0)"
    using zor_poly_pole_eq[OF f_iso ‹is_pole f z0›] unfolding n_def .
  moreover have "continuous_on (ball z0 r) (zor_poly f z0)"
    using r by (intro holomorphic_on_imp_continuous_on) auto
  with r(1,2) have "isCont (zor_poly f z0) z0"
    by (auto simp: continuous_on_eq_continuous_at)
  hence "(zor_poly f z0 ---> zor_poly f z0 z0) (at z0)"
    unfolding isCont_def .
  ultimately have "((λw. f w * (w - z0) ^ nat (-n)) ---> zor_poly f z0 z0) (at z0)"
    by (blast intro: Lim_transform_eventually)
  hence "((λx. f (g x) * (g x - z0) ^ nat (-n)) ---> zor_poly f z0 z0) F"
    by (rule filterlim_compose[OF _ g])
  from tendsto_unique[OF ‹F ≠ bot› this lim] show ?thesis .
qed

lemma
  assumes "is_pole f (x :: complex)" "open A" "x ∈ A"
  assumes "∧y. y ∈ A - {x} ==> (f has_field_derivative f' y) (at y)"
  shows   is_pole_deriv': "is_pole f' x"
    and   zorder_deriv':  "zorder f' x = zorder f x - 1"
proof -
  have holo: "f holomorphic_on A - {x}"
    using assms by (subst holomorphic_on_open) auto
  obtain r where r: "r > 0" "ball x r ⊆ A"
    using assms(2,3) openE by blast
  moreover have "open (ball x r - {x})"
    by auto
  ultimately have "isolated_singularity_at f x"
    by (auto simp: isolated_singularity_at_def analytic_on_open
             intro!: exI[of _ r] holomorphic_on_subset[OF holo])
  hence ev: "∀🪙F w in at x. zor_poly f x w = f w * (w-x) ^ nat (- zorder f x)"
    using ‹is_pole f x› zor_poly_pole_eq by blast

  define P where "P = zor_poly f x"
  define n where "n = nat (-zorder f x)"

  obtain r where r: "r > 0" "cball x r ⊆ A" "P holomorphic_on cball x r" "zorder f x < 0" "P x ≠ 0"
    "∀w∈cball x r - {x}. f w = P w / (w-x) ^ n ∧ P w ≠ 0"
    using P_def assms holo n_def zorder_exist_pole by blast
  have n: "n > 0"
    using r(4) by (auto simp: n_def)

  have [derivative_intros]: "(P has_field_derivative deriv P w) (at w)"
    if "w ∈ ball x r" for w
    using that by (intro holomorphic_derivI[OF holomorphic_on_subset[OF r(3), of "ball x r"]]) auto

  define D where "D = (λw. (deriv P w * (w-x) - of_nat n * P w) / (w-x) ^ (n + 1))"
  define n' where "n' = n - 1"
  have n': "n = Suc n'"
    using n by (simp add: n'_def)

  have "eventually (λw. w ∈ ball x r) (nhds x)"
    using ‹r > 0› by (intro eventually_nhds_in_open) auto
  hence ev'': "eventually (λw. w ∈ ball x r - {x}) (at x)"
    by (auto simp: eventually_at_filter elim: eventually_mono)

  {
    fix w assume w: "w ∈ ball x r - {x}"
    have ev': "eventually (λw. w ∈ ball x r - {x}) (nhds w)"
      using w by (intro eventually_nhds_in_open) auto

    have 🍋: "(deriv P w * (w-x) ^ n - P w * (n * (w-x) ^ (n-1))) / ((w-x) ^ n * (w-x) ^ n) = D w"
      using w n' by (simp add: divide_simps D_def) (simp add: algebra_simps)
    have "((λw. P w / (w-x) ^ n) has_field_derivative D w) (at w)"
      by (rule derivative_eq_intros refl | use w 🍋 in force)+
    also have "?this ⟷ (f has_field_derivative D w) (at w)"
      using r by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
    finally have "(f has_field_derivative D w) (at w)" .
    moreover have "(f has_field_derivative f' w) (at w)"
      using w r by (intro assms) auto
    ultimately have "D w = f' w"
      using DERIV_unique by blast
  } note D_eq = this

  have "is_pole D x"
    unfolding D_def using n ‹r > 0› ‹P x ≠ 0›
    by (intro is_pole_basic[where A = "ball x r"] holomorphic_intros holomorphic_on_subset[OF r(3)]) auto
  also have "?this ⟷ is_pole f' x"
    by (intro is_pole_cong eventually_mono[OF ev''] D_eq) auto
  finally show "is_pole f' x" .

  have "zorder f' x = -int (Suc n)"
  proof (rule zorder_eqI)
    show "open (ball x r)" "x ∈ ball x r"
      using ‹r > 0› by auto
    show "f' w = (deriv P w * (w-x) - of_nat n * P w) * (w-x) powi (- int (Suc n))"
      if "w ∈ ball x r" "w ≠ x" for w
      using that D_eq[of w] n by (auto simp: D_def power_int_diff power_int_minus powr_nat' divide_simps)
  qed (use r n in ‹auto intro!: holomorphic_intros›)
  thus "zorder f' x = zorder f x - 1"
    using n by (simp add: n_def)
qed

lemma
  assumes "is_pole f (x :: complex)" "isolated_singularity_at f x"
  shows   is_pole_deriv: "is_pole (deriv f) x"
    and   zorder_deriv:  "zorder (deriv f) x = zorder f x - 1"
proof -
  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
    by (auto simp: isolated_singularity_at_def)
  hence holo: "f holomorphic_on ball x r - {x}"
    by (subst (asm) analytic_on_open) auto
  have *: "x ∈ ball x r" "open (ball x r)" "open (ball x r - {x})"
    using ‹r > 0› by auto
  show "is_pole (deriv f) x" "zorder (deriv f) x = zorder f x - 1"
    by (meson "*" assms(1) holo holomorphic_derivI is_pole_deriv' zorder_deriv')+
qed

lemma removable_singularity_deriv':
  assumes "f ←-x→ c" "x ∈ A" "open (A :: complex set)"
  assumes "∧y. y ∈ A - {x} ==> (f has_field_derivative f' y) (at y)"
  shows   "∃c. f' ←-x→ c"
proof -
  have holo: "f holomorphic_on A - {x}"
    using assms by (subst holomorphic_on_open) auto

  define g where "g = (λy. if y = x then c else f y)"
  have deriv_g_eq: "deriv g y = f' y" if "y ∈ A - {x}" for y
  proof -
    have ev: "eventually (λy. y ∈ A - {x}) (nhds y)"
      using that assms by (intro eventually_nhds_in_open) auto
    have "(f has_field_derivative f' y) (at y)"
      using assms that by auto
    also have "?this ⟷ (g has_field_derivative f' y) (at y)"
      by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev]) (auto simp: g_def)
    finally show ?thesis
      by (intro DERIV_imp_deriv assms)
  qed

  have "g holomorphic_on A"
    unfolding g_def using assms assms(1) holo 
    by (intro removable_singularity) auto
  hence "deriv g holomorphic_on A"
    by (intro holomorphic_deriv assms)
  hence "continuous_on A (deriv g)"
    by (meson holomorphic_on_imp_continuous_on)
  hence "(deriv g ---> deriv g x) (at x within A)"
    using assms by (auto simp: continuous_on_def)
  also have "?this ⟷ (f' ---> deriv g x) (at x within A)"
    by (intro filterlim_cong refl) (auto simp: eventually_at_filter deriv_g_eq)
  finally have "f' ←-x→ deriv g x"
    using ‹open A› ‹x ∈ A› by (meson tendsto_within_open)
  thus ?thesis
    by blast
qed

lemma removable_singularity_deriv:
  assumes "f ←-x→ c" "isolated_singularity_at f x"
  shows   "∃c. deriv f ←-x→ c"
proof -
  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
    by (auto simp: isolated_singularity_at_def)
  hence holo: "f holomorphic_on ball x r - {x}"
    using analytic_imp_holomorphic by blast
  show ?thesis
    using assms(1)
  proof (rule removable_singularity_deriv')
    show "x ∈ ball x r" "open (ball x r)"
      using ‹r > 0› by auto
  qed (auto intro!: holomorphic_derivI[OF holo])
qed

lemma not_essential_deriv':
  assumes "not_essential f x" "x ∈ A" "open A"
  assumes "∧y. y ∈ A - {x} ==> (f has_field_derivative f' y) (at y)"
  shows   "not_essential f' x"
proof -
  have holo: "f holomorphic_on A - {x}"
    using assms by (subst holomorphic_on_open) auto
  from assms consider "is_pole f x" | c where "f ←-x→ c"
    by (auto simp: not_essential_def)
  thus ?thesis
  proof cases
    case 1
    thus ?thesis
      using assms is_pole_deriv' by blast
  next
    case (2 c)
    thus ?thesis
      by (meson assms removable_singularity_deriv' tendsto_imp_not_essential)
  qed
qed

lemma not_essential_deriv[singularity_intros]:
  assumes "not_essential f x" "isolated_singularity_at f x"
  shows   "not_essential (deriv f) x"
proof -
  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
    by (auto simp: isolated_singularity_at_def)
  hence holo: "f holomorphic_on ball x r - {x}"
    by (subst (asm) analytic_on_open) auto
  show ?thesis
    using assms(1)
  proof (rule not_essential_deriv')
    show "x ∈ ball x r" "open (ball x r)"
      using ‹r > 0› by auto
  qed (auto intro!: holomorphic_derivI[OF holo])
qed

lemma not_essential_frequently_0_imp_tendsto_0:
  fixes f :: "complex ==> complex"
  assumes sing: "isolated_singularity_at f z" "not_essential f z"
  assumes freq: "frequently (λz. f z = 0) (at z)"
  shows   "f ←-z→ 0"
proof -
  from freq obtain g :: "nat ==> complex" where g: "filterlim g (at z) at_top" "∧n. f (g n) = 0"
    using frequently_atE by blast
  have "eventually (λx. f (g x) = 0) sequentially"
    using g by auto
  hence fg: "(λx. f (g x)) <---- 0"
    by (simp add: tendsto_eventually)

  from assms(2) consider c where "f ←-z→ c" | "is_pole f z"
    unfolding not_essential_def by blast
  thus ?thesis
  proof cases
    case (1 c)
    have "(λx. f (g x)) <---- c"
      by (rule filterlim_compose[OF 1 g(1)])
    with fg have "c = 0"
      using LIMSEQ_unique by blast
    with 1 show ?thesis by simp
  next
    case 2
    have "filterlim (λx. f (g x)) at_infinity sequentially"
      using "2" filterlim_compose g(1) is_pole_def by blast
    with fg have False
      by (meson not_tendsto_and_filterlim_at_infinity sequentially_bot)
    thus ?thesis ..
  qed
qed

lemma not_essential_frequently_0_imp_eventually_0:
  fixes f :: "complex ==> complex"
  assumes sing: "isolated_singularity_at f z" "not_essential f z"
  assumes freq: "frequently (λz. f z = 0) (at z)"
  shows   "eventually (λz. f z = 0) (at z)"
proof -
  from sing obtain r where r: "r > 0" and "f analytic_on ball z r - {z}"
    by (auto simp: isolated_singularity_at_def)
  hence holo: "f holomorphic_on ball z r - {z}"
    by (subst (asm) analytic_on_open) auto
  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r by (intro eventually_at_in_open) auto
  from freq and this have "frequently (λw. f w = 0 ∧ w ∈ ball z r - {z}) (at z)"
    using frequently_eventually_frequently by blast
  hence "frequently (λw. w ∈ {w∈ball z r - {z}. f w = 0}) (at z)"
    by (simp add: conj_commute)
  hence limpt: "z islimpt {w∈ball z r - {z}. f w = 0}"
    using islimpt_conv_frequently_at by blast

  define g where "g = (λw. if w = z then 0 else f w)"
  have "f ←-z→ 0"
    by (intro not_essential_frequently_0_imp_tendsto_0 assms)
  hence g_holo: "g holomorphic_on ball z r"
    unfolding g_def by (intro removable_singularity holo) auto

  have g_eq_0: "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)"
      using r by auto
    show "z islimpt {w∈ball z r - {z}. f w = 0}"
      by fact
    show "g w = 0" if "w ∈ {w ∈ ball z r - {z}. f w = 0}" for w
      using that by (auto simp: g_def)
  qed (use r that g_holo in auto)

  have "eventually (λw. w ∈ ball z r - {z}) (at z)"
    using r by (intro eventually_at_in_open) auto
  thus "eventually (λw. f w = 0) (at z)"
    by (metis freq non_zero_neighbour not_eventually not_frequently sing)
qed

lemma pole_imp_not_constant:
  fixes f :: "'a :: {perfect_space} ==> _"
  assumes "is_pole f x" "open A" "x ∈ A" "A ⊆ insert x B"
  shows   "¬f constant_on B"
proof
  assume *: "f constant_on B"
  then obtain c where c: "∀x∈B. f x = c"
    by (auto simp: constant_on_def)
  have "eventually (λy. y ∈ A - {x}) (at x)"
    using assms by (intro eventually_at_in_open) auto
  hence "eventually (λy. f y = c) (at x)"
    by eventually_elim (use c assms in auto)
  hence **: "f ←-x→ c"
    by (simp add: tendsto_eventually)
  show False
    using ** ‹is_pole f x› at_neq_bot is_pole_def 
          not_tendsto_and_filterlim_at_infinity by blast
qed


lemma neg_zorder_imp_is_pole:
  assumes iso: "isolated_singularity_at f z" and f_ness: "not_essential f z"
      and "zorder f z < 0" and fre_nz: "∃🪙F w in at z. f w ≠ 0 "
    shows "is_pole f z"
proof -
  define P where "P = zor_poly f z"
  define n where "n = zorder f z"
  have "n<0" unfolding n_def by (simp add: assms(3))
  define nn where "nn = nat (-n)"

  obtain r where r: "P z ≠ 0" "r>0" and r_holo: "P holomorphic_on cball z r" and
       w_Pn: "(∀w∈cball z r - {z}. f w = P w * (w-z) powi n ∧ P w ≠ 0)"
    using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto

  have "is_pole (λw. P w * (w-z) powi n) z"
    unfolding is_pole_def
  proof (rule tendsto_mult_filterlim_at_infinity)
    show "P ←-z→ P z"
      by (metis ‹r>0› r_holo centre_in_ball continuous_on_interior 
                holomorphic_on_imp_continuous_on interior_cball isContD)
    show "P z≠0" by (simp add: ‹P z ≠ 0›)

    have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
      apply (subst filterlim_inverse_at_iff[symmetric])
      using ‹n🚫›
      by (auto intro!:tendsto_eq_intros filterlim_atI
              simp add: eventually_at_filter)
    then show "LIM x at z. (x - z) powi n :> at_infinity"
    proof (elim filterlim_mono_eventually)
      have "inverse ((x - z) ^ nat (-n)) = (x - z) powi n"
        if "x≠z" for x
        by (metis ‹n 🚫› linorder_not_le power_int_def power_inverse)
      then show "∀🪙F x in at z. inverse ((x - z) ^ nat (-n))
                  = (x - z) powi n"
        by (simp add: eventually_at_filter)
    qed auto
  qed
  moreover have "∀🪙F w in at z. f w = P w * (w-z) powi n"
    unfolding eventually_at_le
    using w_Pn ‹r>0› by (force simp add: dist_commute)
  ultimately show ?thesis using is_pole_cong by fast
qed

lemma is_pole_divide_zorder:
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
      and f_ness: "not_essential f z" and g_ness: "not_essential g z"
      and fg_nconst: "∃🪙Fw in (at z). f w * g w≠ 0"
      and z_less: "zorder f z < zorder g z"
    shows "is_pole (λz. f z / g z) z"
proof -
  define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
                        and "fg=(λw. f w / g w)"

  have "isolated_singularity_at fg z"
    unfolding fg_def using f_iso g_iso g_ness
    by (auto intro: singularity_intros)
  moreover have "not_essential fg z"
    unfolding fg_def using f_iso g_iso g_ness f_ness
    by (auto intro: singularity_intros)
  moreover have "zorder fg z < 0"
  proof -
    have "zorder fg z = fn - gn"
      using zorder_divide[OF f_iso g_iso f_ness g_ness fg_nconst]
      by (simp add: fg_def fn_def gn_def) 
    then show ?thesis
      using z_less by (simp add: fn_def gn_def)
  qed
  moreover have "∃🪙F w in at z. fg w ≠ 0"
    using fg_nconst unfolding fg_def by force
  ultimately show "is_pole fg z"
    using neg_zorder_imp_is_pole by auto
qed

lemma isolated_pole_imp_nzero_times:
  assumes f_iso: "isolated_singularity_at f z"
    and "is_pole f z"
  shows "∃🪙Fw in (at z). deriv f w * f w ≠ 0"
proof (rule ccontr)
  assume "¬ (∃🪙F w in at z. deriv f w * f w ≠ 0)"
  then have "∀🪙F x in at z. deriv f x * f x = 0"
    unfolding not_frequently by simp
  moreover have "∀🪙F w in at z. f w ≠ 0"
    using non_zero_neighbour_pole[OF ‹is_pole f z›] .
  moreover have "∀🪙F w in at z. deriv f w ≠ 0"
    using is_pole_deriv[OF ‹is_pole f z› f_iso,THEN non_zero_neighbour_pole]
    .
  ultimately have "∀🪙F w in at z. False"
    by eventually_elim auto
  then show False by auto
qed

lemma isolated_pole_imp_neg_zorder:
  assumes "isolated_singularity_at f z" and "is_pole f z"
  shows "zorder f z < 0"
  using analytic_imp_holomorphic assms centre_in_ball isolated_singularity_at_def zorder_exist_pole by blast


lemma isolated_singularity_at_deriv[singularity_intros]:
  assumes "isolated_singularity_at f x"
  shows "isolated_singularity_at (deriv f) x"
  by (meson analytic_deriv assms isolated_singularity_at_def)

lemma zorder_deriv_minus_1:
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "∃🪙F w in at z. f w ≠ 0"
      and f_ord: "zorder f z ≠0"
    shows "zorder (deriv f) z = zorder f z - 1"
proof -
  define P where "P = zor_poly f z"
  define n where "n = zorder f z"
  have "n≠0" unfolding n_def using f_ord by auto

  obtain r where "P z ≠ 0" "r>0" and P_holo: "P holomorphic_on cball z r"
          and "(∀w∈cball z r - {z}. f w
                            = P w * (w-z) powi n ∧ P w ≠ 0)"
    using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
  from this(4)
  have f_eq: "(∀w∈cball z r - {z}. f w
                            = P w * (w-z) powi n ∧ P w ≠ 0)"
    using complex_powr_of_int f_ord n_def by presburger

  define D where "D = (λw. (deriv P w * (w-z) + of_int n * P w)
                          * (w-z) powi (n - 1))"

  have deriv_f_eq: "deriv f w = D w" if "w ∈ ball z r - {z}" for w
  proof -
    have ev': "eventually (λw. w ∈ ball z r - {z}) (nhds w)"
      using that by (intro eventually_nhds_in_open) auto

    define wz where "wz = w - z"

    have "wz ≠0" unfolding wz_def using that by auto
    moreover have "(P has_field_derivative deriv P w) (at w)"
      by (meson DiffD1 Elementary_Metric_Spaces.open_ball P_holo
          ball_subset_cball holomorphic_derivI holomorphic_on_subset that)
    ultimately have "((λw. P w * (w-z) powi n) has_field_derivative D w) (at w)"
      unfolding D_def using that
      apply (auto intro!: derivative_eq_intros)
      by (auto simp: algebra_simps simp flip:power_int_add_1' wz_def)
    also have "?this ⟷ (f has_field_derivative D w) (at w)"
      using f_eq
      by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
    ultimately have "(f has_field_derivative D w) (at w)" by simp
    moreover have "(f has_field_derivative deriv f w) (at w)"
      by (metis DERIV_imp_deriv calculation)
    ultimately show ?thesis using DERIV_imp_deriv by blast
  qed

  show "zorder (deriv f) z = n - 1"
  proof (rule zorder_eqI)
    show "open (ball z r)" "z ∈ ball z r"
      using ‹r > 0› by auto
    define g where "g=(λw. (deriv P w * (w-z) + of_int n * P w))"
    show "g holomorphic_on ball z r"
      unfolding g_def using P_holo
      by (auto intro!:holomorphic_intros)
    show "g z ≠ 0"
      unfolding g_def using ‹P z ≠ 0› ‹n≠0› by auto
    show "deriv f w = (deriv P w * (w-z) + of_int n * P w) * (w-z) powi (n - 1)"
      if "w ∈ ball z r" "w ≠ z" for w
      using D_def deriv_f_eq that by blast
  qed
qed


lemma deriv_divide_is_pole: 🍋‹Generalises @{thm zorder_deriv}›
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z" 
      and fg_nconst: "∃🪙Fw in (at z). deriv f w * f w ≠ 0"
      and f_ord: "zorder f z ≠ 0"
    shows "is_pole (λz. deriv f z / f z) z"
proof (rule neg_zorder_imp_is_pole)
  define ff where "ff=(λw. deriv f w / f w)"
  show "isolated_singularity_at ff z" 
    using f_iso f_ness unfolding ff_def
    by (auto intro: singularity_intros)
  show "not_essential ff z" 
    unfolding ff_def using f_ness f_iso by (auto intro: singularity_intros)

  have "zorder ff z = zorder (deriv f) z - zorder f z"
    unfolding ff_def using f_iso f_ness fg_nconst
    using isolated_singularity_at_deriv not_essential_deriv zorder_divide by blast
  moreover have "zorder (deriv f) z = zorder f z - 1"
    using f_iso f_ness f_ord fg_nconst frequently_elim1 zorder_deriv_minus_1 by fastforce
  ultimately show "zorder ff z < 0" by auto
    
  show "∃🪙F w in at z. ff w ≠ 0" 
    unfolding ff_def using fg_nconst by auto
qed

lemma is_pole_deriv_divide_is_pole:
  fixes f g:: "complex ==> complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z"
      and "is_pole f z" 
    shows "is_pole (λz. deriv f z / f z) z"
proof (rule deriv_divide_is_pole[OF f_iso])
  show "not_essential f z" 
    using ‹is_pole f z› unfolding not_essential_def by auto
  show "∃🪙F w in at z. deriv f w * f w ≠ 0"
    using assms f_iso isolated_pole_imp_nzero_times by blast
  show "zorder f z ≠ 0"
    using isolated_pole_imp_neg_zorder assms by fastforce
qed

  
subsection ‹Isolated points›

definition isolated_points_of :: "complex set ==> complex set" where
  "isolated_points_of A = {z∈A. eventually (λw. w ∉ A) (at z)}"

lemma isolated_points_of_altdef: "isolated_points_of A = {z∈A. ¬z islimpt A}"
  unfolding isolated_points_of_def islimpt_def eventually_at_filter eventually_nhds by blast

lemma isolated_points_of_empty [simp]: "isolated_points_of {} = {}"
  and isolated_points_of_UNIV [simp]:  "isolated_points_of UNIV = {}"
  by (auto simp: isolated_points_of_def)

lemma isolated_points_of_open_is_empty [simp]: "open A ==> isolated_points_of A = {}"
  unfolding isolated_points_of_altdef 
  by (simp add: interior_limit_point interior_open)

lemma isolated_points_of_subset: "isolated_points_of A ⊆ A"
  by (auto simp: isolated_points_of_def)

lemma isolated_points_of_discrete:
  assumes "discrete A"
  shows   "isolated_points_of A = A"
  using assms by (auto simp: isolated_points_of_def discrete_altdef)

lemmas uniform_discreteI1 = uniformI1
lemmas uniform_discreteI2 = uniformI2

lemma zorder_zero_eqI':
  assumes "f analytic_on {z}"
  assumes "∧i. i < nat n ==> (deriv ^^ i) f z = 0"
  assumes "(deriv ^^ nat n) f z ≠ 0" and "n ≥ 0"
  shows   "zorder f z = n"
proof -
  from assms(1) obtain A where "open A" "z ∈ A" "f holomorphic_on A"
    using analytic_at by blast
  thus ?thesis
    using zorder_zero_eqI[of f A z n] assms by blast
qed


subsection ‹Isolated zeros›

definition isolated_zero :: "('a::topological_space ==> 'b::real_normed_div_algebra) ==> 'a ==> bool" where
  "isolated_zero f a ⟷ f ←-a→ 0 ∧ eventually (λx. f x ≠ 0) (at a)" 

lemma isolated_zero_shift:
  fixes z :: "'a :: real_normed_vector"
  shows "isolated_zero f z ⟷ isolated_zero (λw. f (z + w)) 0"
  unfolding isolated_zero_def
  by (simp add: at_to_0' eventually_filtermap filterlim_filtermap add_ac)  

lemma isolated_zero_shift':
  fixes z :: "'a :: real_normed_vector"
  assumes "NO_MATCH 0 z"
  shows   "isolated_zero f z ⟷ isolated_zero (λw. f (z + w)) 0"
  by (rule isolated_zero_shift)

lemma isolated_zero_imp_not_essential [intro]:
  "isolated_zero f z ==> not_essential f z"
  unfolding isolated_zero_def not_essential_def
  using tendsto_nhds_iff by blast

lemma pole_is_not_zero:
  fixes f:: "'a::perfect_space ==> 'b::real_normed_field"
  assumes "is_pole f z" 
  shows "¬isolated_zero f z"
proof 
  assume "isolated_zero f z"
  then have "filterlim f (nhds 0) (at z)" 
    unfolding isolated_zero_def using tendsto_nhds_iff by blast
  moreover have "filterlim f at_infinity (at z)" 
    using ‹is_pole f z› unfolding is_pole_def .
  ultimately show False
    using not_tendsto_and_filterlim_at_infinity[OF at_neq_bot]
    by auto
qed

lemma isolated_zero_imp_pole_inverse:
  fixes f :: "_ ==> 'b::{real_normed_div_algebra, division_ring}"
  assumes "isolated_zero f z"
  shows   "is_pole (λz. inverse (f z)) z"
proof -
  from assms have ev: "eventually (λz. f z ≠ 0) (at z)"
    by (auto simp: isolated_zero_def)
  have "filterlim f (nhds 0) (at z)"
    using assms by (simp add: isolated_zero_def)
  with ev have "filterlim f (at 0) (at z)"
    using filterlim_atI by blast
  also have "?this ⟷ filterlim (λz. inverse (inverse (f z))) (at 0) (at z)"
    by (rule filterlim_cong) (use ev in ‹auto elim!: eventually_mono›)
  finally have "filterlim (λz. inverse (f z)) at_infinity (at z)"
    by (subst filterlim_inverse_at_iff [symmetric])
  thus ?thesis
    by (simp add: is_pole_def)
qed

lemma is_pole_imp_isolated_zero_inverse:
  fixes f :: "_ ==> 'b::{real_normed_div_algebra, division_ring}"
  assumes "is_pole f z"
  shows   "isolated_zero (λz. inverse (f z)) z"
proof -
  from assms have ev: "eventually (λz. f z ≠ 0) (at z)"
    by (simp add: non_zero_neighbour_pole)
  have "filterlim f at_infinity (at z)"
    using assms by (simp add: is_pole_def)
  also have "?this ⟷ filterlim (λz. inverse (inverse (f z))) at_infinity (at z)"
    by (rule filterlim_cong) (use ev in ‹auto elim!: eventually_mono›)
  finally have "filterlim (λz. inverse (f z)) (at 0) (at z)"
    by (subst (asm) filterlim_inverse_at_iff [symmetric]) auto
  hence "filterlim (λz. inverse (f z)) (nhds 0) (at z)"
    using filterlim_at by blast
  moreover have "eventually (λz. inverse (f z) ≠ 0) (at z)"
    using ev by eventually_elim auto
  ultimately show ?thesis
    by (simp add: isolated_zero_def)
qed

lemma is_pole_inverse_iff: "is_pole (λz. inverse (f z)) z ⟷ isolated_zero f z"
  using is_pole_imp_isolated_zero_inverse isolated_zero_imp_pole_inverse by fastforce

lemma isolated_zero_inverse_iff: "isolated_zero (λz. inverse (f z)) z ⟷ is_pole f z"
  using is_pole_imp_isolated_zero_inverse isolated_zero_imp_pole_inverse by fastforce

lemma zero_isolated_zero:
  fixes f :: "'a :: {t2_space, perfect_space} ==> _"
  assumes "isolated_zero f z" "isCont f z"
  shows "f z = 0"
proof (rule tendsto_unique)
  show "f ←-z→ f z"
    using assms(2) by (rule isContD)
  show "f ←-z→ 0"
    using assms(1) by (simp add: isolated_zero_def)
qed auto

lemma zero_isolated_zero_analytic:
  assumes "isolated_zero f z" "f analytic_on {z}"
  shows   "f z = 0"
  using assms(1) analytic_at_imp_isCont[OF assms(2)] by (rule zero_isolated_zero)

lemma isolated_zero_analytic_iff:
  assumes "f analytic_on {z}"
  shows   "isolated_zero f z ⟷ f z = 0 ∧ eventually (λz. f z ≠ 0) (at z)"
proof safe
  assume "f z = 0" "eventually (λz. f z ≠ 0) (at z)"
  with assms show "isolated_zero f z"
    unfolding isolated_zero_def by (metis analytic_at_imp_isCont isCont_def)
qed (use zero_isolated_zero_analytic[OF _ assms] in ‹auto simp: isolated_zero_def›)

lemma non_isolated_zero_imp_eventually_zero:
  assumes "f analytic_on {z}" "f z = 0" "¬isolated_zero f z"
  shows   "eventually (λz. f z = 0) (at z)"
proof (rule not_essential_frequently_0_imp_eventually_0)
  from assms(1) show "isolated_singularity_at f z"  "not_essential f z"
    by (simp_all add: isolated_singularity_at_analytic not_essential_analytic)
  from assms(1,2) have "f ←-z→ 0"
    by (metis analytic_at_imp_isCont continuous_within)
  thus "frequently (λz. f z = 0) (at z)"
    using assms(2,3) by (auto simp: isolated_zero_def frequently_def)
qed

lemma non_isolated_zero_imp_eventually_zero':
  assumes "f analytic_on {z}" "f z = 0" "¬isolated_zero f z"
  shows   "eventually (λz. f z = 0) (nhds z)"
  using non_isolated_zero_imp_eventually_zero[OF assms] assms(2)
  using eventually_nhds_conv_at by blast

end