# HG changeset patch
# User paulson
# Date 1676978723 0
# Node ID 5158dc9d096bc5101f88b1a3debc2c2af608b143
# Parent  cf6947717650ceed631f318368215f12d073743e# Parent  66c7ec736c36bd2316a90f2a6bf9ac665a6683e5
merged

diff -r cf6947717650 -r 5158dc9d096b src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -2438,69 +2438,28 @@
 
 declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
 
+(*Seemingly impossible to use DERIV_power_int without introducing the assumption z\<in>S*)
 lemma has_field_derivative_powr_of_int:
   fixes z :: complex
-  assumes gderiv:"(g has_field_derivative gd) (at z within S)" and "g z\<noteq>0"
+  assumes gderiv: "(g has_field_derivative gd) (at z within S)" and "g z \<noteq> 0"
   shows "((\<lambda>z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within S)"
 proof -
-  define dd where "dd = of_int n * g z powr (of_int (n - 1)) * gd"
-  obtain e where "e>0" and e_dist:"\<forall>y\<in>S. dist z y < e \<longrightarrow> g y \<noteq> 0"
-    using DERIV_continuous[OF gderiv,THEN continuous_within_avoid] \<open>g z\<noteq>0\<close> by auto
-  have ?thesis when "n\<ge>0"
-  proof -
-    define dd' where "dd' = of_int n * g z ^ (nat n - 1) * gd"
-    have "dd=dd'"
-    proof (cases "n=0")
-      case False
-      then have "n-1 \<ge>0" using \<open>n\<ge>0\<close> by auto
-      then have "g z powr (of_int (n - 1)) = g z ^ (nat n - 1)"
-        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] by (simp add: nat_diff_distrib')
-      then show ?thesis unfolding dd_def dd'_def by simp
-    qed (simp add:dd_def dd'_def)
-    then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)
-                \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)"
-      by simp
-    also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)"
-    proof (rule has_field_derivative_cong_eventually)
-      show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n"
-        unfolding eventually_at by (metis e_dist \<open>e>0\<close> dist_commute powr_of_int that)
-    qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
-    also have "\<dots>" unfolding dd'_def using gderiv that
-      by (auto intro!: derivative_eq_intros)
-    finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)" .
-    then show ?thesis unfolding dd_def by simp
-  qed
-  moreover have ?thesis when "n<0"
-  proof -
-    define dd' where "dd' = of_int n / g z ^ (nat (1 - n)) * gd"
-    have "dd=dd'"
-    proof -
-      have "g z powr of_int (n - 1) = inverse (g z ^ nat (1-n))"
-        using powr_of_int[OF \<open>g z\<noteq>0\<close>,of "n-1"] that by auto
-      then show ?thesis
-        unfolding dd_def dd'_def by (simp add: divide_inverse)
-    qed
-    then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)
-                \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)"
-      by simp
-    also have "\<dots> \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)"
-    proof (rule has_field_derivative_cong_eventually)
-      show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))"
-         unfolding eventually_at
-         by (metis \<open>e>0\<close> e_dist dist_commute linorder_not_le powr_of_int that)
-    qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
-    also have "\<dots>"
-    proof -
-      have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)"
-        by auto
-      then show ?thesis
-        unfolding dd'_def using gderiv that \<open>g z\<noteq>0\<close>
-        by (auto intro!: derivative_eq_intros simp add:field_split_simps power_add[symmetric])
-    qed
-    finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)" .
-    then show ?thesis unfolding dd_def by simp
-  qed
-  ultimately show ?thesis by force
+  obtain e where "e>0" and e_dist: "\<forall>y\<in>S. dist z y < e \<longrightarrow> g y \<noteq> 0"
+    using DERIV_continuous assms continuous_within_avoid gderiv by blast
+  define D where "D = of_int n * g z powr (of_int (n - 1)) * gd"
+  define E where "E = of_int n * g z powi (n - 1) * gd"
+  have "((\<lambda>z. g z powr of_int n) has_field_derivative D) (at z within S)
+    \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative E) (at z within S)"
+    using assms complex_powr_of_int D_def E_def by presburger
+  also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z powi n) has_field_derivative E) (at z within S)"
+  proof (rule has_field_derivative_cong_eventually)
+    show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x powi n"
+      unfolding eventually_at by (metis \<open>0 < e\<close> complex_powr_of_int dist_commute e_dist)
+  qed (simp add: assms complex_powr_of_int)
+  also have "((\<lambda>z. g z powi n) has_field_derivative E) (at z within S)"
+    unfolding E_def using gderiv assms by (auto intro!: derivative_eq_intros)
+  finally show ?thesis
+    by (simp add: D_def) 
 qed
 
 lemma field_differentiable_powr_of_int:
@@ -3832,15 +3791,8 @@
 
 lemma continuous_within_Arcsin_real:
     "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
-proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
-  case True then show ?thesis
-    using continuous_on_Arcsin_real continuous_on_eq_continuous_within
-    by blast
-next
-  case False
-  with closed_real_abs_le [of 1] show ?thesis
-    by (rule continuous_within_closed_nontrivial)
-qed
+  using closed_real_abs_le continuous_on_Arcsin_real continuous_on_eq_continuous_within 
+        continuous_within_closed_nontrivial by blast
 
 lemma continuous_on_Arccos_real:
     "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
@@ -3858,15 +3810,8 @@
 
 lemma continuous_within_Arccos_real:
     "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
-proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
-  case True then show ?thesis
-    using continuous_on_Arccos_real continuous_on_eq_continuous_within
-    by blast
-next
-  case False
-  with closed_real_abs_le [of 1] show ?thesis
-    by (rule continuous_within_closed_nontrivial)
-qed
+  using closed_real_abs_le continuous_on_Arccos_real continuous_on_eq_continuous_within 
+        continuous_within_closed_nontrivial by blast
 
 lemma sinh_ln_complex: "x \<noteq> 0 \<Longrightarrow> sinh (ln x :: complex) = (x - inverse x) / 2"
   by (simp add: sinh_def exp_minus scaleR_conv_of_real exp_of_real)
diff -r cf6947717650 -r 5158dc9d096b src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -696,7 +696,7 @@
 
 lemma nn_integral_has_integral_lebesgue:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes nonneg: "\<And>x. 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
+  assumes nonneg: "\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
   shows "integral\<^sup>N lborel (\<lambda>x. indicator \<Omega> x * f x) = I"
 proof -
   from I have "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> lebesgue \<rightarrow>\<^sub>M borel"
@@ -713,8 +713,9 @@
     by (rule nn_integral_has_integral_lborel[rotated 2]) auto
   also have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = integral\<^sup>N lborel (\<lambda>x. abs (indicator \<Omega> x * f x))"
     using eq by (intro nn_integral_cong_AE) auto
-  finally show ?thesis
-    using nonneg by auto
+  also have "(\<lambda>x. abs (indicator \<Omega> x * f x)) = (\<lambda>x. indicator \<Omega> x * f x)"
+    using nonneg by (auto simp: indicator_def fun_eq_iff)
+  finally show ?thesis .
 qed
 
 lemma has_integral_iff_nn_integral_lebesgue:
@@ -741,6 +742,38 @@
     using f by (auto simp: nn_integral_completion)
 qed
 
+lemma set_nn_integral_lborel_eq_integral:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes "set_borel_measurable borel A f"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) < \<infinity>"
+  shows "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) = integral A f"
+proof -
+  have eq: "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) = (\<integral>\<^sup>+x. ennreal (indicator A x * f x) \<partial>lborel)"
+    by (intro nn_integral_cong) (auto simp: indicator_def)
+  also have "\<dots> = integral UNIV (\<lambda>x. indicator A x * f x)"
+    using assms eq by (intro nn_integral_lborel_eq_integral)
+                      (auto simp: indicator_def set_borel_measurable_def)
+  also have "integral UNIV (\<lambda>x. indicator A x * f x) = integral A (\<lambda>x. indicator A x * f x)"
+    by (rule integral_spike_set) (auto intro: empty_imp_negligible)
+ 
+  also have "\<dots> = integral A f"
+    by (rule integral_cong) (auto simp: indicator_def)
+  finally show ?thesis .
+qed
+
+lemma nn_integral_has_integral_lebesgue':
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes nonneg: "\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
+  shows "integral\<^sup>N lborel (\<lambda>x. ennreal (f x) * indicator \<Omega> x) = ennreal I"
+proof -
+  have "integral\<^sup>N lborel (\<lambda>x. ennreal (f x) * indicator \<Omega> x) =
+        integral\<^sup>N lborel (\<lambda>x. ennreal (indicator \<Omega> x * f x))"
+    by (intro nn_integral_cong) (auto simp: indicator_def)
+  also have "\<dots> = ennreal I"
+    using assms by (intro nn_integral_has_integral_lebesgue)
+  finally show ?thesis .
+qed
+
 context
   fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
 begin
@@ -959,7 +992,7 @@
     show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
       using f has_integral_implies_lebesgue_measurable[of f _ S] by (auto simp: integrable_on_def)
     show "(\<integral>\<^sup>+ x. ennreal (norm (indicator S x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
-      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ S]
+      using nf nn_integral_has_integral_lebesgue[of _ "\<lambda>x. norm (f x)"]
       by (auto simp: integrable_on_def nn_integral_completion)
   qed
 qed
diff -r cf6947717650 -r 5158dc9d096b src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -76,6 +76,22 @@
     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
 qed
 
+lemma set_integrable_bound:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+    and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
+  assumes "set_integrable M A f" "set_borel_measurable M A g"
+  assumes "AE x in M. x \<in> A \<longrightarrow> norm (g x) \<le> norm (f x)"
+  shows   "set_integrable M A g"
+  unfolding set_integrable_def
+proof (rule Bochner_Integration.integrable_bound)
+  from assms(1) show "integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+    by (simp add: set_integrable_def)
+  from assms(2) show "(\<lambda>x. indicat_real A x *\<^sub>R g x) \<in> borel_measurable M"
+    by (simp add: set_borel_measurable_def)
+  from assms(3) show "AE x in M. norm (indicat_real A x *\<^sub>R g x) \<le> norm (indicat_real A x *\<^sub>R f x)"
+    by eventually_elim (simp add: indicator_def)
+qed
+
 lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
   by (auto simp: set_lebesgue_integral_def)
 
@@ -626,6 +642,11 @@
 "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
 "\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
+lemma set_nn_integral_cong:
+  assumes "M = M'" "A = B" "\<And>x. x \<in> space M \<inter> A \<Longrightarrow> f x = g x"
+  shows   "set_nn_integral M A f = set_nn_integral M' B g"
+  by (metis (mono_tags, lifting) IntI assms indicator_simps(2) mult_eq_0_iff nn_integral_cong)
+
 lemma nn_integral_disjoint_pair:
   assumes [measurable]: "f \<in> borel_measurable M"
           "B \<in> sets M" "C \<in> sets M"
diff -r cf6947717650 -r 5158dc9d096b src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -344,7 +344,7 @@
 lemma holomorphic_factor_unique:
   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) powr n \<and> g w\<noteq>0 \<and> f w =  h w * (w - z) powr m \<and> h w\<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"
   shows "n=m"
 proof -
@@ -353,14 +353,14 @@
   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) powr (n - m) * g w"])
-      have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powr(n-m) * g w"
-        using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps powr_diff) force
+    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>
-            \<Longrightarrow> (x' - z) powr (n - m) * g x' = h x'" for x' by auto
+            \<Longrightarrow> (x' - z) powi (n - m) * g x' = h x'" for x' by auto
     next
       define F where "F \<equiv> at z within ball z r"
-      define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
+      define f' where "f' \<equiv> \<lambda>x. (x - z) powi (n-m)"
       have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
         using \<open>n>m\<close>
@@ -381,14 +381,14 @@
   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) powr (m - n) * h w"])
-      have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powr (m-n) * h w" using \<open>m>n\<close> asm
-        by (simp add:field_simps powr_diff) force
+    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
       then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
-            \<Longrightarrow> (x' - z) powr (m - n) * h x' = g x'" for x' by auto
+            \<Longrightarrow> (x' - z) powi (m - n) * h x' = g x'" for x' by auto
     next
       define F where "F \<equiv> at z within ball z r"
-      define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
+      define f' where "f' \<equiv>\<lambda>x. (x - z) powi (m-n)"
       have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
       moreover have "continuous F f'" unfolding f'_def F_def continuous_def
         using \<open>m>n\<close>
@@ -414,23 +414,23 @@
       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>
   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) powr 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 -
   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) powr (of_int 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))"
   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) powr (of_int n) \<and> g w \<noteq> 0"
+    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"
         and "fac n2 g2 r2" using g2_asm unfolding P_def fac_def by auto
     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) powr n1 \<and> g1 w\<noteq>0
-        \<and> f w = g2 w * (w - z) powr n2  \<and> g2 w\<noteq>0"
+    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"
       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>
@@ -533,19 +533,18 @@
     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) powr of_int n  \<and> g w \<noteq> 0)"
+            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) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
-        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
-            powr_minus that)
+      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)
     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) powr of_int 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
@@ -583,15 +582,15 @@
 
 lemma not_essential_powr[singularity_intros]:
   assumes "LIM w (at z). f w :> (at x)"
-  shows "not_essential (\<lambda>w. (f w) powr (of_int n)) z"
+  shows "not_essential (\<lambda>w. (f w) powi n) z"
 proof -
-  define fp where "fp=(\<lambda>w. (f w) powr (of_int n))"
+  define fp where "fp=(\<lambda>w. (f w) powi n)"
   have ?thesis when "n>0"
   proof -
     have "(\<lambda>w.  (f w) ^ (nat n)) \<midarrow>z\<rightarrow> x ^ nat n"
       using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
     then have "fp \<midarrow>z\<rightarrow> x ^ nat n" unfolding fp_def
-      by (smt (verit, best) LIM_equal of_int_of_nat power_eq_0_iff powr_nat that zero_less_nat_eq)
+      by (smt (verit) LIM_cong power_int_def that)
     then show ?thesis unfolding not_essential_def fp_def by auto
   qed
   moreover have ?thesis when "n=0"
@@ -615,7 +614,7 @@
     proof (elim filterlim_mono_eventually)
       show "\<forall>\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x"
         using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
-        by (smt (verit, ccfv_threshold) eventually_mono powr_of_int that)
+        by (smt (verit) eventuallyI power_int_def power_inverse that)
     qed auto
     then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
   next
@@ -624,8 +623,7 @@
     have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
       using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
     then have "fp \<midarrow>z\<rightarrow> ?xx"
-      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
-          powr_of_int that zero_less_nat_eq)
+      by (smt (verit, best) LIM_cong fp_def power_int_def power_inverse that)
     then show ?thesis unfolding fp_def not_essential_def by auto
   qed
   ultimately show ?thesis by linarith
@@ -633,7 +631,7 @@
 
 lemma isolated_singularity_at_powr[singularity_intros]:
   assumes "isolated_singularity_at f z" "\<forall>\<^sub>F w in (at z). f w\<noteq>0"
-  shows "isolated_singularity_at (\<lambda>w. (f w) powr (of_int n)) z"
+  shows "isolated_singularity_at (\<lambda>w. (f w) powi n) z"
 proof -
   obtain r1 where "r1>0" "f analytic_on ball z r1 - {z}"
     using assms(1) unfolding isolated_singularity_at_def by auto
@@ -642,8 +640,8 @@
   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) powr of_int n) holomorphic_on ball z r3 - {z}"
-    by (intro holomorphic_on_powr_of_int) (use r1 r2 in \<open>auto simp: dist_commute r3_def\<close>)
+  have "(\<lambda>w. (f w) powi n) holomorphic_on ball z r3 - {z}"
+    by (intro holomorphic_on_power_int) (use r1 r2 in \<open>auto simp: dist_commute r3_def\<close>)
   moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith
   ultimately show ?thesis
     by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
@@ -657,13 +655,13 @@
 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) powr of_int 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 holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] 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) powr of_int fn" "fp w \<noteq> 0"
+    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) powr of_int fn \<noteq>0"
+    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
@@ -715,24 +713,24 @@
   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) powr of_int 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 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"
           and gr: "gp holomorphic_on cball z gr"
-                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powr of_int 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 holomorphic_factor_puncture[OF g_iso g_ness g_nconst,THEN ex1_implies_ex] 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) powr (of_int (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) powr of_int fn" "fp w\<noteq>0"
+      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) powr of_int gn" "gp w \<noteq> 0"
+      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) powr (of_int (fn+gn))" "fp w*gp w\<noteq>0"
-        unfolding fg_def by (auto simp add:powr_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
 
     have [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z"
@@ -745,9 +743,8 @@
       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"
-        using Lim_transform_within[OF _ \<open>r1>0\<close>]
-        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
-            singletonD that)
+         apply (elim 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
     moreover have ?thesis when "fn+gn=0"
@@ -771,7 +768,8 @@
         using filterlim_divide_at_infinity by blast
       then have "is_pole fg z" unfolding is_pole_def
         apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>])
-        by (simp_all add: dist_commute fg_times of_int_of_nat powr_minus_divide that)
+        using that
+        by (simp_all add: dist_commute fg_times of_int_of_nat divide_simps power_int_def del: minus_add_distrib)
       then show ?thesis unfolding not_essential_def fg_def by auto
     qed
     ultimately show ?thesis unfolding not_essential_def fg_def by fastforce
@@ -1091,13 +1089,13 @@
 
 definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
   "zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
-                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n)
+                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powi n
                    \<and> h w \<noteq>0)))"
 
 definition\<^marker>\<open>tag important\<close> zor_poly
     ::"[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) powr (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:
@@ -1107,10 +1105,10 @@
       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) powr 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 -
   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) powr (of_int 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))"
   have "\<exists>!n. \<exists>g r. P n g r"
     using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
   then have "\<exists>g r. P n g r"
@@ -1163,20 +1161,20 @@
 
   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) powr of_int 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) powr (of_int (-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) powr of_int fn" "fp w\<noteq>0"
+    have "f w = fp w * (w - z) powi fn" "fp w\<noteq>0"
       using fr(2)[rule_format,of w] that by auto
-    then show "vf w = (inverse (fp w)) * (w - z) powr (of_int (-fn))" "inverse (fp w)\<noteq>0"
-      unfolding vf_def by (auto simp add:powr_minus)
+    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) powr of_int vfn \<and> vfp w \<noteq> 0)"
+      "(\<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 .
@@ -1195,8 +1193,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) powr complex_of_int vfn \<and>
-               vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w - z) powr complex_of_int (- 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)
@@ -1225,7 +1223,7 @@
   obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
       holo1:"zor_poly f z holomorphic_on cball z r1" and
       rball1:"\<forall>w\<in>cball z r1 - {z}.
-           f w = zor_poly f z w * (w - z) powr of_int (zorder f z) \<and>
+           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
 
@@ -1245,7 +1243,7 @@
   ultimately obtain r2 where "r2>0" "zor_poly ff 0 0 \<noteq> 0" and
       holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
       rball2:"\<forall>w\<in>cball 0 r2 - {0}.
-           ff w = zor_poly ff 0 w * w powr of_int (zorder ff 0) \<and>
+           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
 
@@ -1255,9 +1253,9 @@
   have "zor_poly f z w = zor_poly ff 0 (w - z)"
     if "w\<in>ball z r - {z}" for w
   proof -
-    define n::complex where "n= of_int (zorder f z)"
+    define n where "n \<equiv> zorder f z"
 
-    have "f w = zor_poly f z w * (w - z) powr n"
+    have "f w = zor_poly f z w * (w - z) powi n"
     proof -
       have "w\<in>cball z r1 - {z}"
         using r_def that by auto
@@ -1265,26 +1263,25 @@
       show ?thesis unfolding n_def by auto
     qed
 
-    moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powr 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)
-                            powr of_int (zorder ff 0)"
+                            powi (zorder ff 0)"
         by simp
       moreover have "of_int (zorder ff 0) = n"
         unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
       ultimately show ?thesis unfolding ff_def by auto
     qed
-    ultimately have "zor_poly f z w * (w - z) powr n
-                = zor_poly ff 0 (w - z) * (w - z) powr n"
+    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) powr n \<noteq>0"
+    moreover have "(w - z) powi n \<noteq>0"
       using that by auto
     ultimately show ?thesis
-      apply (subst (asm) mult_cancel_right)
-      by (simp add:ff_def)
+      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)"
@@ -1327,31 +1324,32 @@
     using fg_nconst by (auto elim!:frequently_elim1)
   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) powr of_int 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"
           and gr: "gp holomorphic_on cball z gr"
-                  "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powr of_int 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) powr (of_int (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) powr of_int fn" "fp w\<noteq>0"
+    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) powr of_int gn" "gp w \<noteq> 0"
+    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) powr (of_int (fn+gn))" "fp w*gp w\<noteq>0"
-      unfolding fg_def by (auto simp add:powr_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"
           and fgr: "fgp holomorphic_on cball z fgr"
-                  "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w - z) powr of_int 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 "fgp z \<noteq> 0 \<and> (\<exists>r>0. fgp holomorphic_on cball z r
-            \<and> (\<forall>w\<in>cball z r - {z}. fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0))"
+            \<and> (\<forall>w\<in>cball z r - {z}. fg w = fgp w * (w - z) powi fgn \<and> fgp w \<noteq> 0))"
       apply (rule zorder_exist[of fg z, folded fgn_def fgp_def])
       subgoal unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] .
       subgoal unfolding fg_def using not_essential_times[OF f_ness g_ness f_iso g_iso] .
@@ -1371,8 +1369,8 @@
       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
       from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)]
-      show "fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0
-              \<and> fg w = fp w * gp w * (w - z) powr of_int (fn + gn) \<and> fp w * gp w \<noteq> 0" by auto
+      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" by auto
     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)
@@ -1431,10 +1429,10 @@
     \<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) powr of_int 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) powr of_int 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)
@@ -1453,7 +1451,7 @@
         by auto
     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) powr of_int n \<and> g w \<noteq> 0)"
+            "(\<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,6) open_contains_cball_eq by blast
@@ -1461,7 +1459,7 @@
     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) powr of_int 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
@@ -1469,22 +1467,23 @@
   have fz_lim: "f\<midarrow> z \<rightarrow> f z"
     by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
   have gz_lim: "g \<midarrow>z\<rightarrow>g z"
-    by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
-        continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on)
+    using r
+    by (meson Elementary_Metric_Spaces.open_ball analytic_at analytic_at_imp_isCont 
+        ball_subset_cball centre_in_ball holomorphic_on_subset isContD)
   have if_0:"if f z=0 then n > 0 else n=0"
   proof -
-    have "(\<lambda>w. g w * (w - z) powr of_int 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) powr of_int 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 powr_tendsto:"(\<lambda>w. (w - z) powr of_int 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"
-        using powr_tendsto Lim_transform_within[where d=r]
-        by (fastforce simp: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
+        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
       moreover have False when "n=0"
       proof -
@@ -1499,8 +1498,8 @@
       have False when "n>0"
       proof -
         have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
-          using powr_tendsto Lim_transform_within[where d=r]
-          by (fastforce simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
+          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"
           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
@@ -1510,11 +1509,13 @@
     moreover have False when "n<0"
     proof -
       have "(\<lambda>w. inverse ((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
-           "(\<lambda>w.((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0"
-        apply (smt (verit, ccfv_SIG) LIM_cong eq_iff_diff_eq_0 powr_of_int powr_tendsto that)
+        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"
         using that by (auto intro!:tendsto_eq_intros)
-      from tendsto_mult[OF this,simplified]
-      have "(\<lambda>x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \<midarrow>z\<rightarrow> 0" .
+      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"
         by (elim Lim_transform_within_open[where s=UNIV],auto)
       then show False using LIM_const_eq by fastforce
@@ -1531,10 +1532,10 @@
       fix x assume "0 < dist x z" "dist x z < r"
       then have "x \<in> cball z r - {z}" "x\<noteq>z"
         unfolding cball_def by (auto simp add: dist_commute)
-      then have "f x = g x * (x - z) powr of_int n"
+      then have "f x = g x * (x - z) powi n"
         using r(4)[rule_format,of x] by simp
       also have "... = g x * (x - z) ^ nat n"
-        by (smt (verit) \<open>x \<noteq> z\<close> if_0 powr_of_int right_minus_eq)
+        by (smt (verit, best) if_0 int_nat_eq power_int_of_nat)
       finally show "f x = g x * (x - z) ^ nat n" .
     qed
     moreover have "(\<lambda>w. g w * (w-z) ^ nat n) \<midarrow>z\<rightarrow> g w * (w-z) ^ nat n"
@@ -1543,9 +1544,10 @@
     then show ?thesis using \<open>g z\<noteq>0\<close> True by auto
   next
     case False
-    then have "f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0"
+    then have "f w = g w * (w - z) powi n \<and> g w \<noteq> 0"
       using r(4) that by auto
-    then show ?thesis using False if_0 powr_of_int by (auto split:if_splits)
+    then show ?thesis
+      by (smt (verit, best) False if_0 int_nat_eq power_int_of_nat)
   qed
   ultimately show ?thesis using r by auto
 qed
@@ -1560,10 +1562,10 @@
     \<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) powr of_int 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) powr of_int 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)
@@ -1576,7 +1578,7 @@
         by auto
     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) powr of_int n \<and> g w \<noteq> 0)"
+            "(\<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
@@ -1584,7 +1586,7 @@
     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) powr of_int 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
@@ -1599,7 +1601,7 @@
     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"])
-      using r powr_of_int \<open>\<not> n < 0\<close> by auto
+      by (simp add: \<open>\<not> n < 0\<close> linorder_not_le power_int_def r(1) r(4))
     moreover have "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow> c"
     proof (cases "n=0")
       case True
@@ -1616,14 +1618,14 @@
       unfolding is_pole_def by blast
   qed
   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> powr_of_int
-    by (metis Diff_iff divide_inverse eq_iff_diff_eq_0 insert_iff linorder_not_le)
+    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
 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) powr 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
@@ -1634,9 +1636,9 @@
   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) powr 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) powr (of_int 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))"
   have "P n g r"
     unfolding P_def using r assms(3,4,5) by auto
   then have "\<exists>g r. P n g r" by auto
@@ -1663,7 +1665,7 @@
             assms holomorphic_on_subset isolated_singularity_at_def openE)
     qed
     moreover
-    have "\<forall>\<^sub>F w in at z. g w * (w - z) powr 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
@@ -1678,7 +1680,7 @@
         have "z' \<in> cball z r"
           unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
         then show " z' \<in> s" using r(2) by blast
-        show "g z' * (z' - z) powr of_int n \<noteq> 0"
+        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
       ultimately show "\<exists>x\<in>UNIV. x \<noteq> z \<and> dist x z < d \<and> f x \<noteq> 0" by auto
@@ -1813,7 +1815,7 @@
   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) powr (of_int n) \<and> h w\<noteq>0))"
+                    \<and> (\<forall>w\<in>cball z r - {z}. ff w = h w * (w-z) powi n \<and> h w\<noteq>0))"
   have "(\<exists>r. P f n h r) = (\<exists>r. P g n h r)" for n h
   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
@@ -1825,9 +1827,9 @@
       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) powr of_int 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) powr of_int 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)
@@ -1859,7 +1861,7 @@
 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) powr of_int n \<and> h w \<noteq> 0))"
+              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
@@ -1874,17 +1876,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"
-  using zorder_eqI [OF sz] by (simp add: powr_minus_divide)
+  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) powr - 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) powr of_int (zorder f z))"
+       "(\<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) powr - zorder f z"
-    by (auto simp: field_simps powr_minus)
+  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
   thus ?thesis by eventually_elim (insert *, auto)
@@ -1924,27 +1926,27 @@
   fixes f :: "complex \<Rightarrow> complex" and z0 :: complex
   defines "n \<equiv> zorder f z0"
   assumes "isolated_singularity_at f z0" "not_essential f z0" "\<exists>\<^sub>F w in at z0. f w \<noteq> 0"
-  assumes lim: "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> c) F"
+  assumes lim: "((\<lambda>x. f (g x) * (g x - z0) powi - n) \<longlongrightarrow> c) F"
   assumes g: "filterlim g (at z0) F" and "F \<noteq> bot"
   shows   "zor_poly f z0 z0 = c"
 proof -
   from zorder_exist[OF assms(2-4)] obtain r where
     r: "r > 0" "zor_poly f z0 holomorphic_on cball z0 r"
-       "\<And>w. w \<in> cball z0 r - {z0} \<Longrightarrow> f w = zor_poly f z0 w * (w - z0) powr n"
+       "\<And>w. w \<in> cball z0 r - {z0} \<Longrightarrow> f w = zor_poly f z0 w * (w - z0) powi n"
     unfolding n_def by blast
   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
-  hence "eventually (\<lambda>w. zor_poly f z0 w = f w * (w - z0) powr - n) (at z0)"
-    by eventually_elim (insert r, auto simp: field_simps powr_minus)
+  hence "eventually (\<lambda>w. zor_poly f z0 w = f w * (w - z0) powi - n) (at z0)"
+    by eventually_elim (insert r, auto simp: field_simps power_int_minus)
   moreover have "continuous_on (ball z0 r) (zor_poly f z0)"
     using r by (intro holomorphic_on_imp_continuous_on) auto
   with r(1,2) 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 .
-  ultimately have "((\<lambda>w. f w * (w - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
+  ultimately have "((\<lambda>w. f w * (w - z0) powi - n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
     by (blast intro: Lim_transform_eventually)
-  hence "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) F"
+  hence "((\<lambda>x. f (g x) * (g x - z0) powi - n) \<longlongrightarrow> zor_poly f z0 z0) F"
     by (rule filterlim_compose[OF _ g])
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
 qed
@@ -2082,9 +2084,9 @@
   proof (rule zorder_eqI)
     show "open (ball x r)" "x \<in> ball x r"
       using \<open>r > 0\<close> by auto
-    show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powr of_int (- int (Suc n))"
+    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 powr_diff powr_minus powr_nat' divide_simps)
+      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>)
   thus "zorder f' x = zorder f x - 1"
     using n by (simp add: n_def)
@@ -2306,10 +2308,10 @@
   define nn where "nn = nat (-n)"
 
   obtain r where "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
-       w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+       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) powr of_int 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"
@@ -2323,18 +2325,17 @@
       using \<open>n<0\<close>
       by (auto intro!:tendsto_eq_intros filterlim_atI
               simp add:eventually_at_filter)
-    then show "LIM x at z. (x - z) powr of_int n :> at_infinity"
+    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) powr of_int n"
+      have "inverse ((x - z) ^ nat (-n)) = (x - z) powi n"
         if "x\<noteq>z" for x
-        apply (subst powr_of_int)
-        using \<open>n<0\<close> using that by auto
+        by (metis \<open>n < 0\<close> linorder_not_le power_int_def power_inverse)
       then show "\<forall>\<^sub>F x in at z. inverse ((x - z) ^ nat (-n))
-                  = (x - z) powr of_int n"
+                  = (x - z) powi n"
         by (simp add: eventually_at_filter)
     qed auto
   qed
-  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w - z) powr of_int n"
+  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w - z) powi n"
     unfolding eventually_at_le
     apply (rule exI[where x=r])
     using w_Pn \<open>r>0\<close> by (simp add: dist_commute)
@@ -2429,7 +2430,7 @@
 
   obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
           and "(\<forall>w\<in>cball z r - {z}. f w
-                            = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+                            = 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
@@ -2475,10 +2476,9 @@
     show "g z \<noteq> 0"
       unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
     show "deriv f w =
-         (deriv P w * (w - z) + of_int n * P w) * (w - z) powr of_int (n - 1)"
+         (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
-      apply (subst complex_powr_of_int)
-      using deriv_f_eq that unfolding D_def by auto
+      using D_def deriv_f_eq that by blast
   qed
 qed
 
diff -r cf6947717650 -r 5158dc9d096b src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -1091,7 +1091,7 @@
   case True
   define n where "n = zorder f 0"
   obtain r where r: "zor_poly f 0 0 \<noteq> 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0"
-                    "\<forall>w\<in>cball 0 r - {0}. f w = zor_poly f 0 w * w powr of_int n \<and>
+                    "\<forall>w\<in>cball 0 r - {0}. f w = zor_poly f 0 w * w powi n \<and>
                                          zor_poly f 0 w \<noteq> 0"
     using zorder_exist[OF assms True] unfolding n_def by auto
   have holo: "zor_poly f 0 holomorphic_on ball 0 r"
@@ -1144,7 +1144,7 @@
       from zorder_exist[OF iso ness this,folded df_def]
       obtain r where "r>0" and df_holo:"df holomorphic_on cball 0 r" and "df 0 \<noteq> 0"
           "\<forall>w\<in>cball 0 r - {0}.
-             f (z + w) = df w * w powr of_int (zorder (\<lambda>w. f (z + w)) 0) \<and>
+             f (z + w) = df w * w powi (zorder (\<lambda>w. f (z + w)) 0) \<and>
              df w \<noteq> 0"
         by auto
       then have df_nz:"\<forall>w\<in>ball 0 r. df w\<noteq>0" by auto
@@ -1340,7 +1340,7 @@
       by (auto simp: eval_fps_at_0 G_def)
   next
     fix w :: complex assume "w \<in> A \<inter> eball 0 (fls_conv_radius F)" "w \<noteq> 0"
-    thus "f w = eval_fps G w * (w - 0) powr of_int (fls_subdegree F)"
+    thus "f w = eval_fps G w * (w - 0) powi (fls_subdegree F)"
       using A unfolding G_def
       by (subst eval_fps_fls_base_factor)
          (auto simp: complex_powr_of_int power_int_minus field_simps)
@@ -1567,7 +1567,7 @@
   have n_altdef: "n = fls_subdegree F"
     using has_laurent_expansion_zorder_0 [OF assms(1)] by (simp add: n_def)
   obtain r where r: "zor_poly f 0 0 \<noteq> 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0"
-                    "\<forall>w\<in>cball 0 r - {0}. f w = zor_poly f 0 w * w powr of_int n \<and>
+                    "\<forall>w\<in>cball 0 r - {0}. f w = zor_poly f 0 w * w powi n \<and>
                                          zor_poly f 0 w \<noteq> 0"
     using zorder_exist[OF * freq] unfolding n_def by auto
   obtain r' where r': "r' > 0" "\<forall>x\<in>ball 0 r'-{0}. eval_fls F x = f x"
@@ -1590,7 +1590,7 @@
       show ?case
       proof (cases "w = 0")
         case False
-        hence "f w = zor_poly f 0 w * w powr of_int n"
+        hence "f w = zor_poly f 0 w * w powi n"
           using r w by auto
         thus ?thesis using False
           by (simp add: powr_minus complex_powr_of_int power_int_minus)
@@ -2728,7 +2728,7 @@
       using \<open>a \<noteq> 0\<close> by (intro holomorphic_on_compose_gen[OF _ r'(4)] holomorphic_intros) auto
     show "a ^ n * (zor_poly f (a * z) \<circ> (\<lambda>w. a * w)) z \<noteq> 0"
       using r' \<open>a \<noteq> 0\<close> by auto
-    show "f (a * w) = a ^ n * (zor_poly f (a * z) \<circ> (*) a) w * (w - z) powr of_int (zorder f (a * z))"
+    show "f (a * w) = a ^ n * (zor_poly f (a * z) \<circ> (*) a) w * (w - z) powi (zorder f (a * z))"
       if "w \<in> ball z (r' / norm a)" "w \<noteq> z" for w
     proof -
       have "f (a * w) = zor_poly f (a * z) (a * w) * (a * (w - z)) ^ n"
@@ -2736,9 +2736,9 @@
         by (auto simp: divide_simps mult_ac)
       also have "\<dots> = a ^ n * zor_poly f (a * z) (a * w) * (w - z) ^ n"
         by (subst power_mult_distrib) (auto simp: mult_ac)
-      also have "(w - z) ^ n = (w - z) powr of_nat n"
-        using \<open>w \<noteq> z\<close> by (subst powr_nat') auto
-      also have "of_nat n = of_int (zorder f (a * z))"
+      also have "(w - z) ^ n = (w - z) powi of_nat n"
+        by simp
+      also have "of_nat n = zorder f (a * z)"
         using r'(1) by (auto simp: n_def split: if_splits)
       finally show ?thesis
         unfolding o_def n_def .
diff -r cf6947717650 -r 5158dc9d096b src/HOL/Complex_Analysis/Residue_Theorem.thy
--- a/src/HOL/Complex_Analysis/Residue_Theorem.thy	Mon Feb 20 21:53:15 2023 +0100
+++ b/src/HOL/Complex_Analysis/Residue_Theorem.thy	Tue Feb 21 11:25:23 2023 +0000
@@ -3,7 +3,9 @@
   imports Complex_Residues "HOL-Library.Landau_Symbols"
 begin
 
-text \<open>Could be moved to a previous theory importing both Landau Symbols and Elementary Metric Spaces\<close>
+text \<open>Several theorems that could be moved up, 
+  IF there were a previous theory importing both Landau Symbols and Elementary Metric Spaces\<close>
+
 lemma continuous_bounded_at_infinity_imp_bounded:
   fixes f :: "real \<Rightarrow> 'a :: real_normed_field"
   assumes "f \<in> O[at_bot](\<lambda>_. 1)"
@@ -31,6 +33,66 @@
     unfolding bounded_iff by blast
 qed
 
+lemma holomorphic_on_extend:
+  assumes "f holomorphic_on S - {\<xi>}" "\<xi> \<in> interior S" "f \<in> O[at \<xi>](\<lambda>_. 1)"
+  shows   "(\<exists>g. g holomorphic_on S \<and> (\<forall>z\<in>S - {\<xi>}. g z = f z))"
+  by (subst holomorphic_on_extend_bounded) (insert assms, auto elim!: landau_o.bigE)
+
+lemma removable_singularities:
+  assumes "finite X" "X \<subseteq> interior S" "f holomorphic_on (S - X)"
+  assumes "\<And>z. z \<in> X \<Longrightarrow> f \<in> O[at z](\<lambda>_. 1)"
+  shows   "\<exists>g. g holomorphic_on S \<and> (\<forall>z\<in>S-X. g z = f z)"
+  using assms
+proof (induction arbitrary: f rule: finite_induct)
+  case empty
+  thus ?case by auto
+next
+  case (insert z0 X f)
+  from insert.prems and insert.hyps have z0: "z0 \<in> interior (S - X)"
+    by (auto simp: interior_diff finite_imp_closed)
+  hence "\<exists>g. g holomorphic_on (S - X) \<and> (\<forall>z\<in>S - X - {z0}. g z = f z)"
+    using insert.prems insert.hyps by (intro holomorphic_on_extend) auto
+  then obtain g where g: "g holomorphic_on (S - X)" "\<forall>z\<in>S - X - {z0}. g z = f z" by blast
+  have "\<exists>h. h holomorphic_on S \<and> (\<forall>z\<in>S - X. h z = g z)"
+  proof (rule insert.IH)
+    fix z0' assume z0': "z0' \<in> X"
+    hence "eventually (\<lambda>z. z \<in> interior S - (X - {z0'}) - {z0}) (nhds z0')"
+      using insert.prems insert.hyps
+      by (intro eventually_nhds_in_open open_Diff finite_imp_closed) auto
+    hence ev: "eventually (\<lambda>z. z \<in> S - X - {z0}) (at z0')"
+      unfolding eventually_at_filter 
+      by eventually_elim (insert z0' insert.hyps interior_subset[of S], auto)
+    have "g \<in> \<Theta>[at z0'](f)"
+      by (intro bigthetaI_cong eventually_mono[OF ev]) (insert g, auto)
+    also have "f \<in> O[at z0'](\<lambda>_. 1)"
+      using z0' by (intro insert.prems) auto
+    finally show "g \<in> \<dots>" .
+  qed (insert insert.prems g, auto)
+  then obtain h where "h holomorphic_on S" "\<forall>z\<in>S - X. h z = g z" by blast
+  with g have "h holomorphic_on S" "\<forall>z\<in>S - insert z0 X. h z = f z" by auto
+  thus ?case by blast
+qed
+
+lemma continuous_imp_bigo_1:
+  assumes "continuous (at x within A) f"
+  shows   "f \<in> O[at x within A](\<lambda>_. 1)"
+proof (rule bigoI_tendsto)
+  from assms show "((\<lambda>x. f x / 1) \<longlongrightarrow> f x) (at x within A)"
+    by (auto simp: continuous_within)
+qed auto
+
+lemma taylor_bigo_linear:
+  assumes "f field_differentiable at x0 within A"
+  shows   "(\<lambda>x. f x - f x0) \<in> O[at x0 within A](\<lambda>x. x - x0)"
+proof -
+  from assms obtain f' where "(f has_field_derivative f') (at x0 within A)"
+    by (auto simp: field_differentiable_def)
+  hence "((\<lambda>x. (f x - f x0) / (x - x0)) \<longlongrightarrow> f') (at x0 within A)"
+    by (auto simp: has_field_derivative_iff)
+  thus ?thesis by (intro bigoI_tendsto[where c = f']) (auto simp: eventually_at_filter)
+qed
+
+
 subsection \<open>Cauchy's residue theorem\<close>
 
 lemma get_integrable_path:
@@ -509,12 +571,12 @@
     proof -
       define po where "po \<equiv> zorder f p"
       define pp where "pp \<equiv> zor_poly f p"
-      define f' where "f' \<equiv> \<lambda>w. pp w * (w - p) powr po"
+      define f' where "f' \<equiv> \<lambda>w. pp w * (w - p) powi po"
       define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
       obtain r where "pp p\<noteq>0" "r>0" and
           "r<e1" and
           pp_holo:"pp holomorphic_on cball p r" and
-          pp_po:"(\<forall>w\<in>cball p r-{p}. f w = pp w * (w - p) powr po \<and> pp w \<noteq> 0)"
+          pp_po:"(\<forall>w\<in>cball p r-{p}. f w = pp w * (w - p) powi po \<and> pp w \<noteq> 0)"
       proof -
         have "isolated_singularity_at f p"
         proof -
@@ -565,12 +627,12 @@
           then show False using \<open>finite pz\<close> by auto
         qed
         ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r"
-                  "(\<forall>w\<in>cball p r - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)"
+                  "(\<forall>w\<in>cball p r - {p}. f w = pp w * (w - p) powi po \<and> pp w \<noteq> 0)"
           using zorder_exist[of f p,folded po_def pp_def] by auto
         define r1 where "r1=min r e1 / 2"
         have "r1<e1" unfolding r1_def using \<open>e1>0\<close> \<open>r>0\<close> by auto
         moreover have "r1>0" "pp holomorphic_on cball p r1"
-                  "(\<forall>w\<in>cball p r1 - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)"
+                  "(\<forall>w\<in>cball p r1 - {p}. f w = pp w * (w - p) powi po \<and> pp w \<noteq> 0)"
           unfolding r1_def using \<open>e1>0\<close> r by auto
         ultimately show ?thesis using that \<open>pp p\<noteq>0\<close> by auto
       qed
@@ -604,13 +666,13 @@
         define wp where "wp \<equiv> w-p"
         have "wp\<noteq>0" and "pp w \<noteq>0"
           unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
-        moreover have der_f':"deriv f' w = po * pp w * (w-p) powr (po - 1) + deriv pp w * (w-p) powr po"
+        moreover have der_f':"deriv f' w = po * pp w * (w-p) powi (po - 1) + deriv pp w * (w-p) powi po"
         proof (rule DERIV_imp_deriv)
           have "(pp has_field_derivative (deriv pp w)) (at w)"
             using DERIV_deriv_iff_has_field_derivative pp_holo \<open>w\<noteq>p\<close>
             by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset)
-          then show " (f' has_field_derivative of_int po * pp w * (w - p) powr of_int (po - 1)
-                  + deriv pp w * (w - p) powr of_int po) (at w)"
+          then show " (f' has_field_derivative of_int po * pp w * (w - p) powi (po - 1)
+                  + deriv pp w * (w - p) powi po) (at w)"
             unfolding f'_def using \<open>w\<noteq>p\<close>
             by (auto intro!: derivative_eq_intros DERIV_cong[OF has_field_derivative_powr_of_int])
         qed
@@ -620,7 +682,7 @@
           apply (unfold f'_def)
           apply (fold wp_def)
           apply (auto simp add:field_simps)
-          by (metis (no_types, lifting) diff_add_cancel mult.commute powr_add powr_to_1)
+          by (metis (no_types, lifting) mult.commute power_int_minus_mult)
       qed
       then have "cont ff p e2" unfolding cont_def
       proof (elim has_contour_integral_eq)