# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1712745168 -3600
# Node ID 646cd337bb0836adff89d429c110d5c39aedd9f1
# Parent  f7b9179b5029198b6b57ad7ab009d0f9227add1f
Tiny tweaks to proofs

diff -r f7b9179b5029 -r 646cd337bb08 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Mon Apr 08 16:27:11 2024 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Wed Apr 10 11:32:48 2024 +0100
@@ -109,11 +109,15 @@
     using open_contains_ball by blast
   have [simp]: "\<And>n. cmod (1 + of_nat n) = 1 + of_nat n"
     by (metis norm_of_nat of_nat_Suc)
-  have cint: "\<And>x. \<lbrakk>x \<noteq> w; cmod (x - w) < d\<rbrakk>
-         \<Longrightarrow> (\<lambda>z. (f' z / (z - x) ^ k - f' z / (z - w) ^ k) / (x * k - w * k)) contour_integrable_on \<gamma>"
-    using int w d
-    apply (intro contour_integrable_div contour_integrable_diff has_contour_integral_integrable)
-    by (force simp: dist_norm norm_minus_commute)
+  have cint: "(\<lambda>z. (f' z / (z - x) ^ k - f' z / (z - w) ^ k) / (x * k - w * k)) contour_integrable_on \<gamma>"
+    if "x \<noteq> w" "cmod (x - w) < d" for x
+  proof -
+    have "x \<in> S - path_image \<gamma>"
+      by (metis d dist_commute dist_norm mem_ball subsetD that(2))
+    then show ?thesis
+      using contour_integrable_diff contour_integrable_div contour_integrable_on_def int w
+      by meson
+  qed
   have 1: "\<forall>\<^sub>F n in at w. (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k)
                          contour_integrable_on \<gamma>"
     unfolding eventually_at
@@ -1573,11 +1577,15 @@
   case True with assms interior_eq pole_lemma
     show ?thesis by fastforce
 next
-  case False with assms show ?thesis
-    apply (simp add: holomorphic_on_def field_differentiable_def [symmetric], clarify)
-    apply (rule field_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
+  case False 
+  then have "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at x within S"
+    if "x \<in> S" for x
+    using assms that 
+    apply (simp add: holomorphic_on_def)
     apply (rule derivative_intros | force)+
     done
+  with False show ?thesis
+    using holomorphic_on_def holomorphic_transform by presburger
 qed
 
 lemma pole_theorem_open:
@@ -1792,10 +1800,7 @@
     then have "((\<lambda>x. f z / (x - z)) has_contour_integral 0) \<gamma>"
       by (simp add: field_split_simps)
     moreover have "((\<lambda>x. (f x - f z) / (x - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
-      using z
-      apply (simp add: v_def)
-      apply (metis (no_types, lifting) contour_integrable_eq d_def has_contour_integral_eq has_contour_integral_integral cint_fxy)
-      done
+      by (metis (no_types, lifting) z cint_fxy contour_integral_eq d_def has_contour_integral_integral mem_Collect_eq v_def)
     ultimately have *: "((\<lambda>x. f z / (x - z) + (f x - f z) / (x - z)) has_contour_integral (0 + contour_integral \<gamma> (d z))) \<gamma>"
       by (rule has_contour_integral_add)
     have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
@@ -1821,10 +1826,7 @@
   qed (use \<open>0 < d0\<close> d0 in \<open>force simp: dist_norm\<close>)
   define T where "T \<equiv> {y + k |y k. y \<in> path_image \<gamma> \<and> k \<in> cball 0 (dd / 2)}"
   have "\<And>x x'. \<lbrakk>x \<in> path_image \<gamma>; dist x x' * 2 < dd\<rbrakk> \<Longrightarrow> \<exists>y k. x' = y + k \<and> y \<in> path_image \<gamma> \<and> dist 0 k * 2 \<le> dd"
-    apply (rule_tac x=x in exI)
-    apply (rule_tac x="x'-x" in exI)
-    apply (force simp: dist_norm)
-    done
+    by (metis add.commute diff_add_cancel dist_0_norm dist_commute dist_norm less_eq_real_def)
   then have subt: "path_image \<gamma> \<subseteq> interior T"
     using \<open>0 < dd\<close> 
     apply (clarsimp simp add: mem_interior T_def)
diff -r f7b9179b5029 -r 646cd337bb08 src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Mon Apr 08 16:27:11 2024 +0100
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Wed Apr 10 11:32:48 2024 +0100
@@ -716,16 +716,15 @@
       qed
     qed
     define g where [abs_def]: "g z = (if z = \<xi> then deriv h \<xi> else (h z - h \<xi>) / (z - \<xi>))" for z
-    have holg: "g holomorphic_on S"
-      unfolding g_def by (rule pole_lemma [OF holh \<xi>])
     have \<section>: "\<forall>z\<in>S - {\<xi>}. (g z - g \<xi>) / (z - \<xi>) = f z"
       using h0 by (auto simp: g_def power2_eq_square divide_simps DERIV_imp_deriv h_def)
-    show ?thesis
-      apply (intro exI conjI)
-       apply (rule pole_lemma [OF holg \<xi>])
-      apply (simp add: \<section>)
-      done
-  qed
+    have "g holomorphic_on S"
+      unfolding g_def by (rule pole_lemma [OF holh \<xi>])
+    then have "(\<lambda>z. if z = \<xi> then deriv g \<xi> else (g z - g \<xi>) / (z - \<xi>)) holomorphic_on S"
+      using \<xi> pole_lemma by blast
+    then show ?thesis
+      using "\<section>" remove_def by fastforce
+    qed
   ultimately show "?P = ?Q" and "?P = ?R"
     by meson+
 qed
@@ -916,9 +915,8 @@
     fix e::real assume "0 < e"
     with compf [of "cball 0 (inverse e)"]
     show "\<exists>B. \<forall>x. B \<le> cmod x \<longrightarrow> dist ((inverse \<circ> f) x) 0 \<le> e"
-      apply simp
-      apply (clarsimp simp add: compact_eq_bounded_closed bounded_pos norm_inverse)
-      by (metis (no_types, opaque_lifting) inverse_inverse_eq le_less_trans less_eq_real_def less_imp_inverse_less linordered_field_no_ub not_less)
+      apply (clarsimp simp: compact_eq_bounded_closed norm_divide divide_simps mult.commute elim!: bounded_normE_less)
+      by (meson linorder_not_le nle_le)
   qed
   then obtain a n where "\<And>z. f z = (\<Sum>i\<le>n. a i * z^i)"
     using assms pole_at_infinity by blast
@@ -1067,9 +1065,7 @@
       ultimately have False
         using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
         using complex_root_unity [of n 1] 
-        apply (simp add: y0 y1 power_mult_distrib)
-        apply (force simp: algebra_simps)
-        done
+        by (auto simp: y0 y1 power_mult_distrib diff_eq_eq n_ne)
       then show ?thesis ..
     qed
   qed
@@ -1300,7 +1296,7 @@
       have conth': "continuous_on (cball 0 r) h"
         by (meson \<open>r < 1\<close> dual_order.trans holh holomorphic_on_imp_continuous_on holomorphic_on_subset mem_ball_0 mem_cball_0 not_less subsetI)
       obtain w where w: "norm w = r" and lenw: "\<And>z. norm z < r \<Longrightarrow> norm(h z) \<le> norm(h w)"
-        apply (rule Schwarz1 [OF holh']) using conth' \<open>0 < r\<close> by auto
+        using conth' \<open>0 < r\<close> by (auto simp add: intro: Schwarz1 [OF holh'])
       have "h w = f w / w" using fz_eq \<open>r < 1\<close> nzr w by auto
       then have "cmod (h z) < inverse r"
         by (metis \<open>0 < r\<close> \<open>r < 1\<close> divide_strict_right_mono inverse_eq_divide
@@ -1622,8 +1618,7 @@
     using holf cnjs
     by (force simp: holomorphic_on_def)
   have 2: "(\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z))) holomorphic_on (S \<inter> {z. Im z < 0})"
-    apply (rule iffD1 [OF holomorphic_cong [OF refl]])
-    using hol_cfc by auto
+    by (smt (verit) Int_Collect comp_def hol_cfc holomorphic_cong)
   have [simp]: "(S \<inter> {z. 0 \<le> Im z}) \<union> (S \<inter> {z. Im z \<le> 0}) = S"
     by force
   have eq: "\<And>z. \<lbrakk>z \<in> S; Im z \<le> 0; 0 \<le> Im z\<rbrakk> \<Longrightarrow> f z = cnj (f (cnj z))"
@@ -1636,7 +1631,7 @@
   then have 3: "continuous_on S (\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z)))"
     by force
   show ?thesis
-    apply (rule holomorphic_on_paste_across_line [OF \<open>open S\<close>, of "- \<i>" _ 0])
+    using holomorphic_on_paste_across_line [OF \<open>open S\<close>, of "- \<i>" _ 0]
     using 1 2 3 by auto
 qed
 
@@ -1825,13 +1820,12 @@
     by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
   have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
     by (intro holomorphic_intros hol0)
-  then have \<section>: "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
+  moreover have "\<And>z. cmod z < r \<Longrightarrow>
+         cmod (deriv (\<lambda>z. f (a + z)) z) \<le> 2 * cmod (deriv (\<lambda>z. f (a + z)) 0)"
+    by (simp add: fz deriv_chain dist_norm le)
+  ultimately have \<section>: "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
                 \<subseteq> (\<lambda>z. f (a + z) - f a) ` ball 0 r"
-    apply (rule Bloch_lemma_0)
-    using \<open>0 < r\<close>
-      apply (simp_all add: \<open>0 < r\<close> )
-    apply (simp add: fz deriv_chain dist_norm le)
-    done
+    using \<open>0 < r\<close> by (intro Bloch_lemma_0) auto
   show ?thesis
   proof clarify
     fix x