
diff -r 9a60a2d19a4c -r f82317de6f28 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Feb 15 12:46:12 2023 +0000
@@ -102,12 +102,7 @@
   have "((\<lambda>w. w) has_field_derivative 1) (at z)"
     by (intro derivative_intros)
   also have "?this \<longleftrightarrow> ((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)"
-  proof (rule DERIV_cong_ev)
-    have "eventually (\<lambda>w. w \<in> A) (nhds z)"
-      using assms by (intro eventually_nhds_in_open) auto
-    thus "eventually (\<lambda>w. w = exp (f w)) (nhds z)"
-      by eventually_elim (use assms in auto)
-  qed auto
+    by (smt (verit, best) assms has_field_derivative_transform_within_open)
   finally have "((\<lambda>w. exp (f w)) has_field_derivative 1) (at z)" .
   moreover have "((\<lambda>w. exp (f w)) has_field_derivative exp (f z) * deriv f z) (at z)"
     by (rule derivative_eq_intros refl)+
@@ -133,11 +128,7 @@
 theorem exp_Euler: "exp(\<i> * z) = cos(z) + \<i> * sin(z)"
 proof -
   have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) = (\<lambda>n. (\<i> * z) ^ n /\<^sub>R (fact n))"
-  proof
-    fix n
-    show "(cos_coeff n + \<i> * sin_coeff n) * z^n = (\<i> * z) ^ n /\<^sub>R (fact n)"
-      by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
-  qed
+    by (force simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
   also have "\<dots> sums (exp (\<i> * z))"
     by (rule exp_converges)
   finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
@@ -149,8 +140,7 @@
 qed
 
 corollary\<^marker>\<open>tag unimportant\<close> exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
-  using exp_Euler [of "-z"]
-  by simp
+  using exp_Euler [of "-z"] by simp
 
 lemma sin_exp_eq: "sin z = (exp(\<i> * z) - exp(-(\<i> * z))) / (2*\<i>)"
   by (simp add: exp_Euler exp_minus_Euler)
@@ -198,18 +188,7 @@
   by (metis exp_Euler [symmetric] exp_of_nat_mult mult.left_commute)
 
 lemma exp_cnj: "cnj (exp z) = exp (cnj z)"
-proof -
-  have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
-    by auto
-  also have "\<dots> sums (exp (cnj z))"
-    by (rule exp_converges)
-  finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
-  moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
-    by (metis exp_converges sums_cnj)
-  ultimately show ?thesis
-    using sums_unique2
-    by blast
-qed
+  by (simp add: cis_cnj exp_eq_polar)
 
 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   by (simp add: sin_exp_eq exp_cnj field_simps)
@@ -264,7 +243,7 @@
 subsection\<^marker>\<open>tag unimportant\<close>\<open>More on the Polar Representation of Complex Numbers\<close>
 
 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
-  by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
+  using Complex_eq Euler complex.sel by presburger
 
 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
                  (is "?lhs = ?rhs")
@@ -273,7 +252,7 @@
   then have "Re z = 0"
     by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   with \<open>?lhs\<close> show ?rhs
-    by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)
+    by (metis Re_exp cos_one_2pi_int exp_zero mult.commute mult_1 of_int_mult of_int_numeral one_complex.simps(1))
 next
   assume ?rhs then show ?lhs
     using Im_exp Re_exp complex_eq_iff
@@ -298,13 +277,7 @@
 lemma exp_integer_2pi:
   assumes "n \<in> \<int>"
   shows "exp((2 * n * pi) * \<i>) = 1"
-proof -
-  have "exp((2 * n * pi) * \<i>) = exp 0"
-    using assms unfolding Ints_def exp_eq by auto
-  also have "\<dots> = 1"
-    by simp
-  finally show ?thesis .
-qed
+  by (metis assms cis_conv_exp cis_multiple_2pi mult.assoc mult.commute)
 
 lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
   by (simp add: exp_eq)
@@ -312,15 +285,8 @@
 lemma exp_integer_2pi_plus1:
   assumes "n \<in> \<int>"
   shows "exp(((2 * n + 1) * pi) * \<i>) = - 1"
-proof -
-  from assms obtain n' where [simp]: "n = of_int n'"
-    by (auto simp: Ints_def)
-  have "exp(((2 * n + 1) * pi) * \<i>) = exp (pi * \<i>)"
-    using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
-  also have "\<dots> = - 1"
-    by simp
-  finally show ?thesis .
-qed
+  using exp_integer_2pi [OF assms]
+  by (metis cis_conv_exp cis_mult cis_pi distrib_left mult.commute mult.right_neutral)
 
 lemma inj_on_exp_pi:
   fixes z::complex shows "inj_on exp (ball z pi)"
@@ -338,7 +304,6 @@
 
 lemma cmod_add_squared:
   fixes r1 r2::real
-  assumes "r1 \<ge> 0" "r2 \<ge> 0"
   shows "(cmod (r1 * exp (\<i> * \<theta>1) + r2 * exp (\<i> * \<theta>2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 + 2 * r1 * r2 * cos (\<theta>1 - \<theta>2)" (is "(cmod (?z1 + ?z2))\<^sup>2 = ?rhs")
 proof -
   have "(cmod (?z1 + ?z2))\<^sup>2 = (?z1 + ?z2) * cnj (?z1 + ?z2)"
@@ -355,19 +320,8 @@
 
 lemma cmod_diff_squared:
   fixes r1 r2::real
-  assumes "r1 \<ge> 0" "r2 \<ge> 0"
-  shows "(cmod (r1 * exp (\<i> * \<theta>1) - r2 * exp (\<i> * \<theta>2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\<theta>1 - \<theta>2)" (is "(cmod (?z1 - ?z2))\<^sup>2 = ?rhs")
-proof -
-  have "exp (\<i> * (\<theta>2 + pi)) = - exp (\<i> * \<theta>2)"
-    by (simp add: exp_Euler cos_plus_pi sin_plus_pi)
-  then have "(cmod (?z1 - ?z2))\<^sup>2 = cmod (?z1 + r2 * exp (\<i> * (\<theta>2 + pi))) ^2"
-    by simp
-  also have "\<dots> = r1\<^sup>2 + r2\<^sup>2 + 2*r1*r2*cos (\<theta>1 - (\<theta>2 + pi))"
-    using assms cmod_add_squared by blast
-  also have "\<dots> = ?rhs"
-    by (simp add: add.commute diff_add_eq_diff_diff_swap)
-  finally show ?thesis .
-qed
+  shows "(cmod (r1 * exp (\<i> * \<theta>1) - r2 * exp (\<i> * \<theta>2)))\<^sup>2 = r1\<^sup>2 + r2\<^sup>2 - 2*r1*r2*cos (\<theta>1 - \<theta>2)" 
+  using cmod_add_squared [of r1 _ "-r2"] by simp
 
 lemma polar_convergence:
   fixes R::real
@@ -381,8 +335,7 @@
   moreover obtain k where "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"
   proof -
     have "cos (\<theta> j - \<Theta>) = ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)" for j
-      apply (subst cmod_diff_squared)
-      using assms by (auto simp: field_split_simps less_le)
+      using assms by (auto simp: cmod_diff_squared less_le)
     moreover have "(\<lambda>j. ((r j)\<^sup>2 + R\<^sup>2 - (norm(?z j - ?Z))\<^sup>2) / (2 * R * r j)) \<longlonglongrightarrow> ((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R))"
       by (intro L rR tendsto_intros) (use \<open>R > 0\<close> in force)
     moreover have "((R\<^sup>2 + R\<^sup>2 - (norm(?Z - ?Z))\<^sup>2) / (2 * R * R)) = 1"
@@ -430,19 +383,7 @@
 lemma exp_i_ne_1:
   assumes "0 < x" "x < 2*pi"
   shows "exp(\<i> * of_real x) \<noteq> 1"
-proof
-  assume "exp (\<i> * of_real x) = 1"
-  then have "exp (\<i> * of_real x) = exp 0"
-    by simp
-  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
-    by (simp only: Ints_def exp_eq) auto
-  then have "of_real x = (of_int (2 * n) * pi)"
-    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
-  then have "x = (of_int (2 * n) * pi)"
-    by simp
-  then show False using assms
-    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
-qed
+  by (smt (verit) Im_i_times Re_complex_of_real assms exp_complex_eqI exp_zero zero_complex.sel(2))
 
 lemma sin_eq_0:
   fixes z::complex
@@ -458,16 +399,7 @@
 lemma cos_eq_1:
   fixes z::complex
   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = complex_of_real(2 * n * pi))"
-proof -
-  have "cos z = cos (2*(z/2))"
-    by simp
-  also have "\<dots> = 1 - 2 * sin (z/2) ^ 2"
-    by (simp only: cos_double_sin)
-  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
-    by simp
-  show ?thesis
-    by (auto simp: sin_eq_0)
-qed
+  by (metis Re_complex_of_real cos_of_real cos_one_2pi_int cos_one_sin_zero mult.commute of_real_1 sin_eq_0)
 
 lemma csin_eq_1:
   fixes z::complex
@@ -482,10 +414,8 @@
 proof -
   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
     by (simp add: equation_minus_iff)
-  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
-    by (simp only: csin_eq_1)
   also have "\<dots> \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
-    by (rule iff_exI) (metis add.inverse_inverse add_uminus_conv_diff minus_add_distrib)
+    by (metis (mono_tags, lifting) add_uminus_conv_diff csin_eq_1 equation_minus_iff minus_add_distrib)
   also have "\<dots> = ?rhs"
     apply safe
     apply (rule_tac [2] x="-(x+1)" in exI)
@@ -506,10 +436,8 @@
 proof -
   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
-  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
-    by (simp only: csin_eq_1)
   also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
-    by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
+    by (metis csin_eq_1 Re_complex_of_real id_apply of_real_add of_real_divide of_real_eq_id of_real_numeral)
   also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
@@ -519,10 +447,8 @@
 proof -
   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
-  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
-    by (simp add: csin_eq_minus1)
   also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
-    by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
+    by (metis Re_complex_of_real csin_eq_minus1 id_apply of_real_add of_real_eq_id)
   also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
@@ -533,10 +459,8 @@
 proof -
   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
-  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
-    by (simp add: ccos_eq_minus1)
   also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
-    by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
+    by (metis ccos_eq_minus1 id_apply of_real_add of_real_eq_id of_real_eq_iff)
   also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
@@ -568,12 +492,8 @@
         (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then have "sin w - sin z = 0"
-    by (auto simp: algebra_simps)
-  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
-    by (auto simp: sin_diff_sin)
   then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
-    using mult_eq_0_iff by blast
+    by (metis divide_eq_0_iff nonzero_eq_divide_eq right_minus_eq sin_diff_sin zero_neq_numeral)
   then show ?rhs
   proof cases
     case 1
@@ -608,14 +528,10 @@
   fixes w :: complex
   shows "cos w = cos z \<longleftrightarrow> (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
         (is "?lhs = ?rhs")
-proof
+proof 
   assume ?lhs
-  then have "cos w - cos z = 0"
-    by (auto simp: algebra_simps)
-  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
-    by (auto simp: cos_diff_cos)
   then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
-    using mult_eq_0_iff by blast
+    by (metis mult_eq_0_iff cos_diff_cos right_minus_eq zero_neq_numeral)
   then show ?rhs
   proof cases
     case 1
@@ -719,22 +635,7 @@
 lemma norm_cos_plus1_le:
   fixes z::complex
   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
-proof -
-  have mono: "\<And>u w z::real. (1 \<le> w | 1 \<le> z) \<Longrightarrow> (w \<le> u & z \<le> u) \<Longrightarrow> 2 + w + z \<le> 4 * u"
-      by arith
-  have *: "Im z \<le> cmod z"
-    using abs_Im_le_cmod abs_le_D1 by auto
-  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
-    by (simp add: norm_add_rule_thm)
-  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
-    by (simp add: cos_exp_eq)
-  also have "\<dots> = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
-    by (simp add: field_simps)
-  also have "\<dots> = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
-    by (simp add: norm_divide)
-  finally show ?thesis
-    by (metis exp_eq_one_iff exp_le_cancel_iff mult_2 norm_cos_le norm_ge_zero norm_one norm_triangle_mono)
-qed
+  by (smt (verit, best) exp_ge_add_one_self norm_cos_le norm_ge_zero norm_one norm_triangle_ineq)
 
 lemma sinh_conv_sin: "sinh z = -\<i> * sin (\<i>*z)"
   by (simp add: sinh_field_def sin_i_times exp_minus)
@@ -793,6 +694,7 @@
     by simp
 qed auto
 
+text \<open>For complex @{term z}, a tighter bound than in the previous result\<close>
 lemma Taylor_exp:
   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
 proof (rule complex_Taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
@@ -857,14 +759,12 @@
            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   proof (rule complex_Taylor [of "closed_segment 0 z" n
                                  "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
-                                 "exp\<bar>Im z\<bar>" 0 z,  simplified])
+                                 "exp\<bar>Im z\<bar>" 0 z, simplified])
     fix k x
     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
             (at x within closed_segment 0 z)"
-      apply (auto simp: power_Suc)
-      apply (intro derivative_eq_intros | simp)+
-      done
+      by (cases "even k") (intro derivative_eq_intros | simp add: power_Suc)+
   next
     fix x
     assume "x \<in> closed_segment 0 z"
@@ -887,16 +787,15 @@
   have *: "cmod (cos z -
                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
-  proof (rule complex_Taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
-simplified])
+  proof (rule complex_Taylor [of "closed_segment 0 z" n 
+                                 "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" 
+                                 "exp\<bar>Im z\<bar>" 0 z, simplified])
     fix k x
     assume "x \<in> closed_segment 0 z" "k \<le> n"
     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
             (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
              (at x within closed_segment 0 z)"
-      apply (auto simp: power_Suc)
-      apply (intro derivative_eq_intros | simp)+
-      done
+      by (cases "even k") (intro derivative_eq_intros | simp add: power_Suc)+
   next
     fix x
     assume "x \<in> closed_segment 0 z"
@@ -942,18 +841,10 @@
   by (simp add: algebra_simps is_Arg_def)
 
 lemma is_Arg_eqI:
-  assumes r: "is_Arg z r" and s: "is_Arg z s" and rs: "abs (r-s) < 2*pi" and "z \<noteq> 0"
+  assumes "is_Arg z r" and "is_Arg z s" and "abs (r-s) < 2*pi" and "z \<noteq> 0"
   shows "r = s"
-proof -
-  have zr: "z = (cmod z) * exp (\<i> * r)" and zs: "z = (cmod z) * exp (\<i> * s)"
-    using r s by (auto simp: is_Arg_def)
-  with \<open>z \<noteq> 0\<close> have eq: "exp (\<i> * r) = exp (\<i> * s)"
-    by (metis mult_eq_0_iff mult_left_cancel)
-  have  "\<i> * r = \<i> * s"
-    by (rule exp_complex_eqI) (use rs in \<open>auto simp: eq exp_complex_eqI\<close>)
-  then show ?thesis
-    by simp
-qed
+  using assms unfolding is_Arg_def
+  by (metis Im_i_times Re_complex_of_real exp_complex_eqI mult_cancel_left mult_eq_0_iff)
 
 text\<open>This function returns the angle of a complex number from its representation in polar coordinates.
 Due to periodicity, its range is arbitrary. \<^term>\<open>Arg2pi\<close> follows HOL Light in adopting the interval \<open>[0,2\<pi>)\<close>.
@@ -965,28 +856,13 @@
   by (simp add: Arg2pi_def)
 
 lemma Arg2pi_unique_lemma:
-  assumes z:  "is_Arg z t"
-      and z': "is_Arg z t'"
-      and t:  "0 \<le> t"  "t < 2*pi"
-      and t': "0 \<le> t'" "t' < 2*pi"
-      and nz: "z \<noteq> 0"
+  assumes "is_Arg z t"
+      and "is_Arg z t'"
+      and "0 \<le> t"  "t < 2*pi"
+      and "0 \<le> t'" "t' < 2*pi"
+      and "z \<noteq> 0"
   shows "t' = t"
-proof -
-  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
-    by arith
-  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
-    by (metis z z' is_Arg_def)
-  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
-    by (metis nz mult_left_cancel mult_zero_left z is_Arg_def)
-  then have "sin t' = sin t \<and> cos t' = cos t"
-    by (metis cis.simps cis_conv_exp)
-  then obtain n::int where n: "t' = t + 2 * n * pi"
-    by (auto simp: sin_cos_eq_iff)
-  then have "n=0"
-    by (cases n) (use t t' in \<open>auto simp: mult_less_0_iff algebra_simps\<close>)
-  then show "t' = t"
-    by (simp add: n)
-qed
+  using is_Arg_eqI assms by force
 
 lemma Arg2pi: "0 \<le> Arg2pi z \<and> Arg2pi z < 2*pi \<and> is_Arg z (Arg2pi z)"
 proof (cases "z=0")
@@ -998,7 +874,7 @@
              and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
     using sincos_total_2pi [OF complex_unit_circle [OF False]]
     by blast
-  have z: "is_Arg z t"
+  then have z: "is_Arg z t"
     unfolding is_Arg_def
     using t False ReIm
     by (intro complex_eqI) (auto simp: exp_Euler sin_of_real cos_of_real field_split_simps)
@@ -1056,36 +932,20 @@
 qed auto
 
 lemma Arg2pi_lt_pi: "0 < Arg2pi z \<and> Arg2pi z < pi \<longleftrightarrow> 0 < Im z"
-proof (cases "z=0")
-  case False
-  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
-    by (metis Arg2pi_eq)
-  also have "\<dots> = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
-    using False by (simp add: zero_less_mult_iff)
-  also have "\<dots> \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi" (is "_ = ?rhs")
-  proof -
-    have "0 < sin (Arg2pi z) \<Longrightarrow> ?rhs"
-      by (meson Arg2pi_ge_0 Arg2pi_lt_2pi less_le_trans not_le sin_le_zero sin_x_le_x)
-    then show ?thesis
-      by (auto simp: Im_exp sin_gt_zero)
-  qed
-  finally show ?thesis
-    by blast
-qed auto
+  using Arg2pi_le_pi [of z]
+  by (smt (verit, del_insts) Arg2pi_0 Arg2pi_le_pi Arg2pi_minus uminus_complex.simps(2) zero_complex.simps(2))
 
 lemma Arg2pi_eq_0: "Arg2pi z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
 proof (cases "z=0")
   case False
-  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
-    by (metis Arg2pi_eq)
-  also have "\<dots> \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
-    using False  by (simp add: zero_le_mult_iff)
+  then have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
+    by (metis cis.sel(1) cis_conv_exp cos_Arg2pi norm_ge_zero norm_le_zero_iff zero_le_mult_iff)
   also have "\<dots> \<longleftrightarrow> Arg2pi z = 0"
   proof -
     have [simp]: "Arg2pi z = 0 \<Longrightarrow> z \<in> \<real>"
       using Arg2pi_eq [of z] by (auto simp: Reals_def)
     moreover have "\<lbrakk>z \<in> \<real>; 0 \<le> cos (Arg2pi z)\<rbrakk> \<Longrightarrow> Arg2pi z = 0"
-      by (metis Arg2pi_lt_pi Arg2pi_ge_0 Arg2pi_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
+      by (smt (verit, ccfv_SIG) Arg2pi_ge_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff cos_pi)
     ultimately show ?thesis
       by (auto simp: Re_exp)
   qed
@@ -1123,7 +983,7 @@
 
 lemma Arg2pi_eq_iff:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-  shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" (is "?lhs = ?rhs")
+  shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   then have "(cmod w) * (z / cmod z) = w"
@@ -1169,8 +1029,7 @@
   assumes "w \<noteq> 0" "z \<noteq> 0"
     shows "Arg2pi (w * z) = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi w + Arg2pi z
                             else (Arg2pi w + Arg2pi z) - 2*pi)"
-  using Arg2pi_add [OF assms]
-  by auto
+  using Arg2pi_add [OF assms] by auto
 
 lemma Arg2pi_cnj_eq_inverse:
   assumes "z \<noteq> 0" shows "Arg2pi (cnj z) = Arg2pi (inverse z)"
@@ -1264,14 +1123,7 @@
 lemma Ln_of_real:
   assumes "0 < z"
     shows "ln(of_real z::complex) = of_real(ln z)"
-proof -
-  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
-    by (simp add: exp_of_real)
-  also have "\<dots> = of_real(ln z)"
-    using assms by (subst Ln_exp) auto
-  finally show ?thesis
-    using assms by simp
-qed
+  by (smt (verit) Im_complex_of_real Ln_exp assms exp_ln of_real_exp pi_ge_two)
 
 corollary\<^marker>\<open>tag unimportant\<close> Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
   by (auto simp: Ln_of_real elim: Reals_cases)
@@ -1286,16 +1138,10 @@
   using Ln_of_real by force
 
 lemma Ln_1 [simp]: "ln 1 = (0::complex)"
-proof -
-  have "ln (exp 0) = (0::complex)"
-    by (simp add: del: exp_zero)
-  then show ?thesis
-    by simp
-qed
-
+  by (smt (verit, best) Ln_of_real ln_one of_real_0 of_real_1)
 
 lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
-  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
+  by (metis (mono_tags, lifting) Ln_1 exp_Ln exp_zero nonpos_Reals_zero_I)
 
 instance
   by intro_classes (rule ln_complex_def Ln_1)
@@ -1317,17 +1163,12 @@
 corollary\<^marker>\<open>tag unimportant\<close> ln_cmod_le:
   assumes z: "z \<noteq> 0"
     shows "ln (cmod z) \<le> cmod (Ln z)"
-  using norm_exp [of "Ln z", simplified exp_Ln [OF z]]
   by (metis Re_Ln complex_Re_le_cmod z)
 
 proposition\<^marker>\<open>tag unimportant\<close> exists_complex_root:
   fixes z :: complex
   assumes "n \<noteq> 0"  obtains w where "z = w ^ n"
-proof (cases "z=0")
-  case False
-  then show ?thesis
-    by (rule_tac w = "exp(Ln z / n)" in that) (simp add: assms exp_of_nat_mult [symmetric])
-qed (use assms in auto)
+  by (metis assms exp_Ln exp_of_nat_mult nonzero_mult_div_cancel_left of_nat_eq_0_iff power_0_left times_divide_eq_right)
 
 corollary\<^marker>\<open>tag unimportant\<close> exists_complex_root_nonzero:
   fixes z::complex
@@ -1337,17 +1178,23 @@
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Derivative of Ln away from the branch cut\<close>
 
-lemma
+lemma Im_Ln_less_pi: 
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"shows "Im (Ln z) < pi"
+proof -
+  have znz [simp]: "z \<noteq> 0"
+    using assms by auto
+  with Im_Ln_le_pi [of z] show ?thesis
+    by (smt (verit, best) Arg2pi_eq_0_pi Arg2pi_exp Ln_in_Reals assms complex_is_Real_iff complex_nonpos_Reals_iff exp_Ln pi_ge_two)
+qed
+
+lemma has_field_derivative_Ln: 
   assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
-  shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
-    and Im_Ln_less_pi:           "Im (Ln z) < pi"
+  shows "(Ln has_field_derivative inverse(z)) (at z)"
 proof -
   have znz [simp]: "z \<noteq> 0"
     using assms by auto
   then have "Im (Ln z) \<noteq> pi"
-    by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)
-  then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
-    by (simp add: le_neq_trans)
+    by (smt (verit, best) Arg2pi_eq_0_pi Arg2pi_exp Ln_in_Reals assms complex_is_Real_iff complex_nonpos_Reals_iff exp_Ln pi_ge_two)
   let ?U = "{w. -pi < Im(w) \<and> Im(w) < pi}"
   have 1: "open ?U"
     by (simp add: open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
@@ -1356,7 +1203,7 @@
   have 3: "continuous_on ?U (\<lambda>x. Blinfun ((*) (exp x)))"
     unfolding blinfun_mult_right.abs_eq [symmetric] by (intro continuous_intros)
   have 4: "Ln z \<in> ?U"
-    by (auto simp: mpi_less_Im_Ln *)
+    by (simp add: Im_Ln_less_pi assms mpi_less_Im_Ln)
   have 5: "Blinfun ((*) (inverse z)) o\<^sub>L Blinfun ((*) (exp (Ln z))) = id_blinfun"
     by (rule blinfun_eqI) (simp add: bounded_linear_mult_right bounded_linear_Blinfun_apply)
   obtain U' V g g' where "open U'" and sub: "U' \<subseteq> ?U"
@@ -1371,21 +1218,15 @@
     unfolding has_field_derivative_def
   proof (rule has_derivative_transform_within_open)
     show g_eq_Ln: "g y = Ln y" if "y \<in> V" for y
-    proof -
-      obtain x where "y = exp x" "x \<in> U'"
-        using hom homeomorphism_image1 that \<open>y \<in> V\<close> by blast
-      then show ?thesis
-        using sub hom homeomorphism_apply1 by fastforce
-    qed
+      by (smt (verit, ccfv_threshold) Ln_exp hom homeomorphism_def imageI mem_Collect_eq sub subset_iff that)
     have "0 \<notin> V"
       by (meson exp_not_eq_zero hom homeomorphism_def)
     then have "\<And>y. y \<in> V \<Longrightarrow> g' y = inv ((*) y)"
       by (metis exp_Ln g' g_eq_Ln)
     then have g': "g' z = (\<lambda>x. x/z)"
-      by (metis (no_types, opaque_lifting) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
+      by (metis \<open>z \<in> V\<close> bij bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
     show "(g has_derivative (*) (inverse z)) (at z)"
-      using g [OF \<open>z \<in> V\<close>] g'
-      by (simp add: \<open>z \<in> V\<close> field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative)
+      using g [OF \<open>z \<in> V\<close>] g' by (simp add: divide_inverse_commute)
   qed (auto simp: \<open>z \<in> V\<close> \<open>open V\<close>)
 qed
 
@@ -1425,29 +1266,19 @@
   by (auto simp: o_def)
 
 lemma tendsto_Ln [tendsto_intros]:
-  fixes L F
   assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
   shows   "((\<lambda>x. Ln (f x)) \<longlongrightarrow> Ln L) F"
-proof -
-  have "nhds L \<ge> filtermap f F"
-    using assms(1) by (simp add: filterlim_def)
-  moreover have "\<forall>\<^sub>F y in nhds L. y \<in> - \<real>\<^sub>\<le>\<^sub>0"
-    using eventually_nhds_in_open[of "- \<real>\<^sub>\<le>\<^sub>0" L] assms by (auto simp: open_Compl)
-  ultimately have "\<forall>\<^sub>F y in filtermap f F. y \<in> - \<real>\<^sub>\<le>\<^sub>0" by (rule filter_leD)
-  moreover have "continuous_on (-\<real>\<^sub>\<le>\<^sub>0) Ln" by (rule continuous_on_Ln) auto
-  ultimately show ?thesis using continuous_on_tendsto_compose[of "- \<real>\<^sub>\<le>\<^sub>0" Ln f L F] assms
-    by (simp add: eventually_filtermap)
-qed
+  by (simp add: assms isCont_tendsto_compose)
 
 lemma divide_ln_mono:
   fixes x y::real
   assumes "3 \<le> x" "x \<le> y"
   shows "x / ln x \<le> y / ln y"
-proof (rule exE [OF complex_mvt_line [of x y "\<lambda>z. z / Ln z" "\<lambda>z. 1/(Ln z) - 1/(Ln z)^2"]];
-    clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)
-  show "\<And>u. \<lbrakk>x \<le> u; u \<le> y\<rbrakk> \<Longrightarrow> ((\<lambda>z. z / Ln z) has_field_derivative 1 / Ln u - 1 / (Ln u)\<^sup>2) (at u)"
+proof -
+  have "\<And>u. \<lbrakk>x \<le> u; u \<le> y\<rbrakk> \<Longrightarrow> ((\<lambda>z. z / Ln z) has_field_derivative 1 / Ln u - 1 / (Ln u)\<^sup>2) (at u)"
     using \<open>3 \<le> x\<close> by (force intro!: derivative_eq_intros simp: field_simps power_eq_if)
-  show "x / ln x \<le> y / ln y"
+  moreover
+  have "x / ln x \<le> y / ln y"
     if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"
     and x: "x \<le> u" "u \<le> y" for u
   proof -
@@ -1456,6 +1287,9 @@
     show ?thesis
       using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
   qed
+  ultimately show ?thesis
+    using complex_mvt_line [of x y "\<lambda>z. z / Ln z" "\<lambda>z. 1/(Ln z) - 1/(Ln z)^2"] assms
+    by (force simp add: closed_segment_Reals closed_segment_eq_real_ivl)
 qed
 
 theorem Ln_series:
@@ -1505,7 +1339,8 @@
   by (drule Ln_series) (simp add: power_minus')
 
 lemma ln_series':
-  assumes "abs (x::real) < 1"
+  fixes x::real
+  assumes "\<bar>x\<bar> < 1"
   shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
 proof -
   from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
@@ -1513,7 +1348,7 @@
   also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
     by (rule ext) simp
   also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
-    by (subst Ln_of_real [symmetric]) simp_all
+    by (smt (verit) Ln_of_real of_real_1 of_real_add)
   finally show ?thesis by (subst (asm) sums_of_real_iff)
 qed
 
@@ -1604,35 +1439,9 @@
   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
   by simp
 
-lemma Re_Ln_pos_lt:
-  assumes "z \<noteq> 0"
-    shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
-proof -
-  { fix w
-    assume "w = Ln z"
-    then have w: "Im w \<le> pi" "- pi < Im w"
-      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
-      by auto
-    have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
-    proof
-      assume "\<bar>Im w\<bar> < pi/2" then show "0 < Re(exp w)"
-        by (auto simp: Re_exp cos_gt_zero_pi split: if_split_asm)
-    next
-      assume R: "0 < Re(exp w)" then
-      have "\<bar>Im w\<bar> \<noteq> pi/2"
-        by (metis cos_minus cos_pi_half mult_eq_0_iff Re_exp abs_if order_less_irrefl)
-      then show "\<bar>Im w\<bar> < pi/2"
-        using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"] w R
-        by (force simp: Re_exp zero_less_mult_iff abs_if not_less_iff_gr_or_eq)
-    qed
-  }
-  then show ?thesis using assms
-    by auto
-qed
-
 lemma Re_Ln_pos_le:
   assumes "z \<noteq> 0"
-    shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
+  shows "\<bar>Im(Ln z)\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
 proof -
   { fix w
     assume "w = Ln z"
@@ -1647,23 +1456,11 @@
     by auto
 qed
 
-lemma Im_Ln_pos_lt:
+lemma Re_Ln_pos_lt:
   assumes "z \<noteq> 0"
-    shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
-proof -
-  { fix w
-    assume "w = Ln z"
-    then have w: "Im w \<le> pi" "- pi < Im w"
-      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
-      by auto
-    then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
-      using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"] less_linear
-      by (fastforce simp add: Im_exp zero_less_mult_iff)
-  }
-  then show ?thesis using assms
-    by auto
-qed
-
+  shows "\<bar>Im(Ln z)\<bar> < pi/2 \<longleftrightarrow> 0 < Re(z)"
+  using Re_Ln_pos_le assms
+  by (smt (verit) Re_exp arccos_cos cos_minus cos_pi_half exp_Ln exp_gt_zero field_sum_of_halves mult_eq_0_iff)
 
 lemma Im_Ln_pos_le:
   assumes "z \<noteq> 0"
@@ -1681,6 +1478,12 @@
     by auto
 qed
 
+lemma Im_Ln_pos_lt:
+  assumes "z \<noteq> 0"
+  shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
+  using Im_Ln_pos_le [OF assms] assms
+  by (smt (verit, best) Arg2pi_exp Arg2pi_lt_pi exp_Ln)
+
 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> \<bar>Im(Ln z)\<bar> < pi/2"
   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
 
@@ -1701,23 +1504,7 @@
 proof (cases "z=0")
   case False
   show ?thesis
-  proof (rule exp_complex_eqI)
-    have "\<bar>Im (cnj (Ln z)) - Im (Ln (cnj z))\<bar> \<le> \<bar>Im (cnj (Ln z))\<bar> + \<bar>Im (Ln (cnj z))\<bar>"
-      by (rule abs_triangle_ineq4)
-    also have "\<dots> < pi + pi"
-    proof -
-      have "\<bar>Im (cnj (Ln z))\<bar> < pi"
-        by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
-      moreover have "\<bar>Im (Ln (cnj z))\<bar> \<le> pi"
-        by (meson abs_le_iff complex_cnj_zero_iff less_eq_real_def minus_less_iff  False Im_Ln_le_pi mpi_less_Im_Ln)
-      ultimately show ?thesis
-        by simp
-    qed
-    finally show "\<bar>Im (cnj (Ln z)) - Im (Ln (cnj z))\<bar> < 2 * pi"
-      by simp
-    show "exp (cnj (Ln z)) = exp (Ln (cnj z))"
-      by (metis False complex_cnj_zero_iff exp_Ln exp_cnj)
-  qed
+    by (smt (verit) False Im_Ln_less_pi Ln_exp assms cnj.sel(2) exp_Ln exp_cnj mpi_less_Im_Ln)
 qed (use assms in auto)
 
 
@@ -1725,23 +1512,7 @@
 proof (cases "z=0")
   case False
   show ?thesis
-  proof (rule exp_complex_eqI)
-    have "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>"
-      by (rule abs_triangle_ineq4)
-    also have "\<dots> < pi + pi"
-    proof -
-      have "\<bar>Im (Ln (inverse z))\<bar> < pi"
-        by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
-      moreover have "\<bar>Im (- Ln z)\<bar> \<le> pi"
-        using False Im_Ln_le_pi mpi_less_Im_Ln by fastforce
-      ultimately show ?thesis
-        by simp
-    qed
-    finally show "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> < 2 * pi"
-      by simp
-    show "exp (Ln (inverse z)) = exp (- Ln z)"
-      by (simp add: False exp_minus)
-  qed
+    by (smt (verit) False Im_Ln_less_pi Ln_exp assms exp_Ln exp_minus mpi_less_Im_Ln uminus_complex.sel(2))
 qed (use assms in auto)
 
 lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
@@ -1756,12 +1527,7 @@
   by simp
 
 lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
-proof -
-  have  "Ln(-\<i>) = Ln(inverse \<i>)"    by simp
-  also have "\<dots> = - (Ln \<i>)"         using Ln_inverse by blast
-  also have "\<dots> = - (\<i> * pi/2)"     by simp
-  finally show ?thesis .
-qed
+  using Ln_inverse by fastforce
 
 lemma Ln_times:
   assumes "w \<noteq> 0" "z \<noteq> 0"
@@ -1792,10 +1558,9 @@
   using Ln_Reals_eq Ln_times_of_real by fastforce
 
 corollary\<^marker>\<open>tag unimportant\<close> Ln_divide_of_real:
-    "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
-using Ln_times_of_real [of "inverse r" z]
-by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
-         del: of_real_inverse)
+  "\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
+  using Ln_times_of_real [of "inverse r" z]
+  by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse flip: of_real_inverse)
 
 corollary\<^marker>\<open>tag unimportant\<close> Ln_prod:
   fixes f :: "'a \<Rightarrow> complex"
@@ -1818,10 +1583,10 @@
   assumes "z \<noteq> 0"
     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> \<not>(Re(z) < 0 \<and> Im(z) = 0)
                      then Ln(z) + \<i> * pi
-                     else Ln(z) - \<i> * pi)" (is "_ = ?rhs")
+                     else Ln(z) - \<i> * pi)" 
   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
-    by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)
+  by (intro Ln_unique) (auto simp: exp_add exp_diff)
 
 lemma Ln_inverse_if:
   assumes "z \<noteq> 0"
@@ -1854,7 +1619,7 @@
   by (simp add: Ln_times) auto
 
 lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
-  by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
+  by (metis Ln_of_real of_nat_0_less_iff of_real_of_nat_eq)
 
 lemma Ln_of_nat_over_of_nat:
   assumes "m > 0" "n > 0"
@@ -1913,13 +1678,11 @@
     have "f n x + 1 \<notin> \<real>\<^sub>\<le>\<^sub>0" if "x \<in> A" for n x
     proof
       assume "f n x + 1 \<in> \<real>\<^sub>\<le>\<^sub>0"
-      then obtain t where t: "t \<le> 0" "f n x + 1 = of_real t"
-        by (auto elim!: nonpos_Reals_cases)
-      hence "f n x = of_real (t - 1)"
-        by (simp add: algebra_simps)
-      also have "norm \<dots> \<ge> 1"
+      then obtain t where t: "t \<le> 0" "f n x = of_real (t - 1)"
+        by (metis add_diff_cancel nonpos_Reals_cases of_real_1 of_real_diff)
+      moreover have "norm \<dots> \<ge> 1"
         using t by (subst norm_of_real) auto
-      finally show False
+      ultimately show False
         using norm_f[of x n] that by auto
     qed
     thus "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>x. \<Sum>n<n. Ln (1 + f n x))"
@@ -1961,19 +1724,14 @@
     have "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. exp (ln (1 + f n x)))"
       by (simp add: exp_sum)
     also have "\<dots> = (\<Prod>n<N. 1 + f n x)"
-    proof (rule prod.cong)
-      fix n assume "n \<in> {..<N}"
-      have "f n x \<noteq> -1"
-        using norm_f[of x n] x by auto
-      thus "exp (ln (1 + f n x)) = 1 + f n x"
-        by (simp add: add_eq_0_iff)
-    qed auto
+      using norm_f[of x] x
+      by (smt (verit, best) add.right_neutral add_diff_cancel exp_Ln norm_minus_commute norm_one prod.cong)
     finally show "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. 1 + f n x)" .
   qed
   finally show ?thesis .
 qed
 
-(* Theorem 17.6 by Bak & Newman, roughly *)
+text \<open>Theorem 17.6 by Bak and Newman, Complex Analysis [roughly]\<close>
 lemma uniformly_convergent_on_prod:
   fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
   assumes cont: "\<And>n. continuous_on A (f n)"
@@ -2146,15 +1904,13 @@
 lemma Arg_of_real [simp]: "Arg (of_real r) = (if r<0 then pi else 0)"
   by (simp add: Im_Ln_eq_pi Arg_def)
 
-lemma mpi_less_Arg: "-pi < Arg z"
-    and Arg_le_pi: "Arg z \<le> pi"
+lemma mpi_less_Arg: "-pi < Arg z" and Arg_le_pi: "Arg z \<le> pi"
   by (auto simp: Arg_def mpi_less_Im_Ln Im_Ln_le_pi)
 
-lemma
+lemma Arg_eq: 
   assumes "z \<noteq> 0"
-  shows Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
-  using assms exp_Ln exp_eq_polar
-  by (auto simp:  Arg_def)
+  shows "z = of_real(norm z) * exp(\<i> * Arg z)"
+  using cis_conv_exp rcis_cmod_Arg rcis_def by force
 
 lemma is_Arg_Arg: "z \<noteq> 0 \<Longrightarrow> is_Arg z (Arg z)"
   by (simp add: Arg_eq is_Arg_def)
@@ -2196,35 +1952,15 @@
   by (auto simp: is_Arg_def norm_divide field_simps exp_diff Arg_of_real)
 
 lemma Arg_unique_lemma:
-  assumes z:  "is_Arg z t"
-      and z': "is_Arg z t'"
-      and t:  "- pi < t"  "t \<le> pi"
-      and t': "- pi < t'" "t' \<le> pi"
-      and nz: "z \<noteq> 0"
+  assumes "is_Arg z t" "is_Arg z t'"
+      and "- pi < t"  "t \<le> pi"
+      and "- pi < t'" "t' \<le> pi"
+      and "z \<noteq> 0"
     shows "t' = t"
-  using Arg2pi_unique_lemma [of "- (inverse z)"]
-proof -
-  have "pi - t' = pi - t"
-  proof (rule Arg2pi_unique_lemma [of "- (inverse z)"])
-    have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t)))"
-      by (metis is_Arg_def z)
-    also have "\<dots> = (cmod (- inverse z)) * exp (\<i> * (pi - t))"
-      by (auto simp: field_simps exp_diff norm_divide)
-    finally show "is_Arg (- inverse z) (pi - t)"
-      unfolding is_Arg_def .
-    have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t')))"
-      by (metis is_Arg_def z')
-    also have "\<dots> = (cmod (- inverse z)) * exp (\<i> * (pi - t'))"
-      by (auto simp: field_simps exp_diff norm_divide)
-    finally show "is_Arg (- inverse z) (pi - t')"
-      unfolding is_Arg_def .
-  qed (use assms in auto)
-  then show ?thesis
-    by simp
-qed
+  using is_Arg_eqI assms by force
 
 lemma complex_norm_eq_1_exp_eq: "norm z = 1 \<longleftrightarrow> exp(\<i> * (Arg z)) = z"
-  by (metis Arg_eq exp_not_eq_zero exp_zero mult.left_neutral norm_zero of_real_1 norm_exp_i_times)
+  by (metis Arg2pi_eq Arg_eq complex_norm_eq_1_exp norm_eq_zero norm_exp_i_times)
 
 lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * a) = z; 0 < r; -pi < a; a \<le> pi\<rbrakk> \<Longrightarrow> Arg z = a"
   by (rule Arg_unique_lemma [unfolded is_Arg_def, OF _ Arg_eq])
@@ -2239,9 +1975,8 @@
   have [simp]: "cmod z * sin (Arg z) = Im z"
     using assms Arg_eq [of z] by (metis Im_exp exp_Ln norm_exp_eq_Re Arg_def)
   show ?thesis
-    apply (rule Arg_unique [of "norm z", OF complex_eqI])
     using mpi_less_Arg [of z] Arg_le_pi [of z] assms
-    by (auto simp: Re_exp Im_exp)
+    by (intro Arg_unique [of "norm z", OF complex_eqI]) (auto simp: Re_exp Im_exp)
 qed
 
 lemma Arg_1 [simp]: "Arg 1 = 0"
@@ -2292,14 +2027,10 @@
 
 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> then Arg z else - Arg z)"
 proof (cases "z \<in> \<real>")
-  case True
-  then show ?thesis
-    by (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
-next
   case False
   then show ?thesis
     by (simp add: Arg_def Ln_inverse complex_is_Real_iff complex_nonpos_Reals_iff)
-qed
+qed (use Arg_real Re_inverse in auto)
 
 lemma Arg_eq_iff:
   assumes "w \<noteq> 0" "z \<noteq> 0"
@@ -2437,28 +2168,7 @@
 lemma Im_Ln_eq_pi_half:
     "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi/2 \<longleftrightarrow> 0 < Im(z) \<and> Re(z) = 0)"
     "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = -pi/2 \<longleftrightarrow> Im(z) < 0 \<and> Re(z) = 0)"
-proof -
-  show "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi/2 \<longleftrightarrow> 0 < Im(z) \<and> Re(z) = 0)"
-    by (metis Im_Ln_eq_pi Im_Ln_le_pi Im_Ln_pos_lt Re_Ln_pos_le Re_Ln_pos_lt
-      abs_of_nonneg less_eq_real_def order_less_irrefl pi_half_gt_zero)
-next
-  assume "z\<noteq>0"
-  have "Im (Ln z) = - pi / 2 \<Longrightarrow> Im z < 0 \<and> Re z = 0"
-    by (metis Im_Ln_pos_le Re_Ln_pos_le Re_Ln_pos_lt_imp \<open>z \<noteq> 0\<close> abs_if
-     add.inverse_inverse divide_minus_left less_eq_real_def linorder_not_le minus_pi_half_less_zero)
-  moreover have "Im (Ln z) = - pi / 2" when "Im z < 0" "Re z = 0"
-  proof -
-    obtain r::real where "r>0" "z=r * (-\<i>)"
-      by (smt (verit) \<open>Im z < 0\<close> \<open>Re z = 0\<close> add_0 complex_eq mult.commute mult_minus_right of_real_0 of_real_minus)
-    then have "Im (Ln z) = Im (Ln (r*(-\<i>)))" by auto
-    also have "... = Im (Ln (complex_of_real r) + Ln (- \<i>))"
-      by (metis Ln_times_of_real \<open>0 < r\<close> add.inverse_inverse add.inverse_neutral complex_i_not_zero)
-    also have "... = - pi/2"
-      using \<open>r>0\<close> by simp
-    finally show "Im (Ln z) = - pi / 2" .
-  qed
-  ultimately show "(Im(Ln z) = -pi/2 \<longleftrightarrow> Im(z) < 0 \<and> Re(z) = 0)" by auto
-qed
+  using Im_Ln_pos_lt Im_Ln_pos_le Re_Ln_pos_le Re_Ln_pos_lt pi_ge_two by fastforce+
 
 lemma Im_Ln_eq:
   assumes "z\<noteq>0"
@@ -2472,32 +2182,8 @@
                       else
                         if Im z>0 then pi/2 else -pi/2)"
 proof -
-  have eq_arctan_pos:"Im (Ln z) = arctan (Im z/Re z)" when "Re z>0" for z
-  proof -
-    define wR where "wR \<equiv> Re (Ln z)"
-    define \<theta> where "\<theta> \<equiv> arctan (Im z/Re z)"
-    have "z\<noteq>0" using that by auto
-    have "exp (Complex wR \<theta>) = z"
-    proof (rule complex_eqI)
-      have "Im (exp (Complex wR \<theta>)) =exp wR * sin \<theta> "
-        unfolding Im_exp by simp
-      also have "... = Im z"
-        unfolding wR_def Re_Ln[OF \<open>z\<noteq>0\<close>] \<theta>_def using \<open>z\<noteq>0\<close> \<open>Re z>0\<close>
-        by (auto simp add:sin_arctan divide_simps complex_neq_0 cmod_def real_sqrt_divide)
-      finally show "Im (exp (Complex wR \<theta>)) = Im z" .
-    next
-      have "Re (exp (Complex wR \<theta>)) = exp wR * cos \<theta> "
-        unfolding Re_exp by simp
-      also have "... = Re z"
-        by (metis Arg_eq_Im_Ln Re_exp \<open>z \<noteq> 0\<close> \<theta>_def arg_conv_arctan exp_Ln that wR_def)
-      finally show "Re (exp (Complex wR \<theta>)) = Re z" .
-    qed
-    moreover have "-pi<\<theta>" "\<theta>\<le>pi"
-      using arctan_lbound [of \<open>Im z / Re z\<close>] arctan_ubound [of \<open>Im z / Re z\<close>]
-      by (simp_all add: \<theta>_def)
-    ultimately have "Ln z = Complex wR \<theta>" using Ln_unique by auto
-    then show ?thesis using that unfolding \<theta>_def by auto
-  qed
+  have eq_arctan_pos: "Im (Ln z) = arctan (Im z/Re z)" when "Re z>0" for z
+    by (metis Arg_eq_Im_Ln arg_conv_arctan order_less_irrefl that zero_complex.simps(1))
   have ?thesis when "Re z=0"
     using Im_Ln_eq_pi_half[OF \<open>z\<noteq>0\<close>] that
     using assms complex_eq_iff by auto
@@ -2532,12 +2218,12 @@
   assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
     shows "continuous (at z) Arg2pi"
 proof -
-  have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
+  have "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
     by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
-  consider "Re z < 0" | "Im z \<noteq> 0" using assms
+  moreover consider "Re z < 0" | "Im z \<noteq> 0" using assms
     using complex_nonneg_Reals_iff not_le by blast
-  then have "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
-    using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)
+  ultimately have "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+    by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)
   then show ?thesis
     unfolding continuous_at
     by (metis (mono_tags, lifting) Arg2pi_Ln Arg2pi_gt_0 Compl_iff Lim_transform_within_open assms 
@@ -2658,7 +2344,7 @@
 
 lemma powr_complexpow [simp]:
   fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
-  by (induct n) (auto simp: ac_simps powr_add)
+  by (simp add: powr_nat')
 
 lemma powr_complexnumeral [simp]:
   fixes x::complex shows "x powr (numeral n) = x ^ (numeral n)"
@@ -2715,18 +2401,19 @@
 
 lemma
   fixes w::complex
-  shows Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>"
-  and nonneg_Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>\<^sub>\<ge>\<^sub>0"
-  by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
+  assumes "w \<in> \<real>\<^sub>\<ge>\<^sub>0" "z \<in> \<real>"
+  shows Reals_powr [simp]: "w powr z \<in> \<real>" and nonneg_Reals_powr [simp]: "w powr z \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  using assms by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
 
 lemma powr_neg_real_complex:
-  "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
+  fixes w::complex
+  shows "(- of_real x) powr w = (-1) powr (of_real (sgn x) * w) * of_real x powr w"
 proof (cases "x = 0")
   assume x: "x \<noteq> 0"
-  hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
+  hence "(-x) powr w = exp (w * ln (-of_real x))" by (simp add: powr_def)
   also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
     by (simp add: Ln_minus Ln_of_real)
-  also from x have "exp (a * \<dots>) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
+  also from x have "exp (w * \<dots>) = cis pi powr (of_real (sgn x) * w) * of_real x powr w"
     by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
   also note cis_pi
   finally show ?thesis by simp
@@ -2818,28 +2505,14 @@
 
 lemma field_differentiable_powr_of_int:
   fixes z :: complex
-  assumes gderiv: "g field_differentiable (at z within S)" and "g z \<noteq> 0"
+  assumes "g field_differentiable (at z within S)" and "g z \<noteq> 0"
   shows "(\<lambda>z. g z powr of_int n) field_differentiable (at z within S)"
-using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast
+  using has_field_derivative_powr_of_int assms field_differentiable_def by blast
 
 lemma holomorphic_on_powr_of_int [holomorphic_intros]:
-  assumes holf: "f holomorphic_on S" and 0: "\<And>z. z\<in>S \<Longrightarrow> f z \<noteq> 0"
+  assumes "f holomorphic_on S" and "\<And>z. z\<in>S \<Longrightarrow> f z \<noteq> 0"
   shows "(\<lambda>z. (f z) powr of_int n) holomorphic_on S"
-proof (cases "n\<ge>0")
-  case True
-  then have "?thesis \<longleftrightarrow> (\<lambda>z. (f z) ^ nat n) holomorphic_on S"
-    by (metis (no_types, lifting) 0 holomorphic_cong powr_of_int)
-  moreover have "(\<lambda>z. (f z) ^ nat n) holomorphic_on S"
-    using holf by (auto intro: holomorphic_intros)
-  ultimately show ?thesis by auto
-next
-  case False
-  then have "?thesis \<longleftrightarrow> (\<lambda>z. inverse (f z) ^ nat (-n)) holomorphic_on S"
-    by (metis (no_types, lifting) "0" holomorphic_cong power_inverse powr_of_int)
-  moreover have "(\<lambda>z. inverse (f z) ^ nat (-n)) holomorphic_on S"
-    using assms by (auto intro!:holomorphic_intros)
-  ultimately show ?thesis by auto
-qed
+  using assms field_differentiable_powr_of_int holomorphic_on_def by auto
 
 lemma has_field_derivative_powr_right [derivative_intros]:
     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
@@ -2896,7 +2569,7 @@
   define h where
     "h = (\<lambda>z. if f z = 0 then 0 else exp (Re (g z) * ln (cmod (f z)) + abs (Im (g z)) * pi))"
   {
-    fix z :: 'a assume z: "f z \<noteq> 0"
+    fix z :: 'a assume z: "f z \<noteq> 0" 
     define c where "c = abs (Im (g z)) * pi"
     from mpi_less_Im_Ln[OF z] Im_Ln_le_pi[OF z]
       have "abs (Im (Ln (f z))) \<le> pi" by simp
@@ -2905,7 +2578,8 @@
     hence "-Im (g z) * Im (ln (f z)) \<le> c" by simp
     hence "norm (f z powr g z) \<le> h z" by (simp add: powr_def field_simps h_def c_def)
   }
-  hence le: "norm (f z powr g z) \<le> h z" for z by (cases "f x = 0") (simp_all add: h_def)
+  hence le: "norm (f z powr g z) \<le> h z" for z
+    by (simp add: h_def) 
 
   have g': "(g \<longlongrightarrow> b) (inf F (principal {z. f z \<noteq> 0}))"
     by (rule tendsto_mono[OF _ g]) simp_all
@@ -2914,8 +2588,7 @@
   moreover {
     have "filterlim (\<lambda>x. norm (f x)) (principal {0<..}) (principal {z. f z \<noteq> 0})"
       by (auto simp: filterlim_def)
-    hence "filterlim (\<lambda>x. norm (f x)) (principal {0<..})
-             (inf F (principal {z. f z \<noteq> 0}))"
+    hence "filterlim (\<lambda>x. norm (f x)) (principal {0<..}) (inf F (principal {z. f z \<noteq> 0}))"
       by (rule filterlim_mono) simp_all
   }
   ultimately have norm: "filterlim (\<lambda>x. norm (f x)) (at_right 0) (inf F (principal {z. f z \<noteq> 0}))"
@@ -3051,7 +2724,7 @@
 lemma lim_ln_over_power:
   fixes s :: real
   assumes "0 < s"
-  shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
+  shows "(\<lambda>n. ln (real n) / real n powr s) \<longlonglongrightarrow> 0"
 proof -
   have "(\<lambda>n. ln (Suc n) / (Suc n) powr s) \<longlonglongrightarrow> 0"
     using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms




