# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1737584547 0
# Node ID 1171ea4a23e4c7c13ef23012c092213b434a7e52
# Parent  067462a6a652b001b2dbd0f41f8f6b7ded04bfde
more tidying

diff -r 067462a6a652 -r 1171ea4a23e4 src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Sun Jan 19 18:18:07 2025 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Wed Jan 22 22:22:27 2025 +0000
@@ -4,9 +4,9 @@
 
 subsection \<open>Non-essential singular points\<close>
 
-definition\<^marker>\<open>tag important\<close> is_pole ::
-  "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
-  "is_pole f a =  (LIM x (at a). f x :> at_infinity)"
+definition\<^marker>\<open>tag important\<close>
+  is_pole :: "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" 
+  where "is_pole f a =  (LIM x (at a). f x :> at_infinity)"
 
 lemma is_pole_cong:
   assumes "eventually (\<lambda>x. f x = g x) (at a)" "a=b"
@@ -24,10 +24,10 @@
   by (metis add_diff_cancel_right' filterlim_shift_iff is_pole_def)
 
 lemma is_pole_tendsto:
-  fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
+  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)
+  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)"
@@ -46,9 +46,9 @@
 
 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:"\<forall>x\<in>s-{z}. f x\<noteq>0"
+    and f_holo: "f holomorphic_on (s-{z})"
+    and pole: "is_pole f z"
+    and non_z: "\<forall>x\<in>s-{z}. f x\<noteq>0"
   shows "(\<lambda>x. if x=z then 0 else inverse (f x)) holomorphic_on s"
 proof -
   define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
@@ -56,14 +56,14 @@
     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)
+    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>open s\<close>] \<open>open s\<close>
-    by (auto simp add:continuous_on_eq_continuous_at)
+    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)
+    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>open s\<close>
@@ -125,15 +125,15 @@
 
 lemma is_pole_basic:
   assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0"
-  shows   "is_pole (\<lambda>w. f w / (w - z) ^ n) z"
+  shows   "is_pole (\<lambda>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 (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)"
+  have "filterlim (\<lambda>w. (w-z) ^ n) (nhds 0) (at z)"
     using assms by (auto intro!: tendsto_eq_intros)
-  thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)"
+  thus "filterlim (\<lambda>w. (w-z) ^ n) (at 0) (at z)"
     by (intro filterlim_atI tendsto_eq_intros)
-       (insert assms, auto simp: eventually_at_filter)
+       (use assms in \<open>auto simp: eventually_at_filter\<close>)
 qed fact+
 
 lemma is_pole_basic':
@@ -161,7 +161,7 @@
   then have "filterlim (\<lambda>x. f x + c) at_infinity (at z)" 
     unfolding is_pole_def .
   moreover have "((\<lambda>_. -c) \<longlongrightarrow> -c) (at z)" by auto
-  ultimately have " LIM x (at z). f x :> at_infinity"
+  ultimately have "LIM x (at z). f x :> at_infinity"
     using tendsto_add_filterlim_at_infinity'[of "(\<lambda>x. f x + c)"
         "at z" "(\<lambda>_. - c)" "-c"] 
     by auto
@@ -237,11 +237,11 @@
     unfolding islimpt_sequential by blast
   then have "(f \<circ> g) \<longlonglongrightarrow> c"
     by (simp add: tendsto_eventually)
-  moreover have *: "filterlim g (at z) sequentially"
+  moreover have "filterlim g (at z) sequentially"
     using g by (auto simp: filterlim_at)
-  have "filterlim (f \<circ> g) at_infinity sequentially"
-    unfolding o_def by (rule filterlim_compose [OF _ *])
-                       (use \<open>is_pole f z\<close> in \<open>simp add: is_pole_def\<close>)
+  then have "filterlim (f \<circ> g) at_infinity sequentially"
+    unfolding o_def
+    using \<open>is_pole f z\<close> filterlim_compose is_pole_def by blast
   ultimately show False
     using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
 qed
@@ -250,10 +250,10 @@
               \<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
 can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
 (i.e. the singularity is either removable or a pole).\<close>
-definition not_essential::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
+definition not_essential:: "[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
   "not_essential f z = (\<exists>x. f\<midarrow>z\<rightarrow>x \<or> is_pole f z)"
 
-definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
+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 not_essential_cong:
@@ -322,7 +322,7 @@
       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)
+        by (simp add: LIM_equal)
       finally show ?thesis
         by (meson Lim_at_imp_Lim_at_within)
     qed
@@ -332,7 +332,7 @@
       using assms(1) holomorphic_transform by fastforce
   }
   ultimately show ?thesis
-    by (rule no_isolated_singularity) (use assms in auto)
+    using assms by (simp add: no_isolated_singularity)
 qed
 
 lemma removable_singularity':
@@ -354,18 +354,18 @@
 named_theorems singularity_intros "introduction rules for singularities"
 
 lemma holomorphic_factor_unique:
-  fixes f::"complex \<Rightarrow> complex" and z::complex and r::real and m n::int
+  fixes f:: "complex \<Rightarrow> complex" and z::complex and r::real and m n::int
   assumes "r>0" "g z\<noteq>0" "h z\<noteq>0"
-    and asm:"\<forall>w\<in>ball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0 \<and> f w =  h w * (w - z) powi m \<and> h w\<noteq>0"
-    and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r"
+    and asm: "\<forall>w\<in>ball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0 \<and> f w =  h w * (w-z) powi m \<and> h w\<noteq>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 \<noteq> bot" using \<open>r>0\<close>
-      by (auto simp add:at_within_ball_bot_iff)
+  have [simp]: "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
+      by (auto simp add: at_within_ball_bot_iff)
   have False when "n>m"
   proof -
     have "(h \<longlongrightarrow> 0) (at z within ball z r)"
-    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powi (n - m) * g w"])
+    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (n - m) * g w"])
       have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powi(n-m) * g w"
         using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps power_int_diff) force
       then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
@@ -386,16 +386,16 @@
     qed
     moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)"
       using holomorphic_on_imp_continuous_on[OF h_holo]
-      by (auto simp add:continuous_on_def \<open>r>0\<close>)
+      by (auto simp add: continuous_on_def \<open>r>0\<close>)
     ultimately have "h z=0" by (auto intro!: tendsto_unique)
     thus False using \<open>h z\<noteq>0\<close> by auto
   qed
   moreover have False when "m>n"
   proof -
     have "(g \<longlongrightarrow> 0) (at z within ball z r)"
-    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powi (m - n) * h w"])
+    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (m - n) * h w"])
       have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powi (m-n) * h w" using \<open>m>n\<close> asm
-        by (simp add:field_simps power_int_diff) force
+        by (simp add: field_simps power_int_diff) force
       then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
             \<Longrightarrow> (x' - z) powi (m - n) * h x' = g x'" for x' by auto
     next
@@ -414,7 +414,7 @@
     qed
     moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)"
       using holomorphic_on_imp_continuous_on[OF g_holo]
-      by (auto simp add:continuous_on_def \<open>r>0\<close>)
+      by (auto simp add: continuous_on_def \<open>r>0\<close>)
     ultimately have "g z=0" by (auto intro!: tendsto_unique)
     thus False using \<open>g z\<noteq>0\<close> by auto
   qed
@@ -422,19 +422,19 @@
 qed
 
 lemma holomorphic_factor_puncture:
-  assumes f_iso:"isolated_singularity_at f z"
+  assumes f_iso: "isolated_singularity_at f z"
       and "not_essential f z" \<comment> \<open>\<^term>\<open>f\<close> has either a removable singularity or a pole at \<^term>\<open>z\<close>\<close>
-      and non_zero:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" \<comment> \<open>\<^term>\<open>f\<close> will not be constantly zero in a neighbour of \<^term>\<open>z\<close>\<close>
+      and non_zero: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0" \<comment> \<open>\<^term>\<open>f\<close> will not be constantly zero in a neighbour of \<^term>\<open>z\<close>\<close>
   shows "\<exists>!n::int. \<exists>g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
           \<and> (\<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0)"
 proof -
   define P where "P = (\<lambda>f n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
           \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n  \<and> g w\<noteq>0))"
-  have imp_unique:"\<exists>!n::int. \<exists>g r. P f n g r" when "\<exists>n g r. P f n g r"
+  have imp_unique: "\<exists>!n::int. \<exists>g r. P f n g r" when "\<exists>n g r. P f n g r"
   proof (rule ex_ex1I[OF that])
     fix n1 n2 :: int
-    assume g1_asm:"\<exists>g1 r1. P f n1 g1 r1" and g2_asm:"\<exists>g2 r2. P f n2 g2 r2"
-    define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r-{z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0"
+    assume g1_asm: "\<exists>g1 r1. P f n1 g1 r1" and g2_asm: "\<exists>g2 r2. P f n2 g2 r2"
+    define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0"
     obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z\<noteq>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\<noteq>0"
@@ -442,16 +442,16 @@
     define r where "r \<equiv> min r1 r2"
     have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
     moreover have "\<forall>w\<in>ball z r-{z}. f w = g1 w * (w-z) powi n1 \<and> g1 w\<noteq>0
-        \<and> f w = g2 w * (w - z) powi n2  \<and> g2 w\<noteq>0"
+        \<and> f w = g2 w * (w-z) powi n2  \<and> g2 w\<noteq>0"
       using \<open>fac n1 g1 r1\<close> \<open>fac n2 g2 r2\<close>   unfolding fac_def r_def
       by fastforce
     ultimately show "n1=n2" 
       using g1_holo g2_holo \<open>g1 z\<noteq>0\<close> \<open>g2 z\<noteq>0\<close>
       apply (elim holomorphic_factor_unique)
-      by (auto simp add:r_def)
+      by (auto simp add: r_def)
   qed
 
-  have P_exist:"\<exists> n g r. P h n g r" when
+  have P_exist: "\<exists> n g r. P h n g r" when
       "\<exists>z'. (h \<longlongrightarrow> z') (at z)" "isolated_singularity_at h z"  "\<exists>\<^sub>Fw in (at z). h w\<noteq>0"
     for h
   proof -
@@ -474,16 +474,16 @@
         by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that)
       moreover note \<open>h' holomorphic_on ball z r\<close>
       ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \<subseteq> ball z r" and
-          g:"g holomorphic_on ball z r1"
-          "\<And>w. w \<in> ball z r1 \<Longrightarrow> h' w = (w - z) ^ n * g w"
+          g: "g holomorphic_on ball z r1"
+          "\<And>w. w \<in> ball z r1 \<Longrightarrow> h' w = (w-z) ^ n * g w"
           "\<And>w. w \<in> ball z r1 \<Longrightarrow> g w \<noteq> 0"
         using holomorphic_factor_zero_nonconstant[of _ "ball z r" z thesis,simplified,
                 OF \<open>h' holomorphic_on ball z r\<close> \<open>r>0\<close> \<open>h' z=0\<close> \<open>\<not> h' constant_on ball z r\<close>]
-        by (auto simp add:dist_commute)
+        by (auto simp add: dist_commute)
       define rr where "rr=r1/2"
       have "P h' n g rr"
         unfolding P_def rr_def
-        using \<open>n>0\<close> \<open>r1>0\<close> g by (auto simp add:powr_nat)
+        using \<open>n>0\<close> \<open>r1>0\<close> 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
@@ -495,7 +495,7 @@
       proof -
         have "isCont h' z" "h' z\<noteq>0"
           by (auto simp add: Lim_cong_within \<open>h \<midarrow>z\<rightarrow> z'\<close> \<open>z'\<noteq>0\<close> continuous_at h'_def)
-        then obtain r2 where r2:"r2>0" "\<forall>x\<in>ball z r2. h' x\<noteq>0"
+        then obtain r2 where r2: "r2>0" "\<forall>x\<in>ball z r2. h' x\<noteq>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 \<subseteq> ball z r"
@@ -516,14 +516,14 @@
     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: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0"
+    obtain e where [simp]: "e>0" and e_holo: "f holomorphic_on ball z e - {z}" and e_nz: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0"
     proof -
       have "\<forall>\<^sub>F z in at z. f z \<noteq> 0"
         using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def
         by auto
-      then obtain e1 where e1:"e1>0" "\<forall>x\<in>ball z e1-{z}. f x\<noteq>0"
-        using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add:dist_commute)
-      obtain e2 where e2:"e2>0" "f holomorphic_on ball z e2 - {z}"
+      then obtain e1 where e1: "e1>0" "\<forall>x\<in>ball z e1-{z}. f x\<noteq>0"
+        using that eventually_at[of "\<lambda>x. f x\<noteq>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"])
@@ -545,22 +545,23 @@
     qed
     then obtain n g r
       where "0 < r" and
-            g_holo:"g holomorphic_on cball z r" and "g z\<noteq>0" and
-            g_fac:"(\<forall>w\<in>cball z r-{z}. h w = g w * (w - z) powi n  \<and> g w \<noteq> 0)"
+            g_holo: "g holomorphic_on cball z r" and "g z\<noteq>0" and
+            g_fac: "(\<forall>w\<in>cball z r-{z}. h w = g w * (w-z) powi n  \<and> g w \<noteq> 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\<in>cball z r - {z}" for w
+      have "f w = inverse (g w) * (w-z) powi (- n)" when "w\<in>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 \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro:holomorphic_intros)
+        using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro: holomorphic_intros)
     qed
     then show "\<exists>x g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z \<noteq> 0
-                  \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi x  \<and> g w \<noteq> 0)"
+                  \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi x  \<and> g w \<noteq> 0)"
       unfolding P_def by blast
   qed
-  ultimately show ?thesis using \<open>not_essential f z\<close> unfolding not_essential_def  by presburger
+  ultimately show ?thesis 
+    using \<open>not_essential f z\<close> unfolding not_essential_def by presburger
 qed
 
 lemma not_essential_transform:
@@ -631,9 +632,9 @@
 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}"
+  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:"\<forall>w. w \<noteq> z \<and> dist w z < r2 \<longrightarrow> f w \<noteq> 0"
+  obtain r2 where "r2>0" and r2: "\<forall>w. w \<noteq> z \<and> dist w z < r2 \<longrightarrow> f w \<noteq> 0"
     using assms(2) unfolding eventually_at by auto
   define r3 where "r3=min r1 r2"
   have "(\<lambda>w. (f w) powi n) holomorphic_on ball z r3 - {z}"
@@ -644,20 +645,21 @@
 qed
 
 lemma non_zero_neighbour:
-  assumes f_iso:"isolated_singularity_at f z"
-      and f_ness:"not_essential f z"
-      and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+  assumes f_iso: "isolated_singularity_at f z"
+      and f_ness: "not_essential f z"
+      and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
     shows "\<forall>\<^sub>F w in (at z). f w\<noteq>0"
 proof -
-  obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
-          and fr: "fp holomorphic_on cball z fr"
-                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
-    using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto
+  obtain fn fp fr
+    where [simp]: "fp z \<noteq> 0" and "fr > 0"
+      and fr: "fp holomorphic_on cball z fr"
+              "\<And>w. w \<in> cball z fr - {z} \<Longrightarrow> f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
+    using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
   have "f w \<noteq> 0" when " w \<noteq> z" "dist w z < fr" for w
   proof -
-    have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
-      using fr(2)[rule_format, of w] using that by (auto simp add:dist_commute)
-    moreover have "(w - z) powi fn \<noteq>0"
+    have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
+      using fr that by (auto simp add: dist_commute)
+    moreover have "(w-z) powi fn \<noteq>0"
       unfolding powr_eq_0_iff using \<open>w\<noteq>z\<close> by auto
     ultimately show ?thesis by auto
   qed
@@ -682,18 +684,18 @@
     by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
 next
   case False
-  obtain r1 where r1:"r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0"
-    using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at
+  obtain r1 where r1: "r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 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 \<subseteq> S"
+  obtain r2 where r2: "r2>0" "ball z r2 \<subseteq> S"
     using assms openE by blast
   show ?thesis unfolding eventually_at
-    by (metis (no_types) dist_commute dual_order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
+    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"
+  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 (\<lambda>w. f w * g w) z"
 proof -
   define fg where "fg = (\<lambda>w. f w * g w)"
@@ -704,41 +706,40 @@
     from tendsto_cong[OF this] have "fg \<midarrow>z\<rightarrow>0" by auto
     then show ?thesis unfolding not_essential_def fg_def by auto
   qed
-  moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" and g_nconst:"\<exists>\<^sub>Fw in (at z). g w\<noteq>0"
+  moreover have ?thesis when f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0" and g_nconst: "\<exists>\<^sub>Fw in (at z). g w\<noteq>0"
   proof -
-    obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+    obtain fn fp fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
           and fr: "fp holomorphic_on cball z fr"
-                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
-      using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto
-    obtain gn gp gr where [simp]:"gp z \<noteq> 0" and "gr > 0"
+                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
+      using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
+    obtain gn gp gr where [simp]: "gp z \<noteq> 0" and "gr > 0"
           and gr: "gp holomorphic_on cball z gr"
-                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powi gn \<and> gp w \<noteq> 0"
-      using holomorphic_factor_puncture[OF g_iso g_ness g_nconst,THEN ex1_implies_ex] by auto
+                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w-z) powi gn \<and> gp w \<noteq> 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  \<open>fr>0\<close> \<open>gr>0\<close> by auto
-    have fg_times:"fg w = (fp w * gp w) * (w - z) powi (fn+gn)" and fgp_nz:"fp w*gp w\<noteq>0"
+    have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\<noteq>0"
       when "w\<in>ball z r1 - {z}" for w
     proof -
-      have "f w = fp w * (w - z) powi fn" "fp w\<noteq>0"
-        using fr(2)[rule_format,of w] that unfolding r1_def by auto
-      moreover have "g w = gp w * (w - z) powi gn" "gp w \<noteq> 0"
-        using gr(2)[rule_format, of w] that unfolding r1_def by auto
-      ultimately show "fg w = (fp w * gp w) * (w - z) powi (fn+gn)" "fp w*gp w\<noteq>0"
-        using that unfolding fg_def by (auto simp add:power_int_add)
+      have "f w = fp w * (w-z) powi fn" "fp w\<noteq>0"
+        using fr that unfolding r1_def by auto
+      moreover have "g w = gp w * (w-z) powi gn" "gp w \<noteq> 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\<noteq>0"
+        using that by (auto simp add: fg_def power_int_add)
     qed
 
-    have [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z"
+    obtain [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z"
         using fr(1) \<open>fr>0\<close> gr(1) \<open>gr>0\<close>
-        by (meson open_ball ball_subset_cball centre_in_ball
-            continuous_on_eq_continuous_at continuous_within holomorphic_on_imp_continuous_on
-            holomorphic_on_subset)+
+        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 "(\<lambda>w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
+      have "(\<lambda>w. (fp w * gp w) * (w-z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0"
         using that by (auto intro!:tendsto_eq_intros)
       then have "fg \<midarrow>z\<rightarrow> 0"
-         apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
+        using Lim_transform_within[OF _ \<open>r1>0\<close>]
         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
@@ -749,7 +750,7 @@
       then have "fg \<midarrow>z\<rightarrow> fp z*gp z"
         apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
         apply (subst fg_times)
-        by (auto simp add:dist_commute that)
+        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"
@@ -773,28 +774,26 @@
 qed
 
 lemma not_essential_inverse[singularity_intros]:
-  assumes f_ness:"not_essential f z"
-  assumes f_iso:"isolated_singularity_at f z"
+  assumes f_ness: "not_essential f z"
+  assumes f_iso: "isolated_singularity_at f z"
   shows "not_essential (\<lambda>w. inverse (f w)) z"
 proof -
   define vf where "vf = (\<lambda>w. inverse (f w))"
   have ?thesis when "\<not>(\<exists>\<^sub>Fw in (at z). f w\<noteq>0)"
   proof -
     have "\<forall>\<^sub>Fw in (at z). f w=0"
-      using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
+      using not_eventually that by fastforce
     then have "vf \<midarrow>z\<rightarrow>0" 
       unfolding vf_def by (simp add: tendsto_eventually)
-    then show ?thesis unfolding not_essential_def vf_def by auto
+    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 "\<exists>x. f\<midarrow>z\<rightarrow>x " and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
   proof -
-    have "vf \<midarrow>z\<rightarrow>0"
-      using that filterlim_at filterlim_inverse_at_iff unfolding is_pole_def vf_def by blast
-    then show ?thesis unfolding not_essential_def vf_def by auto
-  qed
-  moreover have ?thesis when "\<exists>x. f\<midarrow>z\<rightarrow>x " and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
-  proof -
-    from that obtain fz where fz:"f\<midarrow>z\<rightarrow>fz" by auto
+    from that obtain fz where fz: "f\<midarrow>z\<rightarrow>fz" by auto
     have ?thesis when "fz=0"
 
     proof -
@@ -814,8 +813,8 @@
 qed
 
 lemma isolated_singularity_at_inverse[singularity_intros]:
-  assumes f_iso:"isolated_singularity_at f z"
-      and f_ness:"not_essential f z"
+  assumes f_iso: "isolated_singularity_at f z"
+      and f_ness: "not_essential f z"
   shows "isolated_singularity_at (\<lambda>w. inverse (f w)) z"
 proof -
   define vf where "vf = (\<lambda>w. inverse (f w))"
@@ -825,21 +824,22 @@
       using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
     then have "\<forall>\<^sub>Fw in (at z). vf w=0"
       unfolding vf_def by auto
-    then obtain d1 where "d1>0" and d1:"\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> vf x = 0"
+    then obtain d1 where "d1>0" and d1: "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> vf x = 0"
       unfolding eventually_at by auto
     then have "vf holomorphic_on ball z d1-{z}"
-      apply (rule_tac holomorphic_transform[of "\<lambda>_. 0"])
-      by (auto simp add:dist_commute)
+      using holomorphic_transform[of "\<lambda>_. 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 \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto
+    then show ?thesis 
+      using \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto
   qed
-  moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+  moreover have ?thesis when f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
   proof -
     have "\<forall>\<^sub>F w in at z. f w \<noteq> 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] .
-    then obtain d1 where d1:"d1>0" "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> f x \<noteq> 0"
+    then obtain d1 where d1: "d1>0" "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> f x \<noteq> 0"
       unfolding eventually_at by auto
-    obtain d2 where "d2>0" and d2:"f analytic_on ball z d2 - {z}"
+    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 \<open>d1>0\<close> \<open>d2>0\<close> by auto
@@ -849,31 +849,33 @@
     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
+    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"
+  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 (\<lambda>w. f w / g w) z"
 proof -
   have "not_essential (\<lambda>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)
+    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"
+  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 (\<lambda>w. f w * g w) z"
       and isolated_singularity_at_add[singularity_intros]:
               "isolated_singularity_at (\<lambda>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}"
+      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 \<open>d1>0\<close> \<open>d2>0\<close> by auto
@@ -893,7 +895,7 @@
 qed
 
 lemma isolated_singularity_at_uminus[singularity_intros]:
-  assumes f_iso:"isolated_singularity_at f z"
+  assumes f_iso: "isolated_singularity_at f z"
   shows "isolated_singularity_at (\<lambda>w. - f w) z"
   using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast
 
@@ -1044,7 +1046,7 @@
 
 lemma not_essential_uminus [singularity_intros]:
   assumes f_ness: "not_essential f z"
-  assumes f_iso:"isolated_singularity_at 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"
@@ -1065,17 +1067,17 @@
                    \<and> h w \<noteq>0)))"
 
 definition\<^marker>\<open>tag important\<close> zor_poly
-    ::"[complex \<Rightarrow> complex, complex] \<Rightarrow> complex \<Rightarrow> complex" where
+    :: "[complex \<Rightarrow> complex, complex] \<Rightarrow> complex \<Rightarrow> complex" where
   "zor_poly f z = (SOME h. \<exists>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) powi (zorder f z)
+                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powi (zorder f z)
                    \<and> h w \<noteq>0))"
 
 lemma zorder_exist:
-  fixes f::"complex \<Rightarrow> complex" and z::complex
+  fixes f:: "complex \<Rightarrow> complex" and z::complex
   defines "n \<equiv> zorder f z" and "g \<equiv> zor_poly f z"
-  assumes f_iso:"isolated_singularity_at f z"
-      and f_ness:"not_essential f z"
-      and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
+  assumes f_iso: "isolated_singularity_at f z"
+      and f_ness: "not_essential f z"
+      and f_nconst: "\<exists>\<^sub>Fw in (at z). f w\<noteq>0"
   shows "g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> g holomorphic_on cball z r
     \<and> (\<forall>w\<in>cball z r - {z}. f w  = g w * (w-z) powi n  \<and> g w \<noteq>0))"
 proof -
@@ -1084,13 +1086,13 @@
   have "\<exists>!k. \<exists>g r. P k g r"
     using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
   then have "\<exists>g r. P n g r"
-    unfolding n_def P_def zorder_def
-    by (drule_tac theI',argo)
+    unfolding n_def P_def zorder_def by (rule theI')
   then have "\<exists>r. P n g r"
-    unfolding P_def zor_poly_def g_def n_def
-    by (drule_tac someI_ex,argo)
-  then obtain r1 where "P n g r1" by auto
-  then show ?thesis unfolding P_def by auto
+    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:
@@ -1109,7 +1111,7 @@
     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)
+       apply (simp_all flip: cball_translation_subtract)
     by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
   done
 
@@ -1117,10 +1119,10 @@
   by (rule zorder_shift)
 
 lemma
-  fixes f::"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>Fw in (at z). f w\<noteq>0"
+  fixes f:: "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>Fw in (at z). f w\<noteq>0"
     shows zorder_inverse: "zorder (\<lambda>w. inverse (f w)) z = - zorder f z"
       and zor_poly_inverse: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. inverse (f w)) z w
                                                 = inverse (zor_poly f z w)"
@@ -1131,33 +1133,32 @@
   define fp vfp where
     "fp = zor_poly f z" and "vfp = zor_poly vf z"
 
-  obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+  obtain fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
           and fr: "fp holomorphic_on cball z fr"
-                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
+                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 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)"
+  have fr_inverse: "vf w = (inverse (fp w)) * (w-z) powi (-fn)"
         and fr_nz: "inverse (fp w) \<noteq> 0"
     when "w\<in>ball z fr - {z}" for w
   proof -
-    have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
+    have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
       using fr(2) that by auto
-    then show "vf w = (inverse (fp w)) * (w - z) powi (-fn)" "inverse (fp w)\<noteq>0"
+    then show "vf w = (inverse (fp w)) * (w-z) powi (-fn)" "inverse (fp w)\<noteq>0"
       by (simp_all add: power_int_minus vf_def)
   qed
-  obtain vfr where [simp]:"vfp z \<noteq> 0" and "vfr>0" and vfr:"vfp holomorphic_on cball z vfr"
-      "(\<forall>w\<in>cball z vfr - {z}. vf w = vfp w * (w - z) powi vfn \<and> vfp w \<noteq> 0)"
+  obtain vfr where [simp]: "vfp z \<noteq> 0" and "vfr>0" and vfr: "vfp holomorphic_on cball z vfr"
+      "(\<forall>w\<in>cball z vfr - {z}. vf w = vfp w * (w-z) powi vfn \<and> vfp w \<noteq> 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 "\<exists>\<^sub>F w in at z. vf w \<noteq> 0"
-      using f_nconst unfolding vf_def by (auto elim:frequently_elim1)
+      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 \<open>fr>0\<close> \<open>vfr>0\<close> unfolding r1_def by simp
   show "vfn = - fn"
@@ -1165,8 +1166,8 @@
     have \<section>: "\<And>w. \<lbrakk>fp w = 0; dist z w < fr\<rbrakk> \<Longrightarrow> False"
       using fr_nz by force
     then show "\<forall>w\<in>ball z r1 - {z}.
-               vf w = vfp w * (w - z) powi vfn \<and>
-               vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w - z) powi (- fn) \<and>
+               vf w = vfp w * (w-z) powi vfn \<and>
+               vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w-z) powi (- fn) \<and>
                inverse (fp w) \<noteq> 0"
       using fr_inverse r1_def vfr(2)
       by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball)
@@ -1177,13 +1178,14 @@
   qed (use \<open>r1>0\<close> in auto)
   have "vfp w = inverse (fp w)" when "w\<in>ball z r1-{z}" for w
   proof -
-    have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}"  "w\<noteq>z" using that unfolding r1_def by auto
-    from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)] \<open>vfn = - fn\<close> \<open>w\<noteq>z\<close>
-    show ?thesis by auto
+    have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}"  "w\<noteq>z"
+      using that unfolding r1_def by auto
+    then show ?thesis
+      by (metis \<open>vfn = - fn\<close> power_int_not_zero right_minus_eq  fr_inverse vfr(2)
+          vector_space_over_itself.scale_right_imp_eq) 
   qed
   then show "\<forall>\<^sub>Fw in (at z). vfp w = inverse (fp w)"
-    unfolding eventually_at using \<open>r1>0\<close>
-    by (metis DiffI dist_commute mem_ball singletonD)
+    unfolding eventually_at by (metis DiffI dist_commute mem_ball singletonD \<open>r1>0\<close>)
 qed
 
 lemma zor_poly_shift:
@@ -1193,9 +1195,9 @@
   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) powi (zorder f z) \<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) powi (zorder f z) \<and>
            zor_poly f z w \<noteq> 0"
     using zorder_exist[OF iso1 ness1 nzero1] by blast
 
@@ -1203,54 +1205,50 @@
   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)
+    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)
+    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 powi (zorder ff 0) \<and>
-           zor_poly ff 0 w \<noteq> 0"
+  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 powi (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)"
+  have "zor_poly f z w = zor_poly ff 0 (w-z)"
     if "w\<in>ball z r - {z}" for w
   proof -
     define n where "n \<equiv> zorder f z"
 
-    have "f w = zor_poly f z w * (w - z) powi n"
+    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"
+    moreover have "f w = zor_poly ff 0 (w-z) * (w-z) powi 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)
-                            powi (zorder ff 0)"
-        by simp
+        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"
+    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 \<noteq>0"
+    moreover have "(w-z) powi n \<noteq>0"
       using that by auto
     ultimately show ?thesis
       using mult_cancel_right by blast
   qed
-  then have "\<forall>\<^sub>F w in at z. zor_poly f z w
-                  = zor_poly ff 0 (w - z)"
+  then have "\<forall>\<^sub>F w in at z. zor_poly f z w = zor_poly ff 0 (w-z)"
     unfolding eventually_at
     by (metis DiffI \<open>0 < r\<close> dist_commute mem_ball singletonD)
   moreover have "isCont (zor_poly f z) z"
@@ -1258,20 +1256,21 @@
     by (simp add: \<open>0 < r1\<close> continuous_on_interior)
   moreover 
   have "isCont (zor_poly ff 0) 0"
-    using \<open>0 < r2\<close> centre_in_ball continuous_on_interior holo2 holomorphic_on_imp_continuous_on interior_cball by blast  
-  then have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+    using \<open>0 < r2\<close> continuous_on_interior holo2 holomorphic_on_imp_continuous_on
+    by fastforce
+  then have "isCont (\<lambda>w. zor_poly ff 0 (w-z)) z"
       unfolding isCont_iff by simp
-  ultimately show "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly ff 0 (w - z)"
+  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"
-      and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+  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"
-  shows zorder_times:"zorder (\<lambda>w. f w * g w) z = zorder f z + zorder g z" and
-        zor_poly_times:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w * g w) z w
+  shows zorder_times: "zorder (\<lambda>w. f w * g w) z = zorder f z + zorder g z" and
+        zor_poly_times: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w * g w) z w
                                                   = zor_poly f z w *zor_poly g z w"
 proof -
   define fg where "fg = (\<lambda>w. f w * g w)"
@@ -1279,32 +1278,32 @@
     "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:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
+  have f_nconst: "\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst: "\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
     using fg_nconst by (auto elim!:frequently_elim1)
-  obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0"
+  obtain fr where [simp]: "fp z \<noteq> 0" and "fr > 0"
           and fr: "fp holomorphic_on cball z fr"
-                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powi fn \<and> fp w \<noteq> 0"
+                  "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w-z) powi fn \<and> fp w \<noteq> 0"
     using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto
-  obtain gr where [simp]:"gp z \<noteq> 0" and "gr > 0"
+  obtain gr where [simp]: "gp z \<noteq> 0" and "gr > 0"
           and gr: "gp holomorphic_on cball z gr"
-                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powi gn \<and> gp w \<noteq> 0"
+                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w-z) powi gn \<and> gp w \<noteq> 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 \<open>fr>0\<close> \<open>gr>0\<close> by auto
-  have fg_times:"fg w = (fp w * gp w) * (w - z) powi (fn+gn)" and fgp_nz:"fp w*gp w\<noteq>0"
+  have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\<noteq>0"
     when "w\<in>ball z r1 - {z}" for w
   proof -
-    have "f w = fp w * (w - z) powi fn" "fp w \<noteq> 0"
-      using fr(2)[rule_format,of w] that unfolding r1_def by auto
-    moreover have "g w = gp w * (w - z) powi gn" "gp w \<noteq> 0"
+    have "f w = fp w * (w-z) powi fn" "fp w \<noteq> 0"
+      using fr(2) r1_def that by auto
+    moreover have "g w = gp w * (w-z) powi gn" "gp w \<noteq> 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\<noteq>0"
-      using that unfolding fg_def by (auto simp add:power_int_add)
+    ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w\<noteq>0"
+      using that unfolding fg_def by (auto simp add: power_int_add)
   qed
 
-  obtain fgr where [simp]:"fgp z \<noteq> 0" and "fgr > 0"
+  obtain fgr where [simp]: "fgp z \<noteq> 0" and "fgr > 0"
           and fgr: "fgp holomorphic_on cball z fgr"
-                  "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0"
+                   "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w-z) powi fgn \<and> fgp w \<noteq> 0"
   proof -
     have "isolated_singularity_at fg z"
       unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] .
@@ -1318,42 +1317,40 @@
   define r2 where "r2 = min fgr r1"
   have "r2>0" using \<open>r1>0\<close> \<open>fgr>0\<close> unfolding r2_def by simp
   show "fgn = fn + gn "
-    apply (rule holomorphic_factor_unique[of r2 fgp z "\<lambda>w. fp w * gp w" fg])
-    subgoal using \<open>r2>0\<close> by simp
-    subgoal by simp
-    subgoal by simp
-    subgoal
-    proof (rule ballI)
-      fix w assume "w \<in> ball z r2 - {z}"
-      then have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}"  unfolding r2_def by auto
-      then show "fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0
-              \<and> fg w = fp w * gp w * (w - z) powi (fn + gn) \<and> fp w * gp w \<noteq> 0"
-        using fg_times fgp_nz fgr(2) by blast
-    qed
-    subgoal using fgr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros)
-    subgoal using fr(1) gr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros)
-    done
+  proof (rule holomorphic_factor_unique)
+    show "\<forall>w \<in> ball z r2 - {z}. fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0 \<and> fg w = fp w * gp w * (w - z) powi (fn + gn) \<and> fp w * gp w \<noteq> 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 "(\<lambda>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: \<open>0 < r2\<close>)
 
-  have "fgp w = fp w *gp w" when "w\<in>ball z r2-{z}" for w
+  have "fgp w = fp w *gp w" when w: "w \<in> ball z r2-{z}" for w
   proof -
-    have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" "w\<noteq>z" using that  unfolding r2_def by auto
-    from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)] \<open>fgn = fn + gn\<close> \<open>w\<noteq>z\<close>
-    show ?thesis by auto
+    have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" "w\<noteq>z" 
+      using w unfolding r2_def by auto
+    then show ?thesis
+      by (metis \<open>fgn = fn + gn\<close> eq_iff_diff_eq_0 fg_times fgr(2) power_int_eq_0_iff
+          mult_right_cancel)
   qed
   then show "\<forall>\<^sub>Fw in (at z). fgp w = fp w * gp w"
-    using \<open>r2>0\<close> unfolding eventually_at by (auto simp add:dist_commute)
+    using \<open>r2>0\<close> unfolding eventually_at by (auto simp add: dist_commute)
 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"
-      and f_ness:"not_essential f z" and g_ness:"not_essential g z"
+  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"
-  shows zorder_divide:"zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" and
-        zor_poly_divide:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w
-                                                  = zor_poly f z w  / zor_poly g z w"
+  shows zorder_divide: "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" and
+        zor_poly_divide: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w
+                                       = zor_poly f z w  / zor_poly g z w"
 proof -
-  have f_nconst:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
+  have f_nconst: "\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst: "\<exists>\<^sub>Fw in (at z).g w\<noteq> 0"
     using fg_nconst by (auto elim!:frequently_elim1)
   define vg where "vg=(\<lambda>w. inverse (g w))"
   have 1: "isolated_singularity_at vg z"
@@ -1362,59 +1359,53 @@
     by (simp add: g_iso g_ness not_essential_inverse vg_def)
   moreover have 3: "\<exists>\<^sub>F w in at z. f w * vg w \<noteq> 0"
     using fg_nconst vg_def by auto
-  ultimately  have "zorder (\<lambda>w. f w * vg w) z = zorder f z + zorder vg z"
+  ultimately have "zorder (\<lambda>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 (\<lambda>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)
-
+    by (auto simp add: field_simps)
   have "\<forall>\<^sub>F w in at z. zor_poly (\<lambda>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 "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>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)
+    by eventually_elim (auto simp add: field_simps)
 qed
 
 lemma zorder_exist_zero:
-  fixes f::"complex \<Rightarrow> complex" and z::complex
-  defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z"
-  assumes  holo: "f holomorphic_on s" and
-          "open s" "connected s" "z\<in>s"
-      and non_const: "\<exists>w\<in>s. f w \<noteq> 0"
-  shows "(if f z=0 then n > 0 else n=0) \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> s \<and> g holomorphic_on cball z r
+  fixes f:: "complex \<Rightarrow> complex" and z::complex
+  defines "n \<equiv> zorder f z" and "g \<equiv> zor_poly f z"
+  assumes  holo: "f holomorphic_on S" and "open S" "connected S" "z\<in>S"
+      and non_const: "\<exists>w\<in>S. f w \<noteq> 0"
+  shows "(if f z=0 then n > 0 else n=0) \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> S \<and> g holomorphic_on cball z r
     \<and> (\<forall>w\<in>cball z r. f w  = g w * (w-z) ^ nat n  \<and> g w \<noteq>0))"
 proof -
-  obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> s" "g holomorphic_on cball z r"
-            "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+  obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> S" "g holomorphic_on cball z r"
+            "(\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
   proof -
     have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r
-            \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0))"
+            \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 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,6)
-        by (meson Diff_subset open_ball analytic_on_holomorphic holomorphic_on_subset openE)
+      show "isolated_singularity_at f z"
+        using \<open>open S\<close> \<open>z\<in>S\<close> holo holomorphic_on_imp_analytic_at isolated_singularity_at_analytic 
+        by force 
       show "not_essential f z" unfolding not_essential_def
-        using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on
+        using \<open>open S\<close> \<open>z\<in>S\<close> at_within_open continuous_on holo holomorphic_on_imp_continuous_on
         by fastforce
-      have "\<forall>\<^sub>F w in at z. f w \<noteq> 0 \<and> w\<in>s"
-      proof -
-        obtain w where "w\<in>s" "f w\<noteq>0" using non_const by auto
-        then show ?thesis
-          by (rule non_zero_neighbour_alt[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close>])
-      qed
+      have "\<forall>\<^sub>F w in at z. f w \<noteq> 0 \<and> w\<in>S"
+        using assms(4,5,6) holo non_const non_zero_neighbour_alt by blast
       then show "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
         by (auto elim: eventually_frequentlyE)
     qed
-    then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1"
-            "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+    then obtain r1 where "g z \<noteq> 0" "r1>0" and r1: "g holomorphic_on cball z r1"
+            "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
       by auto
-    obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> s"
+    obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> S"
       using assms(4,6) open_contains_cball_eq by blast
     define r3 where "r3 \<equiv> min r1 r2"
-    have "r3>0" "cball z r3 \<subseteq> s" using \<open>r1>0\<close> r2 unfolding r3_def by auto
+    have "r3>0" "cball z r3 \<subseteq> S" using \<open>r1>0\<close> r2 unfolding r3_def by auto
     moreover have "g holomorphic_on cball z r3"
       using r1(1) unfolding r3_def by auto
-    moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+    moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
       using r1(2) unfolding r3_def by auto
     ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto
   qed
@@ -1425,24 +1416,24 @@
     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"
+  have if_0: "if f z=0 then n > 0 else n=0"
   proof -
-    have "(\<lambda>w. g w * (w - z) powi n) \<midarrow>z\<rightarrow> f z"
+    have "(\<lambda>w. g w * (w-z) powi n) \<midarrow>z\<rightarrow> f z"
       using fz_lim Lim_transform_within_open[where s="ball z r"] r by fastforce
-    then have "(\<lambda>w. (g w * (w - z) powi n) / g w) \<midarrow>z\<rightarrow> f z/g z"
+    then have "(\<lambda>w. (g w * (w-z) powi n) / g w) \<midarrow>z\<rightarrow> f z/g z"
       using gz_lim \<open>g z \<noteq> 0\<close> tendsto_divide by blast
-    then have powi_tendsto:"(\<lambda>w. (w - z) powi n) \<midarrow>z\<rightarrow> f z/g z"
+    then have powi_tendsto: "(\<lambda>w. (w-z) powi n) \<midarrow>z\<rightarrow> f z/g z"
       using Lim_transform_within_open[where s="ball z r"] r by fastforce
 
     have ?thesis when "n\<ge>0" "f z=0"
     proof -
-      have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
+      have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 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 *:"(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp
+      then have *: "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp
       moreover have False when "n=0"
       proof -
-        have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 1"
+        have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 1"
           using \<open>n=0\<close> by auto
         then show False using * using LIM_unique zero_neq_one by blast
       qed
@@ -1452,28 +1443,30 @@
     proof -
       have False when "n>0"
       proof -
-        have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
+        have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
           using Lim_transform_within[OF powi_tendsto, where d=r]
           by (meson \<open>0 \<le> n\<close> power_int_def r(1))
-        moreover have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0"
+        moreover have "(\<lambda>w. (w-z) ^ nat n) \<midarrow>z\<rightarrow> 0"
           using \<open>n>0\<close> by (auto intro!:tendsto_eq_intros)
-        ultimately show False using \<open>f z\<noteq>0\<close> \<open>g z\<noteq>0\<close> using LIM_unique divide_eq_0_iff by blast
+        ultimately show False 
+          using \<open>f z\<noteq>0\<close> \<open>g z\<noteq>0\<close> 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 "(\<lambda>w. inverse ((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
+      have "(\<lambda>w. inverse ((w-z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
         by (smt (verit) LIM_cong power_int_def power_inverse powi_tendsto that)
       moreover
-      have "(\<lambda>w.((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0"
+      have "(\<lambda>w.((w-z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0"
         using that by (auto intro!:tendsto_eq_intros)
       ultimately
       have "(\<lambda>x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \<midarrow>z\<rightarrow> 0" 
         using tendsto_mult by fastforce
       then have "(\<lambda>x. 1::complex) \<midarrow>z\<rightarrow> 0"
         using Lim_transform_within_open by fastforce
-      then show False using LIM_const_eq by fastforce
+      then show False 
+        using LIM_const_eq by fastforce
     qed
     ultimately show ?thesis by fastforce
   qed
@@ -1499,7 +1492,7 @@
     then show ?thesis using \<open>g z\<noteq>0\<close> True by auto
   next
     case False
-    then have "f w = g w * (w - z) powi n \<and> g w \<noteq> 0"
+    then have "f w = g w * (w-z) powi n" "g w \<noteq> 0"
       using r(4) that by auto
     then show ?thesis
       by (smt (verit, best) False if_0 int_nat_eq power_int_of_nat)
@@ -1508,17 +1501,17 @@
 qed
 
 lemma zorder_exist_pole:
-  fixes f::"complex \<Rightarrow> complex" and z::complex
+  fixes f:: "complex \<Rightarrow> complex" and z::complex
   defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z"
   assumes  holo: "f holomorphic_on S-{z}" and "open S" "z\<in>S" and "is_pole f z"
   shows "n < 0 \<and> g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> S \<and> g holomorphic_on cball z r
     \<and> (\<forall>w\<in>cball z r - {z}. f w  = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0))"
 proof -
   obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> S" "g holomorphic_on cball z r"
-            "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+            "(\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
   proof -
     have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r
-            \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0))"
+            \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 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)
@@ -1529,8 +1522,8 @@
       from non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] show "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
         by (auto elim: eventually_frequentlyE)
     qed
-    then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1"
-            "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+    then obtain r1 where "g z \<noteq> 0" "r1>0" and r1: "g holomorphic_on cball z r1"
+            "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
       by auto
     obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> S"
       using assms(4,5) open_contains_cball_eq by metis
@@ -1538,22 +1531,24 @@
     have "r3>0" "cball z r3 \<subseteq> S" using \<open>r1>0\<close> r2 unfolding r3_def by auto
     moreover have "g holomorphic_on cball z r3"
       using r1(1) unfolding r3_def by auto
-    moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powi n \<and> g w \<noteq> 0)"
+    moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w-z) powi n \<and> g w \<noteq> 0)"
       using r1(2) unfolding r3_def by auto
-    ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto
+    ultimately show ?thesis 
+      using that[of r3] \<open>g z\<noteq>0\<close> by auto
   qed
 
   have "n<0"
   proof (rule ccontr)
     assume " \<not> n < 0"
     define c where "c=(if n=0 then g z else 0)"
-    have [simp]:"g \<midarrow>z\<rightarrow> g z"
-      by (metis open_ball at_within_open ball_subset_cball centre_in_ball
-            continuous_on holomorphic_on_imp_continuous_on holomorphic_on_subset r(1) r(3) )
-    have "\<forall>\<^sub>F x in at z. f x = g x * (x - z) ^ nat n"
-      unfolding eventually_at_topological
-      apply (rule_tac exI[where x="ball z r"])
-      by (simp add: \<open>\<not> n < 0\<close> linorder_not_le power_int_def r(1) r(4))
+    have [simp]: "g \<midarrow>z\<rightarrow> g z"
+      using r
+      by (metis centre_in_ball continuous_on_interior holomorphic_on_imp_continuous_on
+          interior_cball isContD)
+    have "\<forall>x \<in> ball z r. x \<noteq> z \<longrightarrow> f x = g x * (x - z) ^ nat n"
+      by (simp add: \<open>\<not> n < 0\<close> linorder_not_le power_int_def r)
+    then have "\<forall>\<^sub>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 "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow> c"
     proof (cases "n=0")
       case True
@@ -1572,12 +1567,13 @@
   moreover have "\<forall>w\<in>cball z r - {z}. f w  = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0"
     using r(4) \<open>n<0\<close>
     by (smt (verit) inverse_eq_divide mult.right_neutral power_int_def power_inverse times_divide_eq_right)
-  ultimately show ?thesis using r(1-3) \<open>g z\<noteq>0\<close> by auto
+  ultimately show ?thesis 
+    using r \<open>g z\<noteq>0\<close> by auto
 qed
 
 lemma zorder_eqI:
   assumes "open S" "z \<in> S" "g holomorphic_on S" "g z \<noteq> 0"
-  assumes fg_eq:"\<And>w. \<lbrakk>w \<in> S;w\<noteq>z\<rbrakk> \<Longrightarrow> f w = g w * (w - z) powi n"
+  assumes fg_eq: "\<And>w. \<lbrakk>w \<in> S;w\<noteq>z\<rbrakk> \<Longrightarrow> 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
@@ -1588,7 +1584,7 @@
   ultimately obtain r where r: "r > 0" "cball z r \<subseteq>  S \<inter> (g -` (-{0}))"
     unfolding open_contains_cball by blast
 
-  let ?gg= "(\<lambda>w. g w * (w - z) powi n)"
+  let ?gg= "(\<lambda>w. g w * (w-z) powi n)"
   define P where "P = (\<lambda>n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0
           \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0))"
   have "P n g r"
@@ -1611,13 +1607,13 @@
             isCont_def not_essential_def)
       show " \<forall>\<^sub>F w in at z. w - z \<noteq> 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)
+        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 "\<forall>\<^sub>F w in at z. g w * (w - z) powi n = f w"
+    have "\<forall>\<^sub>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
@@ -1626,12 +1622,12 @@
       fix d::real assume "0 < d"
       define z' where "z' \<equiv> z+min d r / 2"
       have "z' \<noteq> z" " dist z' z < d "
-        unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
+        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"
-          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
+          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) powi n \<noteq> 0"
           using P_def \<open>P n g r\<close> \<open>z' \<in> cball z r\<close> \<open>z' \<noteq> z\<close> by auto
       qed
@@ -1645,47 +1641,47 @@
 
 lemma simple_zeroI:
   assumes "open S" "z \<in> S" "g holomorphic_on S" "g z \<noteq> 0"
-  assumes "\<And>w. w \<in> S \<Longrightarrow> f w = g w * (w - z)"
+  assumes "\<And>w. w \<in> S \<Longrightarrow> f w = g w * (w-z)"
   shows   "zorder f z = 1"
   using assms zorder_eqI by force
 
 lemma higher_deriv_power:
-  shows   "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) w =
-             pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)"
+  shows   "(deriv ^^ j) (\<lambda>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) (\<lambda>w. (w - z) ^ n) w = deriv ((deriv ^^ j) (\<lambda>w. (w - z) ^ n)) w"
+  have "(deriv ^^ Suc j) (\<lambda>w. (w-z) ^ n) w = deriv ((deriv ^^ j) (\<lambda>w. (w-z) ^ n)) w"
     by simp
-  also have "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) =
-               (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j))"
+  also have "(deriv ^^ j) (\<lambda>w. (w-z) ^ n) =
+               (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j))"
     using Suc by (intro Suc.IH ext)
   also {
     have "(\<dots> has_field_derivative of_nat (n - j) *
-               pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - Suc j)) (at w)"
+               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 \<le> n", subst pochhammer_rec)
-         (insert Suc.prems, simp_all add: algebra_simps Suc_diff_le pochhammer_0_left)
-    finally have "deriv (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)) w =
-                    \<dots> * (w - z) ^ (n - Suc j)"
+         (use Suc.prems in \<open>simp_all add: algebra_simps Suc_diff_le pochhammer_0_left\<close>)
+    finally have "deriv (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w-z) ^ (n - j)) w =
+                    \<dots> * (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 \<in> S"
+  assumes  f_holo: "f holomorphic_on S" and "open S" "z \<in> S"
   assumes zero: "\<And>i. i < nat n \<Longrightarrow> (deriv ^^ i) f z = 0"
   assumes nz: "(deriv ^^ nat n) f z \<noteq> 0" and "n\<ge>0"
   shows   "zorder f z = n"
 proof -
-  obtain r where [simp]:"r>0" and "ball z r \<subseteq> S"
+  obtain r where [simp]: "r>0" and "ball z r \<subseteq> S"
     using \<open>open S\<close> \<open>z\<in>S\<close> openE by blast
-  have nz':"\<exists>w\<in>ball z r. f w \<noteq> 0"
+  have nz': "\<exists>w\<in>ball z r. f w \<noteq> 0"
   proof (rule ccontr)
     assume "\<not> (\<exists>w\<in>ball z r. f w \<noteq> 0)"
     then have "eventually (\<lambda>u. f u = 0) (nhds z)"
@@ -1701,7 +1697,7 @@
   obtain e where e_if: "if f z = 0 then 0 < zn else zn = 0" and
             [simp]: "e>0" and "cball z e \<subseteq> ball z r" and
             g_holo: "g holomorphic_on cball z e" and
-            e_fac: "(\<forall>w\<in>cball z e. f w = g w * (w - z) ^ nat zn \<and> g w \<noteq> 0)"
+            e_fac: "(\<forall>w\<in>cball z e. f w = g w * (w-z) ^ nat zn \<and> g w \<noteq> 0)"
   proof -
     have "f holomorphic_on ball z r"
       using f_holo \<open>ball z r \<subseteq> S\<close> by auto
@@ -1712,23 +1708,23 @@
     by (metis centre_in_cball less_le_not_le order_refl)
 
   define A where "A \<equiv> (\<lambda>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 \<le> int i then A i else 0)" for i
+  have deriv_A: "(deriv ^^ i) f z = (if zn \<le> int i then A i else 0)" for i
   proof -
     have "eventually (\<lambda>w. w \<in> ball z e) (nhds z)"
       using \<open>cball z e \<subseteq> ball z r\<close> \<open>e>0\<close> by (intro eventually_nhds_in_open) auto
-    hence "eventually (\<lambda>w. f w = (w - z) ^ (nat zn) * g w) (nhds z)"
+    hence "eventually (\<lambda>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) (\<lambda>w. (w - z) ^ nat zn * g w) z"
+    hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w-z) ^ nat zn * g w) z"
       by (intro higher_deriv_cong_ev) auto
     also have "\<dots> = (\<Sum>j=0..i. of_nat (i choose j) *
-                       (deriv ^^ j) (\<lambda>w. (w - z) ^ nat zn) z * (deriv ^^ (i - j)) g z)"
+                       (deriv ^^ j) (\<lambda>w. (w-z) ^ nat zn) z * (deriv ^^ (i - j)) g z)"
       using g_holo \<open>e>0\<close>
       by (intro higher_deriv_mult[of _ "ball z e"]) (auto intro!: holomorphic_intros)
     also have "\<dots> = (\<Sum>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) (\<lambda>w. (w - z) ^ nat zn) z =
+      have "(deriv ^^ j) (\<lambda>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 "\<dots> = (if j = nat zn then fact j else 0)"
@@ -1745,18 +1741,15 @@
   qed
 
   have False when "n<zn"
-  proof -
-    have "(deriv ^^ nat n) f z = 0"
-      using deriv_A[of "nat n"] that \<open>n\<ge>0\<close> by auto
-    with nz show False by auto
-  qed
+    using deriv_A[of "nat n"] that \<open>n\<ge>0\<close> by (simp add: nz) 
   moreover have "n\<le>zn"
   proof -
-    have "g z \<noteq> 0" using e_fac[rule_format,of z] \<open>e>0\<close> by simp
+    have "g z \<noteq> 0"
+      by (simp add: \<open>g z \<noteq> 0\<close>)
     then have "(deriv ^^ nat zn) f z \<noteq> 0"
-      using deriv_A[of "nat zn"] by(auto simp add:A_def)
+      using deriv_A[of "nat zn"] by(auto simp add: A_def)
     then have "nat zn \<ge> nat n" using zero[of "nat zn"] by linarith
-    moreover have "zn\<ge>0" using e_if by (auto split:if_splits)
+    moreover have "zn\<ge>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
@@ -1764,7 +1757,7 @@
 
 lemma
   assumes "eventually (\<lambda>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'"
+  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 = (\<lambda>ff n h r. 0 < r \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
                     \<and> (\<forall>w\<in>cball z r - {z}. ff w = h w * (w-z) powi n \<and> h w\<noteq>0))"
@@ -1772,19 +1765,19 @@
   proof -
     have *: "\<exists>r. P g n h r" if "\<exists>r. P f n h r" and "eventually (\<lambda>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:"\<forall>x. x \<noteq> z \<and> dist x z \<le> r2 \<longrightarrow> f x = g x"
+      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: "\<forall>x. x \<noteq> z \<and> dist x z \<le> r2 \<longrightarrow> f x = g x"
         unfolding eventually_at_le by auto
       define r where "r=min r1 r2"
       have "r>0" "h z\<noteq>0" using r1_P \<open>r2>0\<close> 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 \<and> h w \<noteq> 0" when "w\<in>cball z r - {z}" for w
+      moreover have "g w = h w * (w-z) powi n \<and> h w \<noteq> 0" when "w\<in>cball z r - {z}" for w
       proof -
-        have "f w = h w * (w - z) powi n \<and> h w \<noteq> 0"
+        have "f w = h w * (w-z) powi n \<and> h w \<noteq> 0"
           using r1_P that unfolding P_def r_def by auto
-        moreover have "f w=g w" using r2_dist[rule_format,of w] that unfolding r_def
-          by (simp add: dist_commute)
+        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
@@ -1792,7 +1785,7 @@
     from assms have eq': "eventually (\<lambda>z. g z = f z) (at z)"
       by (simp add: eq_commute)
     show ?thesis
-      by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']])
+      using "*" assms(1) eq' by blast
   qed
   then show "zorder f z = zorder g z'" "zor_poly f z = zor_poly g z'"
       using \<open>z=z'\<close> unfolding P_def zorder_def zor_poly_def by auto
@@ -1810,8 +1803,9 @@
 proof -
   define P where
     "P = (\<lambda>f n h r. 0 < r \<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) powi n \<and> h w \<noteq> 0))"
-  have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r" if "P f n h r" "c \<noteq> 0" for f n h r c
+                    h z \<noteq> 0 \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powi n \<and> h w \<noteq> 0))"
+  have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r" 
+    if "P f n h r" "c \<noteq> 0" for f n h r c
     using that unfolding P_def by (auto intro!: holomorphic_intros)
   have "(\<exists>h r. P (\<lambda>x. c * f x) n h r) \<longleftrightarrow> (\<exists>h r. P f n h r)" for n
     using *[of f n _ _ c] *[of "\<lambda>x. c * f x" n _ _ "inverse c"] \<open>c \<noteq> 0\<close>
@@ -1827,17 +1821,17 @@
 
 lemma zorder_nonzero_div_power:
   assumes sz: "open S" "z \<in> S" "f holomorphic_on S" "f z \<noteq> 0" and "n > 0"
-  shows  "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n"
+  shows  "zorder (\<lambda>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" "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
-  shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) powi - zorder f z) (at z)"
+  shows "eventually (\<lambda>w. zor_poly f z w = f w * (w-z) powi - zorder f z) (at z)"
 proof -
-  obtain r where r:"r>0"
-       "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) powi (zorder f z))"
+  obtain r where r: "r>0"
+       "(\<forall>w\<in>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 *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) powi - zorder f z"
+  then have *: "\<forall>w\<in>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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
     using r eventually_at_ball'[of r z UNIV] by auto
@@ -1846,12 +1840,12 @@
 
 lemma zor_poly_zero_eq:
   assumes "f holomorphic_on S" "open S" "connected S" "z \<in> S" "\<exists>w\<in>S. f w \<noteq> 0"
-  shows "eventually (\<lambda>w. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)) (at z)"
+  shows "eventually (\<lambda>w. zor_poly f z w = f w / (w-z) ^ nat (zorder f z)) (at z)"
 proof -
-  obtain r where r:"r>0"
-       "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) ^ nat (zorder f z))"
+  obtain r where r: "r>0"
+       "(\<forall>w\<in>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 *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)"
+  then have *: "\<forall>w\<in>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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
     using r eventually_at_ball'[of r z UNIV] by auto
@@ -1859,15 +1853,15 @@
 qed
 
 lemma zor_poly_pole_eq:
-  assumes f_iso:"isolated_singularity_at f z" "is_pole f z"
-  shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)) (at z)"
+  assumes f_iso: "isolated_singularity_at f z" "is_pole f z"
+  shows "eventually (\<lambda>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}"
+  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"
-       "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w / (w - z) ^ nat (- zorder f z))"
+  obtain r where r: "r>0"
+       "(\<forall>w\<in>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 \<open>is_pole f z\<close>] by auto
-  then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)"
+  then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w-z) ^ nat (- zorder f z)"
     by (auto simp: field_simps)
   have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
     using r eventually_at_ball'[of r z UNIV] by auto
@@ -1892,7 +1886,7 @@
     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(1,2) have "isCont (zor_poly f z0) z0"
+  with r have "isCont (zor_poly f z0) z0"
     by (auto simp: continuous_on_eq_continuous_at)
   hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
     unfolding isCont_def .
@@ -1935,7 +1929,7 @@
 lemma zor_poly_pole_eqI:
   fixes f :: "complex \<Rightarrow> complex" and z0 :: complex
   defines "n \<equiv> zorder f z0"
-  assumes f_iso:"isolated_singularity_at f z0" and "is_pole f z0"
+  assumes f_iso: "isolated_singularity_at f z0" and "is_pole f z0"
   assumes lim: "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> c) F"
   assumes g: "filterlim g (at z0) F" and "F \<noteq> bot"
   shows   "zor_poly f z0 z0 = c"
@@ -1943,9 +1937,12 @@
   obtain r where r: "r > 0"  "zor_poly f z0 holomorphic_on cball z0 r"
   proof -
     have "\<exists>\<^sub>F w in at z0. f w \<noteq> 0"
-      using non_zero_neighbour_pole[OF \<open>is_pole f z0\<close>] by (auto elim:eventually_frequentlyE)
-    moreover have "not_essential f z0" unfolding not_essential_def using \<open>is_pole f z0\<close> by simp
-    ultimately show ?thesis using that zorder_exist[OF f_iso,folded n_def] by auto
+      using non_zero_neighbour_pole[OF \<open>is_pole f z0\<close>] 
+      by (auto elim: eventually_frequentlyE)
+    moreover have "not_essential f z0" 
+      unfolding not_essential_def using \<open>is_pole f z0\<close> by simp
+    ultimately show ?thesis 
+      using that zorder_exist[OF f_iso,folded n_def] by auto
   qed
   from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)"
     using eventually_at_ball'[of r z0 UNIV] by auto
@@ -1979,15 +1976,15 @@
   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)"
+  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
+    "\<forall>w\<in>cball x r - {x}. f w = P w / (w-x) ^ n \<and> P w \<noteq> 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)
 
@@ -1995,7 +1992,7 @@
     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 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)
@@ -2010,12 +2007,10 @@
     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
+    have \<section>: "(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 "((\<lambda>w. P w / (w-x) ^ n) has_field_derivative D w) (at w)"
+      by (rule derivative_eq_intros refl | use w \<section> in force)+
     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)" .
@@ -2036,7 +2031,7 @@
   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) powi (- int (Suc n))"
+    show "f' w = (deriv P w * (w-x) - of_nat n * P w) * (w-x) powi (- 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 power_int_diff power_int_minus powr_nat' divide_simps)
   qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
@@ -2081,7 +2076,8 @@
   qed
 
   have "g holomorphic_on A"
-    unfolding g_def using assms assms(1) holo by (intro removable_singularity) auto
+    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)"
@@ -2124,15 +2120,12 @@
   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)
+    thus ?thesis
+      using assms is_pole_deriv' by blast
   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)
+      by (meson assms removable_singularity_deriv' tendsto_imp_not_essential)
   qed
 qed
 
@@ -2178,7 +2171,7 @@
   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>)
+      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 ..
@@ -2241,13 +2234,14 @@
   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
+    using ** \<open>is_pole f x\<close> 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:"\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
+  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"
@@ -2255,24 +2249,23 @@
   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) powi n \<and> P w \<noteq> 0)"
+  obtain r where r: "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) powi 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) powi n) z"
+  have "is_pole (\<lambda>w. P w * (w-z) powi 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)
+      by (metis \<open>r>0\<close> r_holo centre_in_ball continuous_on_interior 
+                holomorphic_on_imp_continuous_on interior_cball isContD)
     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)
+              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"
@@ -2283,18 +2276,18 @@
         by (simp add: eventually_at_filter)
     qed auto
   qed
-  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w - z) powi n"
+  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w-z) powi n"
     unfolding eventually_at_le
     using w_Pn \<open>r>0\<close> 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 \<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"
+  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"
+      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"
@@ -2302,15 +2295,15 @@
 
   have "isolated_singularity_at fg z"
     unfolding fg_def using f_iso g_iso g_ness
-    by (auto intro:singularity_intros)
+    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)
+    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] .
+      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
@@ -2321,7 +2314,7 @@
 qed
 
 lemma isolated_pole_imp_nzero_times:
-  assumes f_iso:"isolated_singularity_at f z"
+  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)
@@ -2350,30 +2343,30 @@
   by (meson analytic_deriv assms isolated_singularity_at_def)
 
 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"
+  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"
+  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) powi n \<and> P w \<noteq> 0)"
+                            = P w * (w-z) powi 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)"
+  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))"
+  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
+  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
@@ -2384,11 +2377,10 @@
     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)"
+    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')
+      by (auto simp: algebra_simps simp flip:power_int_add_1' wz_def)
     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
@@ -2402,14 +2394,13 @@
   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))"
+    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) powi (n - 1)"
+    show "deriv f w = (deriv P w * (w-z) + of_int n * P w) * (w-z) powi (n - 1)"
       if "w \<in> ball z r" "w \<noteq> z" for w
       using D_def deriv_f_eq that by blast
   qed
@@ -2417,20 +2408,19 @@
 
 
 lemma deriv_divide_is_pole: \<comment>\<open>Generalises @{thm zorder_deriv}\<close>
-  fixes f g::"complex \<Rightarrow> complex" and z::complex
-  assumes f_iso:"isolated_singularity_at f z"
-      and f_ness:"not_essential f z" 
+  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 fg_nconst: "\<exists>\<^sub>Fw in (at z). deriv f w *  f w \<noteq> 0"
-      and f_ord:"zorder f z \<noteq>0"
+      and f_ord: "zorder f z \<noteq>0"
     shows "is_pole (\<lambda>z. deriv f z / f z) z"
 proof (rule neg_zorder_imp_is_pole)
   define ff where "ff=(\<lambda>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)
+    by (auto intro: singularity_intros)
   show "not_essential ff z" 
-    unfolding ff_def using f_ness f_iso
-    by (auto intro:singularity_intros)
+    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
@@ -2444,8 +2434,8 @@
 qed
 
 lemma is_pole_deriv_divide_is_pole:
-  fixes f g::"complex \<Rightarrow> complex" and z::complex
-  assumes f_iso:"isolated_singularity_at f z"
+  fixes f g:: "complex \<Rightarrow> complex" and z::complex
+  assumes f_iso: "isolated_singularity_at f z"
       and "is_pole f z" 
     shows "is_pole (\<lambda>z. deriv f z / f z) z"
 proof (rule deriv_divide_is_pole[OF f_iso])
diff -r 067462a6a652 -r 1171ea4a23e4 src/HOL/Complex_Analysis/Riemann_Mapping.thy
--- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy	Sun Jan 19 18:18:07 2025 +0000
+++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy	Wed Jan 22 22:22:27 2025 +0000
@@ -63,8 +63,10 @@
   qed
   show ?thesis
     unfolding Moebius_function_def
-    apply (intro holomorphic_intros)
-    by (metis "*" mult.commute complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 right_minus_eq)
+  proof (intro holomorphic_intros)
+    show "\<And>z. z \<in> ball 0 1 \<Longrightarrow> 1 - cnj w * z \<noteq> 0"
+      by (metis * complex_cnj_cnj complex_cnj_mult complex_mod_cnj mem_ball_0 mult.commute mult_1 right_minus_eq)
+  qed
 qed
 
 lemma Moebius_function_compose:
@@ -80,7 +82,7 @@
     have "w2 * cnj w2 = 1"
       using that meq by (auto simp: algebra_simps)
     then show "z = 0"
-      by (metis (no_types) \<open>cmod w2 < 1\<close> complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
+      using \<open>cmod w2 < 1\<close> complex_mod_sqrt_Re_mult_cnj by force
   qed
   moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
     using meq by (fastforce simp: algebra_simps)
@@ -151,10 +153,9 @@
           by force
         have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
           if "z \<in> ball 0 1" for z::complex
-        proof (rule DERIV_chain' [where g=f])
-          show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
-            by (metis holomorphic_derivI [OF holF \<open>open S\<close>] \<open>f \<in> F\<close> image_subset_iff r01 that)
-        qed simp
+          using DERIV_chain' [where g=f] \<open>open S\<close>
+          by (meson DERIV_cmult_Id \<open>f \<in> F\<close> holF holomorphic_derivI image_subset_iff
+              r01 that)
         have df0: "((\<lambda>w. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
           using * [of 0] by simp
         have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
@@ -316,12 +317,7 @@
         qed
       qed
       have norm\<psi>1: "norm(\<psi> (h (f z))) < 1" if "z \<in> S" for z
-      proof -
-        have "norm (\<psi> (h (f z)) ^ 2) < 1"
-          by (metis (no_types) that DIM_complex \<psi>2 h01 image_subset_iff mem_ball_0 nf1)
-        then show ?thesis
-          by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
-      qed
+        by (metis \<psi>2 h01 image_subset_iff mem_ball_0 nf1 norm_power power_less1_D that)
       then have \<psi>01: "\<psi> (h (f 0)) \<in> ball 0 1"
         by (simp add: \<open>0 \<in> S\<close>)
       obtain p q where p0: "p (\<psi> (h (f 0))) = 0"
@@ -535,7 +531,7 @@
             using gxy by (auto simp: path_image_join)
         qed (use gxy holf in auto)
         then have fintxy: "f contour_integrable_on linepath x y"
-          by (metis (no_types, lifting) contour_integrable_joinD1 contour_integrable_joinD2 gxy(2) has_contour_integral_integrable pathfinish_linepath pathstart_reversepath valid_path_imp_reverse valid_path_join valid_path_linepath vp(2))
+          using gxy(2) has_contour_integral_integrable vp by fastforce
         have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
           using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
         show ?thesis
@@ -671,8 +667,8 @@
       unfolding norm_divide
       using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
       by (simp_all add: field_split_simps dist_commute dist_norm)
-  then show "?f ` S \<subseteq> ball 0 1"
-    by auto
+    then show "?f ` S \<subseteq> ball 0 1"
+      by auto
     show "inj_on ?f S"
       using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
       by (metis diff_add_cancel)
@@ -697,7 +693,7 @@
     proof (intro exI conjI)
       show "g \<circ> k holomorphic_on h ` S"
         by (smt (verit) holg holk holomorphic_on_compose holomorphic_on_subset imageE image_subset_iff kh)
-      show "\<forall>z\<in>h ` S. f z = ((g \<circ> k) z)\<^sup>2"
+      show "\<forall>z \<in> h ` S. f z = ((g \<circ> k) z)\<^sup>2"
         using eqg kh by auto
     qed
   qed
@@ -714,22 +710,13 @@
 qed
 
 lemma homeomorphic_to_disc:
-  assumes S: "S \<noteq> {}"
-    and prev: "S = UNIV \<or>
+  assumes "S = UNIV \<or>
                (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
-                     (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
-                     (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
+                      (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
+                      (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
   shows "S homeomorphic ball (0::complex) 1"
-  using prev
-proof
-  assume "S = UNIV" then show ?thesis
-    using homeomorphic_ball01_UNIV homeomorphic_sym by blast
-next
-  assume ?P
-  then show ?thesis
-    unfolding homeomorphic_minimal
-    using holomorphic_on_imp_continuous_on by blast
-qed
+  by (smt (verit, ccfv_SIG) holomorphic_on_imp_continuous_on homeomorphic_ball01_UNIV
+      homeomorphic_minimal assms)
 
 lemma homeomorphic_to_disc_imp_simply_connected:
   assumes "S = {} \<or> S homeomorphic ball (0::complex) 1"
@@ -900,15 +887,11 @@
           using n \<open>cmod x < 1\<close> by (auto simp: field_split_simps algebra_simps D_def)
         moreover have " f ` D n \<inter> closure (f ` A n) = {}"
         proof -
-          have op_fDn: "open(f ` (D n))"
-          proof (rule invariance_of_domain)
-            show "continuous_on (D n) f"
-              by (rule continuous_on_subset [OF contf D01])
-            show "open (D n)"
-              by (simp add: D_def)
-            show "inj_on f (D n)"
-              unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
-          qed
+          have"inj_on f (D n)"
+            unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
+          then have op_fDn: "open(f ` (D n))"
+            by (metis invariance_of_domain D_def Elementary_Metric_Spaces.open_ball 
+                continuous_on_subset [OF contf D01])
           have injf: "inj_on f (ball 0 1)"
             by (metis mem_ball_0 inj_on_def gf)
           have "D n \<union> A n \<subseteq> ball 0 1"
@@ -992,9 +975,9 @@
               by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
           qed (use \<open>compact L\<close> \<open>C \<subseteq> L\<close> in auto)
         qed
-        obtain U V where "open U" and "compact (closure U)" and "open V" "K \<subseteq> U"
-                     and V: "\<Inter>(range X) - K \<subseteq> V" and "U \<inter> V = {}"
-          using separation_normal_compact [OF \<open>compact K\<close> clo] by blast
+        obtain U V where "open U" "open V" and "compact (closure U)"
+                     and V: "\<Inter>(range X) - K \<subseteq> V" and U: "K \<subseteq> U" "U \<inter> V = {}"
+          by (metis Diff_disjoint separation_normal_compact [OF \<open>compact K\<close> clo])
         then have "U \<inter> (\<Inter> (range X) - K) = {}"
           by blast
         have "(closure U - U) \<inter> (\<Inter>n. X n \<inter> closure U) \<noteq> {}"
@@ -1049,12 +1032,8 @@
         moreover have "(\<Inter>n. X n \<inter> closure U) = (\<Inter>n. X n) \<inter> closure U"
           by blast
         moreover have "x \<in> U" if "\<And>n. x \<in> X n" "x \<in> closure U" for x
-        proof -
-          have "x \<notin> V"
-            using \<open>U \<inter> V = {}\<close> \<open>open V\<close> closure_iff_nhds_not_empty that(2) by blast
-          then show ?thesis
-            by (metis (no_types) Diff_iff INT_I V \<open>K \<subseteq> U\<close> subsetD that(1))
-        qed
+          by (metis Diff_iff INT_I U V \<open>open V\<close> closure_iff_nhds_not_empty
+              order.refl subsetD that)
         ultimately show False
           by (auto simp: open_Int_closure_eq_empty [OF \<open>open V\<close>, of U])
       qed
@@ -1101,7 +1080,7 @@
           moreover have "closed C"
             using C_ccsw clo_ccs by blast
           ultimately show False
-            by (metis C False \<open>S \<noteq> UNIV\<close> C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
+            by (metis C \<open>S \<noteq> {}\<close> \<open>S \<noteq> UNIV\<close> C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
                 frontier_closed frontier_complement frontier_eq_empty frontier_of_components_subset in_components_maximal inf.orderE)
         qed
         then show "connected_component_set (- S) w \<inter> frontier S \<noteq> {}"
@@ -1114,14 +1093,18 @@
             by (auto simp: closed_Compl closed_connected_component frontier_def openS)
           show "frontier (connected_component_set (- S) z) \<subseteq> frontier (- S)"
             using frontier_of_connected_component_subset by fastforce
-          have "\<not> bounded (-S)"
+          have "connected (closure S - S)"
+            by (metis confr frontier_def interior_open openS)
+          moreover have "\<not> bounded (-S)"
             by (simp add: True cobounded_imp_unbounded)
+          moreover have "bounded (connected_component_set (- S) w)"
+            using C_ccsw \<open>bounded C\<close> by auto
+          ultimately have "z \<notin> S"
+            using \<open>w \<notin> S\<close> openS
+            by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset
+                  connected_component_eq_self connected_diff_open_from_closed subset_UNIV)
           then have "connected_component_set (- S) z \<noteq> {}"
-            unfolding connected_component_eq_empty
-            using confr openS \<open>bounded C\<close> \<open>w \<notin> S\<close>
-            apply (simp add: frontier_def interior_open C_ccsw)
-            by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
-                      connected_diff_open_from_closed subset_UNIV)
+            by (metis ComplI connected_component_eq_empty)
           then show "frontier (connected_component_set (- S) z) \<noteq> {}"
             by (metis False \<open>S \<noteq> UNIV\<close> connected_component_eq_UNIV frontier_complement frontier_eq_empty)
         qed
@@ -1285,8 +1268,8 @@
       obtain \<delta> where "0 < \<delta>" "\<And>w. \<lbrakk>w \<in> S; dist w z < \<delta>\<rbrakk> \<Longrightarrow> dist (g w) (g z) < cmod (g z)"
         using contg [unfolded continuous_on_iff] by (metis \<open>g z \<noteq> 0\<close> \<open>z \<in> S\<close> zero_less_norm_iff)
       then have \<delta>: "\<And>w. \<lbrakk>w \<in> S; w \<in> ball z \<delta>\<rbrakk> \<Longrightarrow> g w + g z \<noteq> 0"
-        apply (clarsimp simp: dist_norm)
-        by (metis add_diff_cancel_left' dist_0_norm dist_complex_def less_le_not_le norm_increases_online norm_minus_commute)
+        by (metis add.commute add_cancel_right_left dist_commute dist_complex_def mem_ball
+            norm_increases_online norm_not_less_zero norm_zero order_less_asym)
       have *: "(\<lambda>x. (f x - f z) / (x - z) / (g x + g z)) \<midarrow>z\<rightarrow> deriv f z / (g z + g z)"
       proof (intro tendsto_intros)
         show "(\<lambda>x. (f x - f z) / (x - z)) \<midarrow>z\<rightarrow> deriv f z"
@@ -1303,10 +1286,9 @@
           using \<open>z \<in> S\<close> \<open>0 < \<delta>\<close> by simp
         show "\<And>x. \<lbrakk>x \<in> ball z \<delta> \<inter> S; x \<noteq> z\<rbrakk>
                   \<Longrightarrow> (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
-          using \<delta>
-          apply (simp add: geq \<open>z \<in> S\<close> divide_simps)
-          apply (auto simp: algebra_simps power2_eq_square)
-          done
+          using \<delta> \<open>z \<in> S\<close>
+          apply (simp add: geq field_split_simps power2_eq_square)
+          by (metis distrib_left mult_cancel_right)
       qed
       then show "\<exists>f'. (g has_field_derivative f') (at z)" ..
     qed
@@ -1401,7 +1383,7 @@
       assume g: "g holomorphic_on ball 0 1" "\<forall>z\<in>ball 0 1. g z \<in> S \<and> f (g z) = z"
         and "\<forall>z\<in>S. cmod (f z) < 1 \<and> g (f z) = z"
       then have "S = g ` (ball 0 1)"
-        by (force simp:)
+        by force
       then have "open S"
         by (metis open_ball g inj_on_def open_mapping_thm3)
     }
@@ -1480,9 +1462,10 @@
         proof -
           have "closed_segment t u \<subseteq> {0..1}"
             using closed_segment_eq_real_ivl t that by auto
+          then have "\<And>r. \<lbrakk>r \<in> closed_segment t u\<rbrakk> \<Longrightarrow> dist (p t) (p r) < cmod (p t - \<zeta>)"
+            by (smt (verit, best) d dist_commute dist_in_closed_segment subsetD \<open>dist u t < d\<close>)
           then have piB: "path_image(subpath t u p) \<subseteq> ?B"
-            apply (clarsimp simp add: path_image_subpath_gen)
-            by (metis subsetD le_less_trans \<open>dist u t < d\<close> d dist_commute dist_in_closed_segment)
+            by (auto simp: path_image_subpath_gen)
           have *: "path (g \<circ> subpath t u p)"
           proof (rule path_continuous_image)
             show "path (subpath t u p)"
@@ -1561,9 +1544,7 @@
     qed
     show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
       by (rule continuous_intros)+
-    show "(\<lambda>w. \<zeta> + exp w) \<in> UNIV \<rightarrow> -{\<zeta>}"
-      by auto
-  qed
+  qed auto
   then have "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
     by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
   then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"