# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1675868724 0
# Node ID 607e1e345e8f6dd139f8ad298c50a05177d65b86
# Parent  0c073854e6cea441c3b5c66c28b5d52a4c847ec7
Lots of new material chiefly about complex analysis

diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -2649,7 +2649,7 @@
 
 lemma powr_nat': "(z :: complex) \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
   by (cases "z = 0") (auto simp: powr_nat)
-  
+    
 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   using Ln_Reals_eq norm_exp_eq_Re by (auto simp: Im_Ln_eq_0 powr_def norm_complex_def)
 
@@ -2694,12 +2694,15 @@
   shows "z powr of_int n = (if n\<ge>0 then z^nat n else inverse (z^nat (-n)))"
   by (metis assms not_le of_int_of_nat powr_complexpow powr_minus)
 
+lemma complex_powr_of_int: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_int n = (z :: complex) powi n"
+  by (cases "z = 0 \<or> n = 0")
+     (auto simp: power_int_def powr_minus powr_nat powr_of_int power_0_left power_inverse)
+  
 lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
   by (metis of_real_Re powr_of_real)
 
 lemma norm_powr_real_mono:
-    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
-     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk> \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
   by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
 
 lemma powr_times_real:
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Connected.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -238,10 +238,7 @@
     connected_component_set S x \<inter> T \<noteq> {};
     connected_component_set S y \<inter> T \<noteq> {}\<rbrakk>
     \<Longrightarrow> connected_component_set S x = connected_component_set S y"
-apply (simp add: ex_in_conv [symmetric])
-apply (rule connected_component_eq)
-by (metis (no_types, opaque_lifting) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
-
+  by (metis (full_types) subsetD connected_component_eq connected_component_maximal disjoint_iff_not_equal)
 
 lemma Union_connected_component: "\<Union>(connected_component_set S ` S) = S"
   apply (rule subset_antisym)
@@ -260,10 +257,36 @@
 lemma connected_component_intermediate_subset:
         "\<lbrakk>connected_component_set U a \<subseteq> T; T \<subseteq> U\<rbrakk>
         \<Longrightarrow> connected_component_set T a = connected_component_set U a"
-  apply (case_tac "a \<in> U")
-  apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
-  using connected_component_eq_empty by blast
+  by (metis connected_component_idemp connected_component_mono subset_antisym)
+
 
+lemma connected_component_homeomorphismI:
+  assumes "homeomorphism A B f g" "connected_component A x y"
+  shows   "connected_component B (f x) (f y)"
+proof -
+  from assms obtain T where T: "connected T" "T \<subseteq> A" "x \<in> T" "y \<in> T"
+    unfolding connected_component_def by blast
+  have "connected (f ` T)" "f ` T \<subseteq> B" "f x \<in> f ` T" "f y \<in> f ` T"
+    using assms T continuous_on_subset[of A f T]
+    by (auto intro!: connected_continuous_image simp: homeomorphism_def)
+  thus ?thesis
+    unfolding connected_component_def by blast
+qed
+
+lemma connected_component_homeomorphism_iff:
+  assumes "homeomorphism A B f g"
+  shows   "connected_component A x y \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> connected_component B (f x) (f y)"
+  by (metis assms connected_component_homeomorphismI connected_component_in homeomorphism_apply1 homeomorphism_sym)
+
+lemma connected_component_set_homeomorphism:
+  assumes "homeomorphism A B f g" "x \<in> A"
+  shows   "connected_component_set B (f x) = f ` connected_component_set A x" (is "?lhs = ?rhs")
+proof -
+  have "y \<in> ?lhs \<longleftrightarrow> y \<in> ?rhs" for y
+    by (smt (verit, best) assms connected_component_homeomorphism_iff homeomorphism_def image_iff mem_Collect_eq)
+  thus ?thesis
+    by blast
+qed
 
 subsection \<open>The set of connected components of a set\<close>
 
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -274,6 +274,48 @@
   ultimately show ?thesis by blast
 qed
 
+lemma frequently_atE:
+  fixes x :: "'a :: metric_space"
+  assumes "frequently P (at x within s)"
+  shows   "\<exists>f. filterlim f (at x within s) sequentially \<and> (\<forall>n. P (f n))"
+proof -
+  have "\<exists>y. y \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P y" for n
+  proof -
+    have "\<exists>z\<in>s. z \<noteq> x \<and> dist z x < (1 / real (Suc n)) \<and> P z"
+      by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one)
+    then show ?thesis
+      by (auto simp: dist_commute conj_commute)
+  qed
+  then obtain f where f: "\<And>n. f n \<in> s \<inter> (ball x (1 / real (Suc n)) - {x}) \<and> P (f n)"
+    by metis
+  have "filterlim f (nhds x) sequentially"
+    unfolding tendsto_iff
+  proof clarify
+    fix e :: real
+    assume e: "e > 0"
+    then obtain n where n: "Suc n > 1 / e"
+      by (meson le_nat_floor lessI not_le)
+    have "dist (f k) x < e" if "k \<ge> n" for k
+    proof -
+      have "dist (f k) x < 1 / real (Suc k)"
+        using f[of k] by (auto simp: dist_commute)
+      also have "\<dots> \<le> 1 / real (Suc n)"
+        using that by (intro divide_left_mono) auto
+      also have "\<dots> < e"
+        using n e by (simp add: field_simps)
+      finally show ?thesis .
+    qed
+    thus "\<forall>\<^sub>F k in sequentially. dist (f k) x < e"
+      unfolding eventually_at_top_linorder by blast
+  qed
+  moreover have "f n \<noteq> x" for n
+    using f[of n] by auto
+  ultimately have "filterlim f (at x within s) sequentially"
+    using f by (auto simp: filterlim_at)
+  with f show ?thesis
+    by blast
+qed
+
 subsection \<open>Limit Points\<close>
 
 lemma islimpt_approachable:
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -659,6 +659,16 @@
 lemma bounded_pos_less: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x < b)"
   by (metis bounded_pos le_less_trans less_imp_le linordered_field_no_ub)
 
+lemma bounded_normE:
+  assumes "bounded A"
+  obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z \<le> B"
+  by (meson assms bounded_pos)
+
+lemma bounded_normE_less:
+  assumes "bounded A"
+  obtains B where "B > 0" "\<And>z. z \<in> A \<Longrightarrow> norm z < B"
+  by (meson assms bounded_pos_less)
+
 lemma Bseq_eq_bounded:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "Bseq f \<longleftrightarrow> bounded (range f)"
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -758,6 +758,87 @@
     by simp
 qed
 
+(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
+lemma islimpt_sequential:
+  fixes x :: "'a::first_countable_topology"
+  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
+    (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  from countable_basis_at_decseq[of x] obtain A where A:
+      "\<And>i. open (A i)"
+      "\<And>i. x \<in> A i"
+      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+    by blast
+  define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
+  {
+    fix n
+    from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
+      unfolding islimpt_def using A(1,2)[of n] by auto
+    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
+      unfolding f_def by (rule someI_ex)
+    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
+  }
+  then have "\<forall>n. f n \<in> S - {x}" by auto
+  moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
+  proof (rule topological_tendstoI)
+    fix S
+    assume "open S" "x \<in> S"
+    from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
+    show "eventually (\<lambda>x. f x \<in> S) sequentially"
+      by (auto elim!: eventually_mono)
+  qed
+  ultimately show ?rhs by fast
+next
+  assume ?rhs
+  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
+    by auto
+  show ?lhs
+    unfolding islimpt_def
+  proof safe
+    fix T
+    assume "open T" "x \<in> T"
+    from lim[THEN topological_tendstoD, OF this] f
+    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
+      unfolding eventually_sequentially by auto
+  qed
+qed
+
+lemma islimpt_isCont_image:
+  fixes f :: "'a :: {first_countable_topology, t2_space} \<Rightarrow> 'b :: {first_countable_topology, t2_space}"
+  assumes "x islimpt A" and "isCont f x" and ev: "eventually (\<lambda>y. f y \<noteq> f x) (at x)"
+  shows   "f x islimpt f ` A"
+proof -
+  from assms(1) obtain g where g: "g \<longlonglongrightarrow> x" "range g \<subseteq> A - {x}"
+    unfolding islimpt_sequential by blast
+  have "filterlim g (at x) sequentially"
+    using g by (auto simp: filterlim_at intro!: always_eventually)
+  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> f (g n) \<noteq> f x"
+    by (metis (mono_tags, lifting) ev eventually_at_top_linorder filterlim_iff)
+  have "(\<lambda>x. g (x + N)) \<longlonglongrightarrow> x"
+    using g(1) by (rule LIMSEQ_ignore_initial_segment)
+  hence "(\<lambda>x. f (g (x + N))) \<longlonglongrightarrow> f x"
+    using assms(2) isCont_tendsto_compose by blast
+  moreover have "range (\<lambda>x. f (g (x + N))) \<subseteq> f ` A - {f x}"
+    using g(2) N by auto
+  ultimately show ?thesis
+    unfolding islimpt_sequential by (intro exI[of _ "\<lambda>x. f (g (x + N))"]) auto
+qed
+
+lemma islimpt_image:
+  assumes "z islimpt g -` A \<inter> B" "g z \<notin> A" "z \<in> B" "open B" "continuous_on B g"
+  shows   "g z islimpt A"
+  unfolding islimpt_def
+proof clarify
+  fix T assume T: "g z \<in> T" "open T"
+  have "z \<in> g -` T \<inter> B"
+    using T assms by auto
+  moreover have "open (g -` T \<inter> B)"
+    using T continuous_on_open_vimage assms by blast
+  ultimately show "\<exists>y\<in>A. y \<in> T \<and> y \<noteq> g z"
+    using assms by (metis (mono_tags, lifting) IntD1 islimptE vimageE)
+qed
+  
 
 subsection \<open>Interior of a Set\<close>
 
@@ -845,7 +926,12 @@
 
 lemma islimpt_conv_frequently_at:
   "x islimpt A \<longleftrightarrow> frequently (\<lambda>y. y \<in> A) (at x)"
-  unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast
+  by (simp add: frequently_def islimpt_iff_eventually)
+
+lemma frequently_at_imp_islimpt:
+  assumes "frequently (\<lambda>y. y \<in> A) (at x)"
+  shows   "x islimpt A"
+  by (simp add: assms islimpt_conv_frequently_at)  
 
 lemma interior_closed_Un_empty_interior:
   assumes cS: "closed S"
@@ -1350,52 +1436,6 @@
   qed
 qed
 
-(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
-lemma islimpt_sequential:
-  fixes x :: "'a::first_countable_topology"
-  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
-    (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  from countable_basis_at_decseq[of x] obtain A where A:
-      "\<And>i. open (A i)"
-      "\<And>i. x \<in> A i"
-      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
-    by blast
-  define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
-  {
-    fix n
-    from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
-      unfolding islimpt_def using A(1,2)[of n] by auto
-    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
-      unfolding f_def by (rule someI_ex)
-    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
-  }
-  then have "\<forall>n. f n \<in> S - {x}" by auto
-  moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
-  proof (rule topological_tendstoI)
-    fix S
-    assume "open S" "x \<in> S"
-    from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
-    show "eventually (\<lambda>x. f x \<in> S) sequentially"
-      by (auto elim!: eventually_mono)
-  qed
-  ultimately show ?rhs by fast
-next
-  assume ?rhs
-  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
-    by auto
-  show ?lhs
-    unfolding islimpt_def
-  proof safe
-    fix T
-    assume "open T" "x \<in> T"
-    from lim[THEN topological_tendstoD, OF this] f
-    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
-      unfolding eventually_sequentially by auto
-  qed
-qed
-
 text\<open>These are special for limits out of the same topological space.\<close>
 
 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -26,8 +26,18 @@
 lemma is_pole_tendsto:
   fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
   shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
-unfolding is_pole_def
-by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+  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 \<Rightarrow> 'b::real_normed_vector)"
+  shows "is_pole f z \<longleftrightarrow> is_pole (\<lambda>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 \<Rightarrow> 'b::real_normed_vector)"
+  shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+  by (metis is_pole_shift_0)
 
 lemma is_pole_inverse_holomorphic:
   assumes "open s"
@@ -71,6 +81,23 @@
   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]:
+  "c \<noteq> 0 \<Longrightarrow> is_pole (\<lambda>z. c * f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+proof
+  assume *: "c \<noteq> 0" "is_pole (\<lambda>z. c * f z) z"
+  have "is_pole (\<lambda>z. inverse c * (c * f z)) z" unfolding is_pole_def
+    by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+  thus "is_pole f z"
+    using *(1) by (simp add: field_simps)
+next
+  assume *: "c \<noteq> 0" "is_pole f z"
+  show "is_pole (\<lambda>z. c * f z) z" unfolding is_pole_def 
+    by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+qed
+
+lemma is_pole_uminus_iff [simp]: "is_pole (\<lambda>z. -f z :: 'a :: real_normed_field) z \<longleftrightarrow> 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 (\<lambda>z::complex. 1 / (z - a)) a"
   using is_pole_inverse_power[of 1 a] by simp
 
@@ -80,7 +107,7 @@
   shows   "is_pole (\<lambda>z. f z / g z) z"
 proof -
   have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
-    using assms filterlim_compose filterlim_inverse_at_infinity isCont_def 
+    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
@@ -113,6 +140,62 @@
 definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
   "isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
 
+lemma removable_singularity:
+  assumes "f holomorphic_on A - {x}" "open A"
+  assumes "f \<midarrow>x\<rightarrow> c"
+  shows   "(\<lambda>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 \<in> A"
+    show "(?g \<longlongrightarrow> ?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 \<longlongrightarrow> ?g y) (at y within A - {x})"
+        using False y by (auto simp: continuous_on_def)
+      also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?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 \<midarrow>x\<rightarrow> c"
+        by fact
+      also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y)"
+        by (intro filterlim_cong) (auto simp: eventually_at_filter)
+      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
+    by (rule no_isolated_singularity) (use assms in auto)
+qed
+
+lemma removable_singularity':
+  assumes "isolated_singularity_at f z"
+  assumes "f \<midarrow>z\<rightarrow> c"
+  shows   "(\<lambda>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 "(\<lambda>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:
@@ -137,7 +220,7 @@
       define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
       have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        using \<open>n>m\<close> 
+        using \<open>n>m\<close>
           by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
@@ -165,7 +248,7 @@
       define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
       have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
-        using \<open>m>n\<close> 
+        using \<open>m>n\<close>
         by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
@@ -272,7 +355,7 @@
     ultimately show ?thesis by auto
   qed
 
-  have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"  
+  have ?thesis when "\<exists>x. (f \<longlongrightarrow> 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"
@@ -312,7 +395,7 @@
     have "P f (-n) (inverse o g) r"
     proof -
       have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
-        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus 
+        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
             powr_minus that)
       then show ?thesis
         unfolding P_def comp_def
@@ -398,7 +481,7 @@
     have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
       using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
     then have "fp \<midarrow>z\<rightarrow> ?xx"
-      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff 
+      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
           powr_of_int that zero_less_nat_eq)
     then show ?thesis unfolding fp_def not_essential_def by auto
   qed
@@ -520,7 +603,7 @@
         using that by (auto intro!:tendsto_eq_intros)
       then have "fg \<midarrow>z\<rightarrow> 0"
         using Lim_transform_within[OF _ \<open>r1>0\<close>]
-        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq 
+        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
             singletonD that)
       then show ?thesis unfolding not_essential_def fg_def by auto
     qed
@@ -629,7 +712,7 @@
       using f_iso unfolding isolated_singularity_at_def by auto
     define d3 where "d3=min d1 d2"
     have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
-    moreover 
+    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}"
@@ -712,9 +795,114 @@
   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_shift:
+  assumes "isolated_singularity_at (\<lambda>x. f (x + w)) z"
+  shows   "isolated_singularity_at f (z + w)"
+proof -
+  from assms obtain r where r: "r > 0" and ana: "(\<lambda>x. f (x + w)) analytic_on ball z r - {z}"
+    unfolding isolated_singularity_at_def by blast
+  have "((\<lambda>x. f (x + w)) \<circ> (\<lambda>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) \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (x + w)) z"
+  using isolated_singularity_at_shift[of f w z]
+        isolated_singularity_at_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+  by (auto simp: algebra_simps)
+
+lemma isolated_singularity_at_shift_0:
+  "NO_MATCH 0 z \<Longrightarrow> isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at (\<lambda>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 (\<lambda>x. f (x + w)) z"
+  shows   "not_essential f (z + w)"
+proof -
+  from assms consider c where "(\<lambda>x. f (x + w)) \<midarrow>z\<rightarrow> c" | "is_pole (\<lambda>x. f (x + w)) z"
+    unfolding not_essential_def by blast
+  thus ?thesis
+  proof cases
+    case (1 c)
+    hence "f \<midarrow>z + w\<rightarrow> 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) \<longleftrightarrow> not_essential (\<lambda>x. f (x + w)) z"
+  using not_essential_shift[of f w z]
+        not_essential_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+  by (auto simp: algebra_simps)
+
+lemma not_essential_shift_0:
+  "NO_MATCH 0 z \<Longrightarrow> not_essential f z \<longleftrightarrow> not_essential (\<lambda>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 \<in> A" "open A"
+  shows   "not_essential f x"
+proof -
+  have "continuous_on A f"
+    using assms holomorphic_on_imp_continuous_on by blast
+  hence "f \<midarrow>x\<rightarrow> f x"
+    using assms continuous_on_eq_continuous_at isContD by blast
+  thus ?thesis
+    by (auto simp: not_essential_def)
+qed
+
+lemma eventually_not_pole:
+  assumes "isolated_singularity_at f z"
+  shows   "eventually (\<lambda>w. \<not>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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    by (intro eventually_at_in_open) auto
+  thus "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+  proof eventually_elim
+    case (elim w)
+    with r show ?case
+      using analytic_imp_holomorphic not_is_pole_holomorphic open_delete by blast
+  qed
+qed
+
+lemma not_islimpt_poles:
+  assumes "isolated_singularity_at f z"
+  shows   "\<not>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} \<Longrightarrow> \<not>is_pole f z"
+  using analytic_at not_is_pole_holomorphic by blast
+
+lemma not_essential_const [singularity_intros]: "not_essential (\<lambda>_. c) z"
+  unfolding not_essential_def by (rule exI[of _ c]) auto
+
+lemma not_essential_uminus [singularity_intros]:
+  assumes f_ness: "not_essential f z"
+  assumes f_iso:"isolated_singularity_at f z"
+  shows "not_essential (\<lambda>w. -f w) z"
+proof -
+  have "not_essential (\<lambda>w. -1 * f w) z"
+    by (intro assms singularity_intros)
+  thus ?thesis by simp
+qed
+
 subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
 
-
 definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
   "zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
                    \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n)
@@ -749,6 +937,29 @@
   then show ?thesis unfolding P_def by auto
 qed
 
+lemma zorder_shift:
+  shows  "zorder f z = zorder (\<lambda>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 (\<lambda>u. u-z)" in exI)
+    apply (rule_tac x="r" in exI)
+    apply (intro conjI holomorphic_on_compose holomorphic_intros)
+       apply (simp_all add: 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 \<Longrightarrow> zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+  by (rule zorder_shift)
+
 lemma
   fixes f::"complex \<Rightarrow> complex" and z::complex
   assumes f_iso:"isolated_singularity_at f z"
@@ -819,6 +1030,99 @@
     by (metis DiffI dist_commute mem_ball singletonD)
 qed
 
+lemma zor_poly_shift:
+  assumes iso1: "isolated_singularity_at f z"
+    and ness1: "not_essential f z"
+    and nzero1: "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+  shows "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\<lambda>u. f (z + u)) 0 (w-z)"
+proof -
+  obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
+      holo1:"zor_poly f z holomorphic_on cball z r1" and
+      rball1:"\<forall>w\<in>cball z r1 - {z}.
+           f w = zor_poly f z w * (w - z) powr of_int (zorder f z) \<and>
+           zor_poly f z w \<noteq> 0"
+    using zorder_exist[OF iso1 ness1 nzero1] by blast
+
+  define ff where "ff=(\<lambda>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 "\<exists>\<^sub>F w in at 0. ff w \<noteq> 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 \<noteq> 0" and
+      holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
+      rball2:"\<forall>w\<in>cball 0 r2 - {0}.
+           ff w = zor_poly ff 0 w * w powr of_int (zorder ff 0) \<and>
+           zor_poly ff 0 w \<noteq> 0"
+    using zorder_exist[of ff 0] by auto
+
+  define r where "r=min r1 r2"
+  have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
+
+  have "zor_poly f z w = zor_poly ff 0 (w - z)"
+    if "w\<in>ball z r - {z}" for w
+  proof -
+    define n::complex where "n= of_int (zorder f z)"
+
+    have "f w = zor_poly f z w * (w - z) powr n"
+    proof -
+      have "w\<in>cball z r1 - {z}"
+        using r_def that by auto
+      from rball1[rule_format, OF this]
+      show ?thesis unfolding n_def by auto
+    qed
+
+    moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powr n"
+    proof -
+      have "w-z\<in>cball 0 r2 - {0}"
+        using r_def that by (auto simp:dist_complex_def)
+      from rball2[rule_format, OF this]
+      have "ff (w - z) = zor_poly ff 0 (w - z) * (w - z)
+                            powr of_int (zorder ff 0)"
+        by simp
+      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) powr n
+                = zor_poly ff 0 (w - z) * (w - z) powr n"
+      by auto
+    moreover have "(w - z) powr n \<noteq>0"
+      using that by auto
+    ultimately show ?thesis
+      apply (subst (asm) mult_cancel_right)
+      by (simp add:ff_def)
+  qed
+  then have "\<forall>\<^sub>F w in at z. zor_poly f z w
+                  = zor_poly ff 0 (w - z)"
+    unfolding eventually_at
+    apply (rule_tac x=r in exI)
+    using \<open>r>0\<close> by (auto simp:dist_commute)
+  moreover have "isCont (zor_poly f z) z"
+    using holo1[THEN holomorphic_on_imp_continuous_on]
+    apply (elim continuous_on_interior)
+    using \<open>r1>0\<close> by auto
+  moreover have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+  proof -
+    have "isCont (zor_poly ff 0) 0"
+      using holo2[THEN holomorphic_on_imp_continuous_on]
+      apply (elim continuous_on_interior)
+      using \<open>r2>0\<close> by auto
+    then show ?thesis
+      unfolding isCont_iff by simp
+  qed
+  ultimately show "\<forall>\<^sub>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 \<Rightarrow> complex" and z::complex
   assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
@@ -979,7 +1283,7 @@
   have fz_lim: "f\<midarrow> z \<rightarrow> f z"
     by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
   have gz_lim: "g \<midarrow>z\<rightarrow>g z"
-    by (metis r open_ball at_within_open ball_subset_cball centre_in_ball 
+    by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
         continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on)
   have if_0:"if f z=0 then n > 0 else n=0"
   proof -
@@ -1185,7 +1489,7 @@
         unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
       moreover have "f z' \<noteq> 0"
       proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
-        have "z' \<in> cball z r" 
+        have "z' \<in> cball z r"
           unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
         then show " z' \<in> s" using r(2) by blast
         show "g z' * (z' - z) powr of_int n \<noteq> 0"
@@ -1493,4 +1797,476 @@
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
 qed
 
-end
\ No newline at end of file
+lemma
+  assumes "is_pole f (x :: complex)" "open A" "x \<in> A"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (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 \<subseteq> 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: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w - x) ^ nat (- zorder f x)"
+    using \<open>is_pole f x\<close> 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 \<subseteq> A" "P holomorphic_on cball x r" "zorder f x < 0" "P x \<noteq> 0"
+    "\<forall>w\<in>cball x r - {x}. f w = P w / (w - x) ^ n \<and> P w \<noteq> 0"
+    unfolding P_def n_def using zorder_exist_pole[OF holo assms(2,3,1)] 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 \<in> 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 = (\<lambda>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 (\<lambda>w. w \<in> ball x r) (nhds x)"
+    using \<open>r > 0\<close> by (intro eventually_nhds_in_open) auto
+  hence ev'': "eventually (\<lambda>w. w \<in> ball x r - {x}) (at x)"
+    by (auto simp: eventually_at_filter elim: eventually_mono)
+
+  {
+    fix w assume w: "w \<in> ball x r - {x}"
+    have ev': "eventually (\<lambda>w. w \<in> ball x r - {x}) (nhds w)"
+      using w by (intro eventually_nhds_in_open) auto
+
+    have "((\<lambda>w. P w / (w - x) ^ n) has_field_derivative D w) (at w)"
+      apply (rule derivative_eq_intros refl | use w in force)+
+      using w
+      apply (simp add: divide_simps D_def)
+      apply (simp add: n' algebra_simps)
+      done
+    also have "?this \<longleftrightarrow> (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 \<open>r > 0\<close> \<open>P x \<noteq> 0\<close>
+    by (intro is_pole_basic[where A = "ball x r"] holomorphic_intros holomorphic_on_subset[OF r(3)]) auto
+  also have "?this \<longleftrightarrow> 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 \<in> ball x r"
+      using \<open>r > 0\<close> by auto
+    show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powr of_int (- int (Suc n))"
+      if "w \<in> ball x r" "w \<noteq> x" for w
+      using that D_eq[of w] n by (auto simp: D_def powr_diff powr_minus powr_nat' divide_simps)
+  qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
+  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 \<in> ball x r" "open (ball x r)" "open (ball x r - {x})"
+    using \<open>r > 0\<close> by auto
+  show "is_pole (deriv f) x" "zorder (deriv f) x = zorder f x - 1"
+    by (rule is_pole_deriv' zorder_deriv', (rule assms * holomorphic_derivI holo | assumption)+)+
+qed
+
+lemma removable_singularity_deriv':
+  assumes "f \<midarrow>x\<rightarrow> c" "x \<in> A" "open (A :: complex set)"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+  shows   "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+proof -
+  have holo: "f holomorphic_on A - {x}"
+    using assms by (subst holomorphic_on_open) auto
+
+  define g where "g = (\<lambda>y. if y = x then c else f y)"
+  have deriv_g_eq: "deriv g y = f' y" if "y \<in> A - {x}" for y
+  proof -
+    have ev: "eventually (\<lambda>y. y \<in> 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 \<longleftrightarrow> (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 \<longlongrightarrow> deriv g x) (at x within A)"
+    using assms by (auto simp: continuous_on_def)
+  also have "?this \<longleftrightarrow> (f' \<longlongrightarrow> deriv g x) (at x within A)"
+    by (intro filterlim_cong refl) (auto simp: eventually_at_filter deriv_g_eq)
+  finally have "f' \<midarrow>x\<rightarrow> deriv g x"
+    using \<open>open A\<close> \<open>x \<in> A\<close> by (meson tendsto_within_open)
+  thus ?thesis
+    by blast
+qed
+
+lemma removable_singularity_deriv:
+  assumes "f \<midarrow>x\<rightarrow> c" "isolated_singularity_at f x"
+  shows   "\<exists>c. deriv f \<midarrow>x\<rightarrow> 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 \<in> ball x r" "open (ball x r)"
+      using \<open>r > 0\<close> by auto
+  qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_deriv':
+  assumes "not_essential f x" "x \<in> A" "open A"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (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 \<midarrow>x\<rightarrow> c"
+    by (auto simp: not_essential_def)
+  thus ?thesis
+  proof cases
+    case 1
+    hence "is_pole f' x"
+      using is_pole_deriv' assms by blast
+    thus ?thesis by (auto simp: not_essential_def)
+  next
+    case (2 c)
+    from 2 have "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+      by (rule removable_singularity_deriv'[OF _ assms(2-4)])
+    thus ?thesis
+      by (auto simp: not_essential_def)
+  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 \<in> ball x r" "open (ball x r)"
+      using \<open>r > 0\<close> by auto
+  qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_frequently_0_imp_tendsto_0:
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes sing: "isolated_singularity_at f z" "not_essential f z"
+  assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+  shows   "f \<midarrow>z\<rightarrow> 0"
+proof -
+  from freq obtain g :: "nat \<Rightarrow> complex" where g: "filterlim g (at z) at_top" "\<And>n. f (g n) = 0"
+    using frequently_atE by blast
+  have "eventually (\<lambda>x. f (g x) = 0) sequentially"
+    using g by auto
+  hence fg: "(\<lambda>x. f (g x)) \<longlonglongrightarrow> 0"
+    by (simp add: tendsto_eventually)
+
+  from assms(2) consider c where "f \<midarrow>z\<rightarrow> c" | "is_pole f z"
+    unfolding not_essential_def by blast
+  thus ?thesis
+  proof cases
+    case (1 c)
+    have "(\<lambda>x. f (g x)) \<longlonglongrightarrow> 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 (\<lambda>x. f (g x)) at_infinity sequentially"
+      by (rule filterlim_compose[OF _ g(1)]) (use 2 in \<open>auto simp: is_pole_def\<close>)
+    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 \<Rightarrow> complex"
+  assumes sing: "isolated_singularity_at f z" "not_essential f z"
+  assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+  shows   "eventually (\<lambda>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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    using r by (intro eventually_at_in_open) auto
+  from freq and this have "frequently (\<lambda>w. f w = 0 \<and> w \<in> ball z r - {z}) (at z)"
+    using frequently_eventually_frequently by blast
+  hence "frequently (\<lambda>w. w \<in> {w\<in>ball z r - {z}. f w = 0}) (at z)"
+    by (simp add: conj_commute)
+  hence limpt: "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+    using islimpt_conv_frequently_at by blast
+
+  define g where "g = (\<lambda>w. if w = z then 0 else f w)"
+  have "f \<midarrow>z\<rightarrow> 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 \<in> 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\<in>ball z r - {z}. f w = 0}"
+      by fact
+    show "g w = 0" if "w \<in> {w \<in> 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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    using r by (intro eventually_at_in_open) auto
+  thus "eventually (\<lambda>w. f w = 0) (at z)"
+  proof eventually_elim
+    case (elim w)
+    thus ?case using g_eq_0[of w]
+      by (auto simp: g_def)
+  qed
+qed
+
+lemma pole_imp_not_constant:
+  fixes f :: "'a :: {perfect_space} \<Rightarrow> _"
+  assumes "is_pole f x" "open A" "x \<in> A" "A \<subseteq> insert x B"
+  shows   "\<not>f constant_on B"
+proof
+  assume *: "f constant_on B"
+  then obtain c where c: "\<forall>x\<in>B. f x = c"
+    by (auto simp: constant_on_def)
+  have "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
+    using assms by (intro eventually_at_in_open) auto
+  hence "eventually (\<lambda>y. f y = c) (at x)"
+    by eventually_elim (use c assms in auto)
+  hence **: "f \<midarrow>x\<rightarrow> c"
+    by (simp add: tendsto_eventually)
+  show False
+    using not_tendsto_and_filterlim_at_infinity[OF _ ** assms(1)[unfolded is_pole_def]] by simp
+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:"\<exists>\<^sub>F w in at z. f w \<noteq> 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 "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
+       w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+    using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto
+
+  have "is_pole (\<lambda>w. P w * (w - z) powr of_int n) z"
+    unfolding is_pole_def
+  proof (rule tendsto_mult_filterlim_at_infinity)
+    show "P \<midarrow>z\<rightarrow> P z"
+      by (meson open_ball \<open>0 < r\<close> ball_subset_cball centre_in_ball
+          continuous_on_eq_continuous_at continuous_on_subset
+          holomorphic_on_imp_continuous_on isContD r_holo)
+    show "P z\<noteq>0" by (simp add: \<open>P z \<noteq> 0\<close>)
+
+    have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
+      apply (subst filterlim_inverse_at_iff[symmetric])
+      using \<open>n<0\<close>
+      by (auto intro!:tendsto_eq_intros filterlim_atI
+              simp add:eventually_at_filter)
+    then show "LIM x at z. (x - z) powr of_int n :> at_infinity"
+    proof (elim filterlim_mono_eventually)
+      have "inverse ((x - z) ^ nat (-n)) = (x - z) powr of_int n"
+        if "x\<noteq>z" for x
+        apply (subst powr_of_int)
+        using \<open>n<0\<close> using that by auto
+      then show "\<forall>\<^sub>F x in at z. inverse ((x - z) ^ nat (-n))
+                  = (x - z) powr of_int n"
+        by (simp add: eventually_at_filter)
+    qed auto
+  qed
+  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w - z) powr of_int n"
+    unfolding eventually_at_le
+    apply (rule exI[where x=r])
+    using w_Pn \<open>r>0\<close> by (simp add: dist_commute)
+  ultimately show ?thesis using is_pole_cong by fast
+qed
+
+lemma is_pole_divide_zorder:
+  fixes f g::"complex \<Rightarrow> 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: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
+      and z_less:"zorder f z < zorder g z"
+    shows "is_pole (\<lambda>z. f z / g z) z"
+proof -
+  define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
+                        and "fg=(\<lambda>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,folded fn_def gn_def fg_def] .
+    then show ?thesis
+      using z_less by (simp add: fn_def gn_def)
+  qed
+  moreover have "\<exists>\<^sub>F w in at z. fg w \<noteq> 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 "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+proof (rule ccontr)
+  assume "\<not> (\<exists>\<^sub>F w in at z.  deriv f w  * f w \<noteq> 0)"
+  then have "\<forall>\<^sub>F x in at z. deriv f x * f x = 0"
+    unfolding not_frequently by simp
+  moreover have "\<forall>\<^sub>F w in at z. f w \<noteq> 0"
+    using non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] .
+  moreover have "\<forall>\<^sub>F w in at z. deriv f w \<noteq> 0"
+    using is_pole_deriv[OF \<open>is_pole f z\<close> f_iso,THEN non_zero_neighbour_pole]
+    .
+  ultimately have "\<forall>\<^sub>F w in at z. False"
+    apply eventually_elim
+    by auto
+  then show False by auto
+qed
+
+lemma isolated_pole_imp_neg_zorder:
+  assumes f_iso:"isolated_singularity_at f z"
+    and "is_pole f z"
+  shows "zorder f z<0"
+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
+  show ?thesis
+    using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>]
+    by auto
+qed
+
+lemma isolated_singularity_at_deriv[singularity_intros]:
+  assumes "isolated_singularity_at f x"
+  shows "isolated_singularity_at (deriv f) x"
+proof -
+  obtain r where "r>0" "f analytic_on ball x r - {x}"
+    using assms unfolding isolated_singularity_at_def by auto
+  from analytic_deriv[OF this(2)]
+  have "deriv f analytic_on ball x r - {x}" .
+  with \<open>r>0\<close> show ?thesis
+    unfolding isolated_singularity_at_def by auto
+qed
+
+lemma zorder_deriv_minus_1:
+  fixes f g::"complex \<Rightarrow> complex" and z::complex
+  assumes f_iso:"isolated_singularity_at f z"
+      and f_ness:"not_essential f z"
+      and f_nconst:"\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+      and f_ord:"zorder f z \<noteq>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\<noteq>0" unfolding n_def using f_ord by auto
+
+  obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
+          and "(\<forall>w\<in>cball z r - {z}. f w
+                            = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+    using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
+  from this(4)
+  have f_eq:"(\<forall>w\<in>cball z r - {z}. f w
+                            = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+    using complex_powr_of_int f_ord n_def by presburger
+
+  define D where "D = (\<lambda>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 \<in> ball z r - {z}" for w
+  proof -
+    have ev': "eventually (\<lambda>w. w \<in> ball z r - {z}) (nhds w)"
+      using that by (intro eventually_nhds_in_open) auto
+
+    define wz where "wz = w - z"
+
+    have "wz \<noteq>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 "((\<lambda>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)
+      apply (fold wz_def)
+      by (auto simp:algebra_simps simp flip:power_int_add_1')
+    also have "?this \<longleftrightarrow> (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 \<in> ball z r"
+      using \<open>r > 0\<close> by auto
+    define g where "g=(\<lambda>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 \<noteq> 0"
+      unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
+    show "deriv f w =
+         (deriv P w * (w - z) + of_int n * P w) * (w - z) powr of_int (n - 1)"
+      if "w \<in> ball z r" "w \<noteq> z" for w
+      apply (subst complex_powr_of_int)
+      using deriv_f_eq that unfolding D_def by auto
+  qed
+qed
+
+end
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Complex_Analysis/Contour_Integration.thy
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -94,8 +94,6 @@
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path\<close>
 
-
-
 lemma has_contour_integral_reversepath:
   assumes "valid_path g" and f: "(f has_contour_integral i) g"
     shows "(f has_contour_integral (-i)) (reversepath g)"
@@ -807,9 +805,8 @@
 lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\<lambda>x. c) = c*(b - a)"
   by (rule contour_integral_unique [OF has_contour_integral_const_linepath])
 
-lemma contour_integral_neg:
-    "f contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. -(f x)) = -(contour_integral g f)"
-  by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)
+lemma contour_integral_neg: "contour_integral g (\<lambda>z. -f z) = -contour_integral g f"
+  by (simp add: contour_integral_integral)
 
 lemma contour_integral_add:
     "f1 contour_integrable_on g \<Longrightarrow> f2 contour_integrable_on g \<Longrightarrow> contour_integral g (\<lambda>x. f1 x + f2 x) =
@@ -903,6 +900,19 @@
    unfolding contour_integrable_on_def
    by (metis has_contour_integral_sum)
 
+lemma contour_integrable_lmul_iff:
+    "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+  using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "\<lambda>x. c * f x" g "inverse c"]
+  by (auto simp: field_simps)
+
+lemma contour_integrable_rmul_iff:
+    "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+  using contour_integrable_rmul[of f g c] contour_integrable_rmul[of "\<lambda>x. c * f x" g "inverse c"]
+  by (auto simp: field_simps)
+
+lemma contour_integrable_div_iff:
+    "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) contour_integrable_on g \<longleftrightarrow> f contour_integrable_on g"
+  using contour_integrable_rmul_iff[of "inverse c"] by (simp add: field_simps)
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Reversing a path integral\<close>
 
@@ -912,9 +922,9 @@
   using has_contour_integral_reversepath valid_path_linepath by fastforce
 
 lemma contour_integral_reverse_linepath:
-    "continuous_on (closed_segment a b) f
-     \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
-  by (metis contour_integrable_continuous_linepath contour_integral_unique has_contour_integral_integral has_contour_integral_reverse_linepath)
+    "continuous_on (closed_segment a b) f \<Longrightarrow> contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
+  using contour_integral_reversepath by fastforce
+
 
 
 text \<open>Splitting a path integral in a flat way.*)\<close>
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Complex_Analysis/Residue_Theorem.thy
--- a/src/HOL/Complex_Analysis/Residue_Theorem.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Residue_Theorem.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -454,9 +454,8 @@
 
 theorem argument_principle:
   fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set"
-  defines "pz \<equiv> {w. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
-  assumes "open s" and
-          "connected s" and
+  defines "pz \<equiv> {w\<in>s. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
+  assumes "open s" "connected s" and
           f_holo:"f holomorphic_on s-poles" and
           h_holo:"h holomorphic_on s" and
           "valid_path g" and
@@ -464,7 +463,7 @@
           path_img:"path_image g \<subseteq> s - pz" and
           homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
           finite:"finite pz" and
-          poles:"\<forall>p\<in>poles. is_pole f p"
+          poles:"\<forall>p\<in>s\<inter>poles. is_pole f p"
   shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> *
           (\<Sum>p\<in>pz. winding_number g p * h p * zorder f p)"
     (is "?L=?R")
@@ -505,10 +504,12 @@
           case False
           then have "p\<in>s-poles" using \<open>p\<in>s\<close> poles unfolding pz_def by auto
           moreover have "open (s-poles)"
-            using \<open>open s\<close>
-            apply (elim open_Diff)
-            apply (rule finite_imp_closed)
-            using finite unfolding pz_def by simp
+          proof -
+            have "closed (s \<inter> poles)"
+              using finite by (simp add: pz_def finite_imp_closed rev_finite_subset subset_eq)
+            then show ?thesis
+              by (metis Diff_Compl Diff_Diff_Int Diff_eq \<open>open s\<close> open_Diff) 
+          qed
           ultimately have "isCont f p"
             using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at
             by auto
@@ -518,13 +519,21 @@
         proof (rule ccontr)
           assume "\<not> (\<exists>\<^sub>F w in at p. f w \<noteq> 0)"
           then have "\<forall>\<^sub>F w in at p. f w= 0" unfolding frequently_def by auto
-          then obtain rr where "rr>0" "\<forall>w\<in>ball p rr - {p}. f w =0"
+          then obtain r1 where "r1>0" and r1:"\<forall>w\<in>ball p r1 - {p}. f w =0"
             unfolding eventually_at by (auto simp add:dist_commute)
-          then have "ball p rr - {p} \<subseteq> {w\<in>ball p rr-{p}. f w=0}" by blast
-          moreover have "infinite (ball p rr - {p})" using \<open>rr>0\<close> using finite_imp_not_open by fastforce
-          ultimately have "infinite {w\<in>ball p rr-{p}. f w=0}" using infinite_super by blast
+          obtain r2 where "r2>0" and r2: "ball p r2 \<subseteq> s"
+            using \<open>p\<in>s\<close> \<open>open s\<close> openE by blast
+          define rr where "rr=min r1 r2"
+
+          from r1 r2
+          have "ball p rr - {p} \<subseteq> {w\<in> s \<inter> ball p rr-{p}. f w=0}"
+            unfolding rr_def by auto
+          moreover have "infinite (ball p rr - {p})" 
+            using \<open>r1>0\<close> \<open>r2>0\<close> finite_imp_not_open 
+            unfolding rr_def by fastforce
+          ultimately have "infinite {w\<in>s \<inter> ball p rr-{p}. f w=0}" using infinite_super by blast
           then have "infinite pz"
-            unfolding pz_def infinite_super by auto
+            unfolding pz_def by (smt (verit) infinite_super Collect_mono_iff DiffE Int_iff)
           then show False using \<open>finite pz\<close> by auto
         qed
         ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r"
@@ -795,7 +804,7 @@
 theorem Rouche_theorem:
   fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
   defines "fg\<equiv>(\<lambda>p. f p + g p)"
-  defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
+  defines "zeros_fg\<equiv>{p\<in>s. fg p = 0}" and "zeros_f\<equiv>{p\<in>s. f p = 0}"
   assumes
     "open s" and "connected s" and
     "finite zeros_fg" and
@@ -844,9 +853,8 @@
     proof -
       have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p
       proof -
-        have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
-          apply (cases "cmod (f p) = 0")
-          by (auto simp add: norm_divide)
+        have "cmod (g p/f p) <1"
+          by (smt (verit) divide_less_eq_1_pos norm_divide norm_ge_zero path_less that)
         then show ?thesis unfolding h_def by (auto simp add:dist_complex_def)
       qed
       then have "path_image (h o \<gamma>) \<subseteq> ball 1 1"
@@ -935,9 +943,8 @@
         assume "\<not> h p \<noteq> 0"
         then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2)
         then have "cmod (g p/f p) = 1" by auto
-        moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
-          apply (cases "cmod (f p) = 0")
-          by (auto simp add: norm_divide)
+        moreover have "cmod (g p/f p) <1"
+          by (simp add: \<open>f p \<noteq> 0\<close> norm_divide path_less that)
         ultimately show False by auto
       qed
       have der_fg:"deriv fg p =  deriv f p + deriv g p" unfolding fg_def
@@ -963,20 +970,24 @@
     ultimately show ?thesis by auto
   qed
   moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
-    unfolding c_def zeros_fg_def w_def
-  proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
-        , of _ "{}" "\<lambda>_. 1",simplified])
-    show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
-    show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
-    show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+  proof -
+    have "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
+    moreover
+    have "path_image \<gamma> \<subseteq> s - {p\<in>s. fg p = 0}" using path_fg unfolding zeros_fg_def .
+    moreover
+    have " finite {p\<in>s. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
+    ultimately show ?thesis
+      unfolding c_def zeros_fg_def w_def
+      using argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1"]
+      by simp
   qed
   moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
     unfolding c_def zeros_f_def w_def
   proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
         , of _ "{}" "\<lambda>_. 1",simplified])
     show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
-    show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
-    show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
+    show "path_image \<gamma> \<subseteq> s - {p\<in>s. f p = 0}" using path_f unfolding zeros_f_def .
+    show " finite {p\<in>s. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
   qed
   ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
     by auto
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Filter.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -223,6 +223,16 @@
   shows "\<exists>\<^sub>Fx in F. Q x \<and> P x"
   using assms eventually_elim2 by (force simp add: frequently_def)
 
+lemma frequently_cong:
+  assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+  shows   "frequently Q F \<longleftrightarrow> frequently R F"
+  unfolding frequently_def 
+  using QR by (auto intro!: eventually_cong [OF ev])
+
+lemma frequently_eventually_frequently:
+  "frequently P F \<Longrightarrow> eventually Q F \<Longrightarrow> frequently (\<lambda>x. P x \<and> Q x) F"
+  using frequently_cong [of Q F P "\<lambda>x. P x \<and> Q x"] by meson
+  
 lemma eventually_frequently_const_simps:
   "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
   "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
@@ -606,12 +616,6 @@
 lemma filtermap_INF: "filtermap f (\<Sqinter>b\<in>B. F b) \<le> (\<Sqinter>b\<in>B. filtermap f (F b))"
   by (rule INF_greatest, rule filtermap_mono, erule INF_lower)
 
-lemma frequently_cong:
-  assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
-  shows   "frequently Q F \<longleftrightarrow> frequently R F"
-  unfolding frequently_def 
-  using QR by (auto intro!: eventually_cong [OF ev])
-
 lemma frequently_filtermap:
   "frequently P (filtermap f F) = frequently (\<lambda>x. P (f x)) F"
   by (simp add: frequently_def eventually_filtermap)
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Topological_Spaces.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -1078,6 +1078,37 @@
 lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
 
+lemma Lim_cong:
+  assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
+  shows   "Lim F f = Lim G g"
+proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
+  case True
+  then obtain c where c: "(f \<longlongrightarrow> c) F"
+    by blast
+  hence "Lim F f = c"
+    using True by (intro tendsto_Lim) auto
+  moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
+    using assms by (intro filterlim_cong) auto
+  with True c assms have "Lim G g = c"
+    by (intro tendsto_Lim) auto
+  ultimately show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof (cases "F = bot")
+    case True
+    thus ?thesis using assms
+      by (auto simp: Topological_Spaces.Lim_def)
+  next
+    case False
+    have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
+      using assms by (intro filterlim_cong) auto
+    thus ?thesis
+      by (auto simp: Topological_Spaces.Lim_def)
+  qed
+qed
+
 lemma eventually_Lim_ident_at:
   "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
     (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
@@ -2217,6 +2248,18 @@
   "continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
   by (auto simp: continuous_on_def at_discrete)
 
+lemma continuous_on_of_nat [continuous_intros]:
+  assumes "continuous_on A f"
+  shows   "continuous_on A (\<lambda>n. of_nat (f n))"
+  using continuous_on_compose[OF assms continuous_on_discrete[of _ of_nat]]
+  by (simp add: o_def)
+
+lemma continuous_on_of_int [continuous_intros]:
+  assumes "continuous_on A f"
+  shows   "continuous_on A (\<lambda>n. of_int (f n))"
+  using continuous_on_compose[OF assms continuous_on_discrete[of _ of_int]]
+  by (simp add: o_def)
+
 subsubsection \<open>Continuity at a point\<close>
 
 definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
@@ -2330,6 +2373,21 @@
   "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
   using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
 
+lemma at_within_isCont_imp_nhds:
+  fixes f:: "'a:: {t2_space,perfect_space} \<Rightarrow> 'b:: t2_space"
+  assumes "\<forall>\<^sub>F w in at z. f w = g w" "isCont f z" "isCont g z"
+  shows "\<forall>\<^sub>F w in nhds z. f w = g w"
+proof -
+  have "g \<midarrow>z\<rightarrow> f z"
+    using assms isContD tendsto_cong by blast 
+  moreover have "g \<midarrow>z\<rightarrow> g z" using \<open>isCont g z\<close> using isCont_def by blast
+  ultimately have "f z=g z" using LIM_unique by auto
+  moreover have "\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> f x = g x"
+    using assms unfolding eventually_at_filter by auto
+  ultimately show ?thesis 
+    by (auto elim:eventually_mono)
+qed
+
 lemma filtermap_nhds_open_map':
   assumes cont: "isCont f a"
     and "open A" "a \<in> A"
@@ -2933,6 +2991,30 @@
     by auto
 qed
 
+lemma connected_Un_UN:
+  assumes "connected A" "\<And>X. X \<in> B \<Longrightarrow> connected X" "\<And>X. X \<in> B \<Longrightarrow> A \<inter> X \<noteq> {}"
+  shows   "connected (A \<union> \<Union>B)"
+proof (rule connectedI_const)
+  fix f :: "'a \<Rightarrow> bool"
+  assume f: "continuous_on (A \<union> \<Union>B) f"
+  have "connected A" "continuous_on A f"
+    by (auto intro: assms continuous_on_subset[OF f(1)])
+  from connectedD_const[OF this] obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+    by metis
+  have "f x = c" if "x \<in> X" "X \<in> B" for x X
+  proof -
+    have "connected X" "continuous_on X f"
+      using that by (auto intro: assms continuous_on_subset[OF f])
+    from connectedD_const[OF this] obtain c' where c': "\<And>x. x \<in> X \<Longrightarrow> f x = c'"
+      by metis
+    from assms(3) and that obtain y where "y \<in> A \<inter> X"
+      by auto
+    with c[of y] c'[of y] c'[of x] that show ?thesis
+      by auto
+  qed
+  with c show "\<exists>c. \<forall>x\<in>A \<union> \<Union> B. f x = c"
+    by (intro exI[of _ c]) auto
+qed   
 
 section \<open>Linear Continuum Topologies\<close>
 
@@ -3885,5 +3967,4 @@
   then show ?thesis using open_subdiagonal closed_Diff by auto
 qed
 
-
 end