# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1604791231 0
# Node ID cd93b8c9671070050214b515c8d89ee66e11e90d
# Parent  726d17b280ea0e37ac43f9e7af063d7cc5cda3ab
another big cleanup

diff -r 726d17b280ea -r cd93b8c96710 src/HOL/Complex_Analysis/Great_Picard.thy
--- a/src/HOL/Complex_Analysis/Great_Picard.thy	Thu Nov 05 19:09:11 2020 +0000
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy	Sat Nov 07 23:20:31 2020 +0000
@@ -42,14 +42,10 @@
   assumes "0 < n"
   shows "0 < n + sqrt(real n ^ 2 - 1)"
 proof -
-  have "(n-1)^2 \<le> n^2 - 1"
-    using assms by (simp add: algebra_simps power2_eq_square)
-  then have "real (n - 1) \<le> sqrt (real (n\<^sup>2 - 1))"
-    by (metis of_nat_le_iff of_nat_power real_le_rsqrt)
-  then have "n-1 \<le> sqrt(real n ^ 2 - 1)"
-    by (simp add: Suc_leI assms of_nat_diff)
+  have "0 < n * n"
+    by (simp add: assms)
   then show ?thesis
-    using assms by linarith
+    by (metis add.commute add.right_neutral add_pos_nonneg assms diff_ge_0_iff_ge nat_less_real_le of_nat_0 of_nat_0_less_iff of_nat_power power2_eq_square real_sqrt_ge_0_iff)
 qed
 
 
@@ -131,8 +127,8 @@
       have "((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> 2"
         using Schottky_lemma1 \<open>0 < n\<close>  by (simp add: field_split_simps)
       then have "ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> ln 2"
-        apply (subst ln_le_cancel_iff)
-        using Schottky_lemma1 \<open>0 < n\<close> by auto (force simp: field_split_simps)
+        using Schottky_lemma1 [of n] \<open>0 < n\<close> 
+        by (simp add: field_split_simps add_pos_nonneg)
       also have "... \<le> 3"
         using ln_add_one_self_le_self [of 1] by auto
       finally show ?thesis .
@@ -146,11 +142,11 @@
     by (auto simp: abs_if)
   then show thesis
   proof
-    assume "\<bar>x - a\<bar> < 1 / 2"
+    assume "\<bar>x - a\<bar> < 1/2"
     then show ?thesis
       by (rule_tac n=n in that) (auto simp: a_def \<open>0 < n\<close>)
   next
-    assume "\<bar>x - b\<bar> < 1 / 2"
+    assume "\<bar>x - b\<bar> < 1/2"
     then show ?thesis
       by (rule_tac n="Suc n" in that) (auto simp: b_def \<open>0 < n\<close>)
   qed
@@ -165,54 +161,65 @@
 proof -
   have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real
     by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
-  have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) -
-                 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) +
-            inverse
-             (exp (\<i> * (of_int m * complex_of_real pi) -
-                    (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2"
+  define plusi where "plusi (e::complex) \<equiv> e + inverse e" for e
+  have 1: "\<exists>k. plusi (exp (\<i> * (of_int m * complex_of_real pi) - ln (real n + sqrt ((real n)\<^sup>2 - 1)))) = of_int k * 2" 
+           (is "\<exists>k. ?\<Phi> k")
          if "n > 0" for m n
   proof -
-    have eeq: "e \<noteq> 0 \<Longrightarrow> e + inverse e = n*2 \<longleftrightarrow> inverse e^2 - 2 * n*inverse e + 1 = 0" for n e::complex
-      by (auto simp: field_simps power2_eq_square)
+    have eeq: "e \<noteq> 0 \<Longrightarrow> plusi e = n \<longleftrightarrow> (inverse e) ^ 2 = n/e - 1" for n e::complex
+      by (auto simp: plusi_def field_simps power2_eq_square)
+    have [simp]: "1 \<le> real n * real n"
+      using nat_0_less_mult_iff nat_less_real_le that by force
+    consider "odd m" | "even m"
+      by blast
+    then have "\<exists>k. ?\<Phi> k"
+    proof cases
+      case 1
+      then have "?\<Phi> (- n)"
+        using Schottky_lemma1 [OF that]
+        by (simp add: eeq) (simp add: power2_eq_square exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
+      then show ?thesis ..
+    next
+      case 2
+      then have "?\<Phi> n"
+        using Schottky_lemma1 [OF that]
+        by (simp add: eeq) (simp add: power2_eq_square exp_diff exp_Euler exp_of_real algebra_simps)
+      then show ?thesis ..
+    qed
+    then show ?thesis by blast
+  qed
+  have 2: "\<exists>k. plusi (exp (\<i> * (of_int m * complex_of_real pi) +
+                      (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2"
+           (is "\<exists>k. ?\<Phi> k")
+            if "n > 0" for m n
+  proof -
+    have eeq: "e \<noteq> 0 \<Longrightarrow> plusi e = n \<longleftrightarrow> e^2 - n*e + 1 = 0" for n e::complex
+      by (auto simp: plusi_def field_simps power2_eq_square)
     have [simp]: "1 \<le> real n * real n"
       by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that)
-    show ?thesis
-      apply (simp add: eeq)
-      using Schottky_lemma1 [OF that]
-      apply (auto simp: eeq exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
-       apply (rule_tac x="int n" in exI)
-       apply (auto simp: power2_eq_square algebra_simps)
-       apply (rule_tac x="- int n" in exI)
-      apply (auto simp: power2_eq_square algebra_simps)
-      done
-  qed
-  have 2: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) +
-                 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) +
-            inverse
-             (exp (\<i> * (of_int m * complex_of_real pi) +
-                    (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2"
-            if "n > 0" for m n
-  proof -
-    have eeq: "e \<noteq> 0 \<Longrightarrow> e + inverse e = n*2 \<longleftrightarrow> e^2 - 2 * n*e + 1 = 0" for n e::complex
-      by (auto simp: field_simps power2_eq_square)
-    have [simp]: "1 \<le> real n * real n"
-      by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that)
-    show ?thesis
-      apply (simp add: eeq)
-      using Schottky_lemma1 [OF that]
-      apply (auto simp: exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
-       apply (rule_tac x="int n" in exI)
-       apply (auto simp: power2_eq_square algebra_simps)
-       apply (rule_tac x="- int n" in exI)
-      apply (auto simp: power2_eq_square algebra_simps)
-      done
+    consider "odd m" | "even m"
+      by blast
+    then have "\<exists>k. ?\<Phi> k"
+    proof cases
+      case 1
+      then have "?\<Phi> (- n)"
+        using Schottky_lemma1 [OF that]
+        by (simp add: eeq) (simp add: power2_eq_square exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
+      then show ?thesis ..
+    next
+      case 2
+      then have "?\<Phi> n"
+        using Schottky_lemma1 [OF that]
+        by (simp add: eeq) (simp add: power2_eq_square exp_add exp_Euler exp_of_real algebra_simps)
+      then show ?thesis ..
+    qed
+    then show ?thesis by blast
   qed
   have "\<exists>x. cos (complex_of_real pi * z) = of_int x"
     using assms
-    apply safe
-      apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq)
+    apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq simp flip: plusi_def)
      apply (auto simp: algebra_simps dest: 1 2)
-      done
+    done
   then have "sin(pi * cos(pi * z)) ^ 2 = 0"
     by (simp add: Complex_Transcendental.sin_eq_0)
   then have "1 - cos(pi * cos(pi * z)) ^ 2 = 0"
@@ -251,12 +258,10 @@
   proof -
     have "cmod (2 * f 0 - 1) \<le> cmod (2 * f 0) + 1"
       by (metis norm_one norm_triangle_ineq4)
-    also have "... \<le> 2 + cmod (f 0) * 3"
-      by simp
+    also have "... \<le> 6 + 9 * cmod (f 0)"
+      by auto
     finally have "1 + norm(2 * f 0 - 1) / 3 \<le> (2 + norm(f 0) - 1) * 3"
-      apply (simp add: field_split_simps)
-      using norm_ge_zero [of "f 0 * 2 - 1"]
-      by linarith
+      by (simp add: divide_simps)
     with nh0 have "norm(h 0) \<le> (2 + norm(f 0) - 1) * 3"
       by linarith
     then have "1 + norm(h 0) / 3 \<le> 2 + norm(f 0)"
@@ -277,12 +282,11 @@
     proof -
       have w: "w \<in> ball 0 1"
         using segment_bound [OF that] \<open>z \<in> ball 0 1\<close> by simp
-      have ttt: "\<And>z. z \<in> frontier (cball 0 1) \<Longrightarrow> 1 - t \<le> dist w z"
-        using \<open>norm z \<le> t\<close> segment_bound1 [OF \<open>w \<in> closed_segment 0 z\<close>]
-        apply (simp add: dist_complex_def)
-        by (metis diff_left_mono dist_commute dist_complex_def norm_triangle_ineq2 order_trans)
       have *: "\<lbrakk>\<And>b. (\<exists>w \<in> T \<union> U. w \<in> ball b 1); \<And>x. x \<in> D \<Longrightarrow> g x \<notin> T \<union> U\<rbrakk> \<Longrightarrow> \<nexists>b. ball b 1 \<subseteq> g ` D" for T U D
         by force
+      have ttt: "1 - t \<le> dist w u" if "cmod u = 1" for u
+        using \<open>norm z \<le> t\<close> segment_bound1 [OF \<open>w \<in> closed_segment 0 z\<close>] norm_triangle_ineq2 [of u w] that
+        by (simp add: dist_norm norm_minus_commute)
       have "\<nexists>b. ball b 1 \<subseteq> g ` cball 0 1"
       proof (rule *)
         show "(\<exists>w \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union>
@@ -304,8 +308,7 @@
               by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
             with le m \<open>0 < n\<close> show ?thesis
               apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI)
-               apply (simp_all del: Complex_eq greaterThan_0)
-              by blast
+               by (force simp del: Complex_eq greaterThan_0)+
           next
             case ge
             then obtain n where "0 < n" and n: "\<bar>- Im b - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
@@ -313,16 +316,13 @@
             have "dist b (Complex m (Im b)) \<le> 1/2"
               by (metis cancel_comm_monoid_add_class.diff_cancel cmod_eq_Re complex.sel(1) complex.sel(2) dist_norm m(2) minus_complex.code)
             moreover
-            have "dist (Complex m (- ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) (Complex m (Im b)) < 1/2"
-              using n
-              apply (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq)
-              by (metis add.commute add_uminus_conv_diff)
+            have "dist (Complex m (- ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) (Complex m (Im b)) 
+                = \<bar> - Im b - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar>"
+              by (simp add: complex_norm dist_norm cmod_eq_Re complex_diff)
             ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1"
-              by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
+              using n by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
             with ge m \<open>0 < n\<close> show ?thesis
-              apply (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI)
-               apply (simp_all del: Complex_eq greaterThan_0)
-              by blast
+              by (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI) auto
           qed
         qed
         show "g v \<notin> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union>
@@ -396,8 +396,10 @@
         using Rpos by blast
       have holg: "g holomorphic_on cball 0 1"
         unfolding g_def
-        apply (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf])
-        using Rpos by (auto simp: less_imp_le norm_mult)
+      proof (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf])
+        show "(*) (complex_of_real (R (f 0))) ` cball 0 1 \<subseteq> cball 0 (R (f 0))"
+          using Rpos by (auto simp: less_imp_le norm_mult)
+      qed
       have *: "norm(g z) \<le> exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12 * t / (1 - t))))"
            if "0 < t" "t < 1" "norm z \<le> t" for t z
       proof (rule Schottky [OF holg])
@@ -406,9 +408,9 @@
         show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not> (g z = 0 \<or> g z = 1)"
           using Rpos by (simp add: g_def less_imp_le norm_mult Rf)
       qed (auto simp: that)
-      have C1: "g holomorphic_on ball 0 (1 / 2)"
+      have C1: "g holomorphic_on ball 0 (1/2)"
         by (rule holomorphic_on_subset [OF holg]) auto
-      have C2: "continuous_on (cball 0 (1 / 2)) g"
+      have C2: "continuous_on (cball 0 (1/2)) g"
         by (meson cball_divide_subset_numeral holg holomorphic_on_imp_continuous_on holomorphic_on_subset)
       have C3: "cmod (g z) \<le> R (f 0) / 3" if "cmod (0 - z) = 1/2" for z
       proof -
@@ -426,9 +428,8 @@
         by (rule holomorphic_on_imp_differentiable_at [OF _ open_ball])
            (auto simp: Rpos [of "f 0"])
       have g_eq: "deriv g 0 = of_real ?r * deriv f 0"
-        apply (rule DERIV_imp_deriv)
-        apply (simp add: g_def)
-        by (metis DERIV_chain DERIV_cmult_Id fd0 field_differentiable_derivI mult.commute mult_zero_right)
+        unfolding g_def
+        by (metis DERIV_imp_deriv DERIV_chain DERIV_cmult_Id fd0 field_differentiable_derivI mult.commute mult_zero_right)
       show ?thesis
         using cmod_g'_le Rpos [of "f 0"]  by (simp add: g_eq norm_mult)
     qed
@@ -449,10 +450,10 @@
   show ?thesis
   proof (cases "\<forall>x. deriv f x = 0")
     case True
-    obtain c where "\<And>x. f(x) = c"
-      apply (rule DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf])
-       apply (metis True DiffE holf holomorphic_derivI open_UNIV, auto)
-      done
+    have "(f has_field_derivative 0) (at x)" for x
+      by (metis True UNIV_I holf holomorphic_derivI open_UNIV)
+    then obtain c where "\<And>x. f(x) = c"
+      by (meson UNIV_I DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf])
     then show ?thesis
       using that by auto
   next
@@ -468,12 +469,9 @@
         using f01 by (simp add: fw_def)
     qed
     have "(fw has_field_derivative deriv f w * inverse (deriv f w)) (at 0)"
-      apply (simp add: fw_def)
-      apply (rule DERIV_chain)
-      using holf holomorphic_derivI apply force
-      apply (intro derivative_eq_intros w)
-          apply (auto simp: field_simps)
-      done
+      unfolding fw_def
+      apply (intro DERIV_chain derivative_eq_intros w)+
+      using holf holomorphic_derivI by (force simp: field_simps)+
     then show ?thesis
       using norm_let1 w by (simp add: DERIV_imp_deriv)
   qed
@@ -538,8 +536,8 @@
     obtain c where c: "(\<lambda>x. (f(f x) - x)/(f x - x)) = (\<lambda>x. c)"
     proof (rule little_Picard_01)
       show "(\<lambda>x. (f(f x) - x)/(f x - x)) holomorphic_on UNIV"
-        apply (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf])
-        using non_fp by auto
+        using non_fp
+        by (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf]) auto
     qed auto
     then obtain "c \<noteq> 0" "c \<noteq> 1"
       by (metis (no_types, hide_lams) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
@@ -549,10 +547,8 @@
     proof (rule DERIV_unique)
       show "((\<lambda>x. f (f x) - c * f x) has_field_derivative
               deriv f z * (deriv f (f z) - c)) (at z)"
-        apply (intro derivative_eq_intros)
-            apply (rule DERIV_chain [unfolded o_def, of f])
-             apply (auto simp: algebra_simps intro!: holomorphic_derivI [OF holfU])
-        done
+        by (rule derivative_eq_intros holomorphic_derivI [OF holfU] 
+                    DERIV_chain [unfolded o_def, where f=f and g=f] | simp add: algebra_simps)+
       show "((\<lambda>x. f (f x) - c * f x) has_field_derivative 1 * (1 - c)) (at z)"
         by (simp add: eq mult_commute_abs)
     qed
@@ -601,8 +597,8 @@
       next
         case False
         have "\<And>x. (1 - k) * x \<noteq> f 0"
-          using l [of 0] apply (simp add: algebra_simps)
-          by (metis diff_add_cancel l mult.commute non_fp)
+          using l [of 0]
+          by (simp add: algebra_simps) (metis diff_add_cancel l mult.commute non_fp)
         then show False
           by (metis False eq_iff_diff_eq_0 mult.commute nonzero_mult_div_cancel_right times_divide_eq_right)
       qed
@@ -641,17 +637,20 @@
         by simp
     next
       case (Suc d) then show ?case
-        apply simp
-          using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast
+        using seq_suble [OF sub_kk] strict_mono_less_eq [OF sub_rr]
+        by (simp add: order_subst1)
     qed
     then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n"
       by (metis le_iff_add)
     show "strict_mono (\<lambda>n. rr n n)"
-      apply (simp add: strict_mono_Suc_iff)
-      by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr)
+      unfolding strict_mono_Suc_iff
+      by (simp add: Suc_le_lessD strict_monoD strict_mono_imp_increasing sub_kk sub_rr)
     have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i
-      apply (induction d arbitrary: i, auto)
-      by (meson order_trans seq_suble sub_kk)
+    proof (induction d arbitrary: i)
+      case (Suc d)
+      then show ?case
+        using seq_suble [OF sub_kk] by simp (meson order_trans)
+    qed auto
     then have "\<And>m n i. n \<le> m \<Longrightarrow> \<exists>j. i \<le> j \<and> rr m i = rr n j"
       by (metis le_iff_add)
     then show "P i (r \<circ> (\<lambda>n. rr n n))" for i
@@ -679,18 +678,13 @@
       have "f (r n) (\<sigma> i) \<in> cball 0 M" for n
         by (simp add: \<sigma> M)
       then show ?thesis
-        using compact_def [of "cball (0::'b) M"] apply simp
-        apply (drule_tac x="(\<lambda>n. f (r n) (\<sigma> i))" in spec)
-        apply (force simp: o_def)
-        done
+        using compact_def [of "cball (0::'b) M"] by (force simp: o_def)
     qed
-    show "\<And>i r k1 k2 N.
-               \<lbrakk>\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k1)) n (\<sigma> i)) \<longlonglongrightarrow> l; \<And>j. N \<le> j \<Longrightarrow> \<exists>j'\<ge>j. k2 j = k1 j'\<rbrakk>
-               \<Longrightarrow> \<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k2)) n (\<sigma> i)) \<longlonglongrightarrow> l"
-      apply (simp add: lim_sequentially)
-      apply (erule ex_forward all_forward imp_forward)+
-        apply auto
-      by (metis (no_types, hide_lams) le_cases order_trans)
+    show "\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k2)) n (\<sigma> i)) \<longlonglongrightarrow> l" 
+      if "\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k1)) n (\<sigma> i)) \<longlonglongrightarrow> l" "\<And>j. N \<le> j \<Longrightarrow> \<exists>j'\<ge>j. k2 j = k1 j'"
+      for i N and r k1 k2 :: "nat\<Rightarrow>nat"
+      using that
+      by (simp add: lim_sequentially) (metis (no_types, hide_lams) le_cases order_trans)
   qed auto
   with \<sigma> that show ?thesis
     by force
@@ -714,22 +708,18 @@
        if "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(r n) x - g x) < e"
        for g:: "'a \<Rightarrow> 'b" and r :: "nat \<Rightarrow> nat"
   proof (rule uniform_limit_theorem [of _ "\<F> \<circ> r"])
-    show "\<forall>\<^sub>F n in sequentially. continuous_on S ((\<F> \<circ> r) n)"
-      apply (simp add: eventually_sequentially)
-      apply (rule_tac x=0 in exI)
-      using UEQ apply (force simp: continuous_on_iff)
-      done
+    have "continuous_on S (\<F> (r n))" for n
+      using UEQ by (force simp: continuous_on_iff)
+    then show "\<forall>\<^sub>F n in sequentially. continuous_on S ((\<F> \<circ> r) n)"
+      by (simp add: eventually_sequentially)
     show "uniform_limit S (\<F> \<circ> r) g sequentially"
-      apply (simp add: uniform_limit_iff eventually_sequentially)
-        by (metis dist_norm that)
+      using that by (metis (mono_tags, hide_lams) comp_apply dist_norm uniform_limit_sequentially_iff)
   qed auto
   moreover
   obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
     by (metis separable that)
   obtain k where "strict_mono k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
-    apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M])
-    using \<open>R \<subseteq> S\<close> apply force+
-    done
+    using \<open>R \<subseteq> S\<close> by (force intro: function_convergent_subsequence [OF \<open>countable R\<close> M])
   then have Cauchy: "Cauchy ((\<lambda>n. \<F> (k n) x))" if "x \<in> R" for x
     using convergent_eq_Cauchy that by blast
   have "\<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> x \<in> S \<longrightarrow> dist ((\<F> \<circ> k) m x) ((\<F> \<circ> k) n x) < e"
@@ -741,8 +731,7 @@
     obtain T where "T \<subseteq> R" and "finite T" and T: "S \<subseteq> (\<Union>c\<in>T. ball c d)"
     proof (rule compactE_image [OF  \<open>compact S\<close>, of R "(\<lambda>x. ball x d)"])
       have "closure R \<subseteq> (\<Union>c\<in>R. ball c d)"
-        apply clarsimp
-        using \<open>0 < d\<close> closure_approachable by blast
+        using \<open>0 < d\<close> by (auto simp: closure_approachable)
       with SR show "S \<subseteq> (\<Union>c\<in>R. ball c d)"
         by auto
     qed auto
@@ -777,12 +766,10 @@
     then show ?thesis
       by force
   qed
-  then have "\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. norm(\<F>(k n) x - g x) < e"
-    using uniformly_convergent_eq_cauchy [of "\<lambda>x. x \<in> S" "\<F> \<circ> k"]
-    apply (simp add: o_def dist_norm)
-    by meson
+  then obtain g where "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> x \<in> S \<longrightarrow> norm ((\<F> \<circ> k) n x - g x) < e"
+    using uniformly_convergent_eq_cauchy [of "\<lambda>x. x \<in> S" "\<F> \<circ> k"] by (auto simp add: dist_norm)
   ultimately show thesis
-    by (metis that \<open>strict_mono k\<close>)
+    by (metis \<open>strict_mono k\<close> comp_apply that)
 qed
 
 
@@ -823,15 +810,15 @@
       proof -
         obtain r where "0 < r" and r: "cball z r \<subseteq> S"
           using z KS [of i] \<open>open S\<close> by (force simp: open_contains_cball)
-        have "cball z (2 / 3 * r) \<subseteq> cball z r"
+        have "cball z (2/3 * r) \<subseteq> cball z r"
           using \<open>0 < r\<close> by (simp add: cball_subset_cball_iff)
-        then have z23S: "cball z (2 / 3 * r) \<subseteq> S"
+        then have z23S: "cball z (2/3 * r) \<subseteq> S"
           using r by blast
         obtain M where "0 < M" and M: "\<And>n w. dist z w \<le> 2/3 * r \<Longrightarrow> norm(\<F> n w) \<le> M"
         proof -
           obtain N where N: "\<forall>n\<ge>N. cball z (2/3 * r) \<subseteq> K n"
-            using subK compact_cball [of z "(2 / 3 * r)"] z23S by force
-          have "cmod (\<F> n w) \<le> \<bar>B N\<bar> + 1" if "dist z w \<le> 2 / 3 * r" for n w
+            using subK compact_cball [of z "(2/3 * r)"] z23S by force
+          have "cmod (\<F> n w) \<le> \<bar>B N\<bar> + 1" if "dist z w \<le> 2/3 * r" for n w
           proof -
             have "w \<in> K N"
               using N mem_cball that by blast
@@ -849,27 +836,28 @@
               for n y
         proof -
           have "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral
-                    (2 * pi) * \<i> * winding_number (circlepath z (2 / 3 * r)) \<xi> * \<F> n \<xi>)
-                (circlepath z (2 / 3 * r))"
-             if "dist \<xi> z < (2 / 3 * r)" for \<xi>
+                    (2 * pi) * \<i> * winding_number (circlepath z (2/3 * r)) \<xi> * \<F> n \<xi>)
+                (circlepath z (2/3 * r))"
+             if "dist \<xi> z < (2/3 * r)" for \<xi>
           proof (rule Cauchy_integral_formula_convex_simple)
             have "\<F> n holomorphic_on S"
               by (simp add: \<H> \<open>\<And>n. \<F> n \<in> \<H>\<close>)
-            with z23S show "\<F> n holomorphic_on cball z (2 / 3 * r)"
+            with z23S show "\<F> n holomorphic_on cball z (2/3 * r)"
               using holomorphic_on_subset by blast
           qed (use that \<open>0 < r\<close> in \<open>auto simp: dist_commute\<close>)
           then have *: "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral (2 * pi) * \<i> * \<F> n \<xi>)
-                     (circlepath z (2 / 3 * r))"
-             if "dist \<xi> z < (2 / 3 * r)" for \<xi>
+                     (circlepath z (2/3 * r))"
+             if "dist \<xi> z < (2/3 * r)" for \<xi>
             using that by (simp add: winding_number_circlepath dist_norm)
            have y: "((\<lambda>w. \<F> n w / (w - y)) has_contour_integral (2 * pi) * \<i> * \<F> n y)
-                 (circlepath z (2 / 3 * r))"
-             apply (rule *)
-             using that \<open>0 < r\<close> by (simp only: dist_norm norm_minus_commute)
+                    (circlepath z (2/3 * r))"
+           proof (rule *)
+             show "dist y z < 2/3 * r"
+               using that \<open>0 < r\<close> by (simp only: dist_norm norm_minus_commute)
+           qed
            have z: "((\<lambda>w. \<F> n w / (w - z)) has_contour_integral (2 * pi) * \<i> * \<F> n z)
-                 (circlepath z (2 / 3 * r))"
-             apply (rule *)
-             using \<open>0 < r\<close> by simp
+                 (circlepath z (2/3 * r))"
+             using \<open>0 < r\<close> by (force intro!: *)
            have le_er: "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) \<le> e / r"
                 if "cmod (x - z) = r/3 + r/3" for x
            proof -
@@ -889,26 +877,26 @@
              also have "... = cmod (\<F> n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
                by (simp add: norm_mult norm_divide that)
              also have "... \<le> M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
-               apply (rule mult_mono)
-                  apply (rule leM)
-                 using \<open>r > 0\<close> \<open>M > 0\<close> neq by auto
-               also have "... < M * ((e * r / (6 * M)) / (cmod(x - y) * (2/3 * r)))"
-                 unfolding mult_less_cancel_left
-                 using y_near_z(2) \<open>M > 0\<close> \<open>r > 0\<close> neq
-                 apply (simp add: field_simps mult_less_0_iff norm_minus_commute)
-                 done
+               using \<open>r > 0\<close> \<open>M > 0\<close> by (intro mult_mono [OF leM]) auto
+             also have "... < M * ((e * r / (6 * M)) / (cmod(x - y) * (2/3 * r)))"
+               unfolding mult_less_cancel_left
+               using y_near_z(2) \<open>M > 0\<close> \<open>r > 0\<close> neq
+               by (simp add: field_simps mult_less_0_iff norm_minus_commute)
              also have "... \<le> e/r"
                using \<open>e > 0\<close> \<open>r > 0\<close> r4_le_xy by (simp add: field_split_simps)
              finally show ?thesis by simp
            qed
            have "(2 * pi) * cmod (\<F> n y - \<F> n z) = cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z)"
              by (simp add: right_diff_distrib [symmetric] norm_mult)
-           also have "cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z) \<le> e / r * (2 * pi * (2 / 3 * r))"
-             apply (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z], of "e/r"])
-             using \<open>e > 0\<close> \<open>r > 0\<close> le_er by auto
-           also have "... = (2 * pi) * e * ((2 / 3))"
+           also have "cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z) \<le> e / r * (2 * pi * (2/3 * r))"
+
+           proof (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z]])
+             show "\<And>x. cmod (x - z) = 2/3 * r \<Longrightarrow> cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) \<le> e / r"
+               using le_er by auto
+           qed (use \<open>e > 0\<close> \<open>r > 0\<close> in auto)
+           also have "... = (2 * pi) * e * ((2/3))"
              using \<open>r > 0\<close> by (simp add: field_split_simps)
-           finally have "cmod (\<F> n y - \<F> n z) \<le> e * (2 / 3)"
+           finally have "cmod (\<F> n y - \<F> n z) \<le> e * (2/3)"
              by simp
            also have "... < e"
              using \<open>e > 0\<close> by simp
@@ -934,29 +922,30 @@
     then show ?thesis
       by auto
   qed
-  have "\<exists>k g. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)"
-         for i r
-    apply (rule *)
-    using rng_f by auto
-  then have **: "\<And>i r. \<exists>k. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)"
-    by (force simp: o_assoc)
-  obtain k :: "nat \<Rightarrow> nat" where "strict_mono k"
-             and "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (id \<circ> k)) n x - g x) < e"
-    (* TODO: clean up this mess *)
-    apply (rule subsequence_diagonalization_lemma [OF **, of id id])
-     apply (erule ex_forward all_forward imp_forward)+
-      apply force
-     apply (erule exE)
-    apply (rename_tac i r k1 k2 N g e Na)
-     apply (rule_tac x="max N Na" in exI)
-     apply fastforce+
-    done
-  then have lt_e: "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> k) n x - g x) < e"
-    by simp
+  define \<Phi> where "\<Phi> \<equiv> \<lambda>g i r. \<lambda>k::nat\<Rightarrow>nat. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (r \<circ> k)) n x - g x) < e"
+  obtain k :: "nat \<Rightarrow> nat" where "strict_mono k" and k: "\<And>i. \<exists>g. \<Phi> g i id k"
+  proof (rule subsequence_diagonalization_lemma [where r=id])
+    show "\<exists>g. \<Phi> g i id (r \<circ> k2)" 
+      if ex: "\<exists>g. \<Phi> g i id (r \<circ> k1)" and "\<And>j. N \<le> j \<Longrightarrow> \<exists>j'\<ge>j. k2 j = k1 j'" 
+      for i k1 k2 N and r::"nat\<Rightarrow>nat"
+    proof -
+      obtain g where "\<Phi> g i id (r \<circ> k1)"
+        using ex by blast
+      then have "\<Phi> g i id (r \<circ> k2)"
+        using that
+        by (simp add: \<Phi>_def) (metis (no_types, hide_lams) le_trans linear)
+      then show ?thesis
+        by metis
+    qed
+    have "\<exists>k g. strict_mono (k::nat\<Rightarrow>nat) \<and> \<Phi> g i id (r \<circ> k)" for i r
+      unfolding \<Phi>_def o_assoc using rng_f by (force intro!: *)
+    then show "\<And>i r. \<exists>k. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<exists>g. \<Phi> g i id (r \<circ> k))"
+      by force
+  qed fastforce
   have "\<exists>l. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. norm(\<F> (k n) z - l) < e" if "z \<in> S" for z
   proof -
     obtain G where G: "\<And>i e. e > 0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K i. cmod ((\<F> \<circ> k) n x - G i x) < e"
-      using lt_e by metis
+      using k unfolding \<Phi>_def by (metis id_comp)
     obtain N where "\<And>n. n \<ge> N \<Longrightarrow> z \<in> K n"
       using subK [of "{z}"] that \<open>z \<in> S\<close> by auto
     moreover have "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K N. cmod ((\<F> \<circ> k) n x - G N x) < e"
@@ -976,11 +965,14 @@
       obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> T \<subseteq> K n"
         using subK [OF T] by blast
       obtain h where h: "\<And>e. e>0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K N. cmod ((\<F> \<circ> k) n x - h x) < e"
-        using lt_e by blast
+        using k unfolding \<Phi>_def by (metis id_comp)
       have geq: "g w = h w" if "w \<in> T" for w
-        apply (rule LIMSEQ_unique [of "\<lambda>n. \<F>(k n) w"])
-        using \<open>T \<subseteq> S\<close> g_lim that apply blast
-        using h N that by (force simp: lim_sequentially dist_norm)
+      proof (rule LIMSEQ_unique)
+        show "(\<lambda>n. \<F> (k n) w) \<longlonglongrightarrow> g w"
+          using \<open>T \<subseteq> S\<close> g_lim that by blast
+        show "(\<lambda>n. \<F> (k n) w) \<longlonglongrightarrow> h w"
+          using h N that by (force simp: lim_sequentially dist_norm)
+      qed
       show ?thesis
         using T h N \<open>0 < e\<close> by (fastforce simp add: geq)
     qed
@@ -1028,23 +1020,22 @@
   then have holf0: "\<F> n holomorphic_on ball z0 r" for n
     by (meson holf holomorphic_on_subset)
   have *: "((\<lambda>z. deriv (\<F> n) z / \<F> n z) has_contour_integral 0) (circlepath z0 (r/2))" for n
-  proof (rule Cauchy_theorem_disc_simple [of _ z0 r])
+  proof (rule Cauchy_theorem_disc_simple)
     show "(\<lambda>z. deriv (\<F> n) z / \<F> n z) holomorphic_on ball z0 r"
-      apply (intro holomorphic_intros holomorphic_deriv holf holf0 open_ball nz)
-      using \<open>ball z0 r \<subseteq> S\<close> by blast
+      by (metis (no_types) \<open>open S\<close> holf holomorphic_deriv holomorphic_on_divide holomorphic_on_subset nz subS)
   qed (use \<open>0 < r\<close> in auto)
   have hol_dg: "deriv g holomorphic_on S"
     by (simp add: \<open>open S\<close> holg holomorphic_deriv)
   have "continuous_on (sphere z0 (r/2)) (deriv g)"
-    apply (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg])
-    using \<open>0 < r\<close> subS by auto
+    using \<open>0 < r\<close> subS 
+    by (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg]) auto
   then have "compact (deriv g ` (sphere z0 (r/2)))"
     by (rule compact_continuous_image [OF _ compact_sphere])
   then have bo_dg: "bounded (deriv g ` (sphere z0 (r/2)))"
     using compact_imp_bounded by blast
   have "continuous_on (sphere z0 (r/2)) (cmod \<circ> g)"
-    apply (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg])
-    using \<open>0 < r\<close> subS by auto
+    using \<open>0 < r\<close> subS 
+    by (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg]) auto
   then have "compact ((cmod \<circ> g) ` sphere z0 (r/2))"
     by (rule compact_continuous_image [OF _ compact_sphere])
   moreover have "(cmod \<circ> g) ` sphere z0 (r/2) \<noteq> {}"
@@ -1063,51 +1054,54 @@
       proof (rule uniform_limitI)
         fix e::real
         assume "0 < e"
-        have *: "dist (deriv (\<F> n) w) (deriv g w) < e"
-          if e8: "\<And>x. dist z0 x \<le> 3 * r / 4 \<Longrightarrow> dist (\<F> n x) (g x) * 8 < r * e"
-          and w: "dist w z0 = r/2"  for n w
+
+        show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (deriv (\<F> n) x) (deriv g x) < e"
         proof -
-          have "ball w (r/4) \<subseteq> ball z0 r"  "cball w (r/4) \<subseteq> ball z0 r"
-            using \<open>0 < r\<close> by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff w)
-          with subS have wr4_sub: "ball w (r/4) \<subseteq> S" "cball w (r/4) \<subseteq> S" by force+
-          moreover
-          have "(\<lambda>z. \<F> n z - g z) holomorphic_on S"
-            by (intro holomorphic_intros holf holg)
-          ultimately have hol: "(\<lambda>z. \<F> n z - g z) holomorphic_on ball w (r/4)"
-            and cont: "continuous_on (cball w (r / 4)) (\<lambda>z. \<F> n z - g z)"
-            using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+
-          have "w \<in> S"
-            using \<open>0 < r\<close> wr4_sub by auto
-          have "\<And>y. dist w y < r / 4 \<Longrightarrow> dist z0 y \<le> 3 * r / 4"
-            apply (rule dist_triangle_le [where z=w])
-            using w by (simp add: dist_commute)
-          with e8 have in_ball: "\<And>y. y \<in> ball w (r/4) \<Longrightarrow> \<F> n y - g y \<in> ball 0 (r/4 * e/2)"
-            by (simp add: dist_norm [symmetric])
-          have "\<F> n field_differentiable at w"
-            by (metis holomorphic_on_imp_differentiable_at \<open>w \<in> S\<close> holf \<open>open S\<close>)
+          have "dist (deriv (\<F> n) w) (deriv g w) < e"
+            if e8: "\<And>x. dist z0 x \<le> 3 * r / 4 \<Longrightarrow> dist (\<F> n x) (g x) * 8 < r * e"
+              and w: "w \<in> sphere z0 (r/2)"  for n w
+          proof -
+            have "ball w (r/4) \<subseteq> ball z0 r"  "cball w (r/4) \<subseteq> ball z0 r"
+              using \<open>0 < r\<close> w by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff dist_commute)
+            with subS have wr4_sub: "ball w (r/4) \<subseteq> S" "cball w (r/4) \<subseteq> S" by force+
+            moreover
+            have "(\<lambda>z. \<F> n z - g z) holomorphic_on S"
+              by (intro holomorphic_intros holf holg)
+            ultimately have hol: "(\<lambda>z. \<F> n z - g z) holomorphic_on ball w (r/4)"
+              and cont: "continuous_on (cball w (r / 4)) (\<lambda>z. \<F> n z - g z)"
+              using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+
+            have "w \<in> S"
+              using \<open>0 < r\<close> wr4_sub by auto
+            have "dist z0 y \<le> 3 * r / 4" if "dist w y < r/4" for y
+            proof (rule dist_triangle_le [where z=w])
+              show "dist z0 w + dist y w \<le> 3 * r / 4"
+                using w that by (simp add: dist_commute)
+            qed
+            with e8 have in_ball: "\<And>y. y \<in> ball w (r/4) \<Longrightarrow> \<F> n y - g y \<in> ball 0 (r/4 * e/2)"
+              by (simp add: dist_norm [symmetric])
+            have "\<F> n field_differentiable at w"
+              by (metis holomorphic_on_imp_differentiable_at \<open>w \<in> S\<close> holf \<open>open S\<close>)
+            moreover
+            have "g field_differentiable at w"
+              using \<open>w \<in> S\<close> \<open>open S\<close> holg holomorphic_on_imp_differentiable_at by auto
+            moreover
+            have "cmod (deriv (\<lambda>w. \<F> n w - g w) w) * 2 \<le> e"
+              using Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1] \<open>r > 0\<close> by auto
+            ultimately have "dist (deriv (\<F> n) w) (deriv g w) \<le> e/2"
+              by (simp add: dist_norm)
+            then show ?thesis
+              using \<open>e > 0\<close> by auto
+          qed
           moreover
-          have "g field_differentiable at w"
-            using \<open>w \<in> S\<close> \<open>open S\<close> holg holomorphic_on_imp_differentiable_at by auto
-          moreover
-          have "cmod (deriv (\<lambda>w. \<F> n w - g w) w) * 2 \<le> e"
-            apply (rule Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1, simplified])
-            using \<open>r > 0\<close> by auto
-          ultimately have "dist (deriv (\<F> n) w) (deriv g w) \<le> e/2"
-            by (simp add: dist_norm)
-          then show ?thesis
-            using \<open>e > 0\<close> by auto
+          have "cball z0 (3 * r / 4) \<subseteq> ball z0 r"
+            by (simp add: cball_subset_ball_iff \<open>0 < r\<close>)
+          with subS have "uniform_limit (cball z0 (3 * r/4)) \<F> g sequentially"
+            by (force intro: ul_g)
+          then have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>cball z0 (3 * r / 4). dist (\<F> n x) (g x) < r / 4 * e / 2"
+            using \<open>0 < e\<close> \<open>0 < r\<close> by (force simp: intro!: uniform_limitD)
+          ultimately show ?thesis
+            by (force simp add: eventually_sequentially)
         qed
-        have "cball z0 (3 * r / 4) \<subseteq> ball z0 r"
-          by (simp add: cball_subset_ball_iff \<open>0 < r\<close>)
-        with subS have "uniform_limit (cball z0 (3 * r/4)) \<F> g sequentially"
-          by (force intro: ul_g)
-        then have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>cball z0 (3 * r / 4). dist (\<F> n x) (g x) < r / 4 * e / 2"
-          using \<open>0 < e\<close> \<open>0 < r\<close> by (force simp: intro!: uniform_limitD)
-        then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (deriv (\<F> n) x) (deriv g x) < e"
-          apply (simp add: eventually_sequentially)
-          apply (elim ex_forward all_forward imp_forward asm_rl)
-          using * apply (force simp: dist_commute)
-          done
       qed
       show "uniform_limit (sphere z0 (r/2)) \<F> g sequentially"
       proof (rule uniform_limitI)
@@ -1118,8 +1112,7 @@
         with subS have "uniform_limit (sphere z0 (r/2)) \<F> g sequentially"
           by (force intro: ul_g)
         then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (\<F> n x) (g x) < e"
-          apply (rule uniform_limitD)
-          using \<open>0 < e\<close> by force
+          using \<open>0 < e\<close> uniform_limit_iff by blast
       qed
       show "b > 0" "\<And>x. x \<in> sphere z0 (r/2) \<Longrightarrow> b \<le> cmod (g x)"
         using b \<open>0 < r\<close> by (fastforce simp: geq hnz)+
@@ -1140,19 +1133,18 @@
     have h_der: "(h has_field_derivative deriv h w) (at w)"
       using holh holomorphic_derivI w_inb by blast
     have "deriv g w = ((of_nat m * h w + deriv h w * (w - z0)) * (w - z0) ^ m) / (w - z0)"
-         if "r = dist z0 w * 2" "w \<noteq> z0"
+      if "r = dist z0 w * 2" "w \<noteq> z0"
     proof -
       have "((\<lambda>w. (w - z0) ^ m * h w) has_field_derivative
             (m * h w + deriv h w * (w - z0)) * (w - z0) ^ m / (w - z0)) (at w)"
         apply (rule derivative_eq_intros h_der refl)+
         using that \<open>m > 0\<close> \<open>0 < r\<close> apply (simp add: divide_simps distrib_right)
-        apply (metis Suc_pred mult.commute power_Suc)
-        done
+        by (metis Suc_pred mult.commute power_Suc)
       then show ?thesis
-        apply (rule DERIV_imp_deriv [OF has_field_derivative_transform_within_open [where S = "ball z0 r"]])
-        using that \<open>m > 0\<close> \<open>0 < r\<close>
-          apply (simp_all add: hnz geq)
-        done
+      proof (rule DERIV_imp_deriv [OF has_field_derivative_transform_within_open])
+        show "\<And>x. x \<in> ball z0 r \<Longrightarrow> (x - z0) ^ m * h x = g x"
+          by (simp add: hnz geq)
+      qed (use that \<open>m > 0\<close> \<open>0 < r\<close> in auto)
     qed
     with \<open>0 < r\<close> \<open>0 < m\<close> w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w"
       by (auto simp: geq field_split_simps hnz)
@@ -1164,10 +1156,8 @@
     show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))"
       by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple)
     show "((\<lambda>x. deriv h x / h x) has_contour_integral 0) (circlepath z0 (r/2))"
-      apply (rule Cauchy_theorem_disc_simple [of _ z0 r])
       using hnz holh holomorphic_deriv holomorphic_on_divide \<open>0 < r\<close>
-         apply force+
-      done
+      by (fastforce intro!: Cauchy_theorem_disc_simple [of _ z0 r])
   qed
   ultimately show False using \<open>0 < m\<close> by auto
 qed
@@ -1215,17 +1205,9 @@
           using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
         then have z1: "\<forall>\<^sub>F n in sequentially. dist (\<F> n z1) (g z1) < e/2"
           by simp
-        have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e/2 + e/2"
-          apply (rule eventually_mono [OF eventually_conj [OF K z1]])
-          apply (simp add: dist_norm algebra_simps del: divide_const_simps)
-          by (metis add.commute dist_commute dist_norm dist_triangle_add_half)
-        have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e/2 + e/2"
-          using eventually_conj [OF K z1]
-          apply (rule eventually_mono)
-          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half field_sum_of_halves)
-        then
-        show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
-          by simp
+        show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e" 
+          apply (rule eventually_mono [OF  eventually_conj [OF K z1]])
+          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half)
       qed
       show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"
         unfolding constant_on_def
@@ -1264,22 +1246,28 @@
     proof -
       have "h \<in> X"
         using \<open>Y \<subseteq> X\<close> \<open>h \<in> Y\<close>  by blast
-      with holX have "h holomorphic_on S" 
-        by auto
-      then have "h holomorphic_on cball w e"
-        by (metis e holomorphic_on_subset)
-      then have hol_h_o: "(h \<circ> (\<lambda>z. (w + of_real e * z))) holomorphic_on cball 0 1"
-        apply (intro holomorphic_intros holomorphic_on_compose)
-        apply (erule holomorphic_on_subset)
-        using that \<open>e > 0\<close> by (auto simp: dist_norm norm_mult)
+      have hol_h_o: "(h \<circ> (\<lambda>z. (w + of_real e * z))) holomorphic_on cball 0 1"
+      proof (intro holomorphic_intros holomorphic_on_compose)
+        have "h holomorphic_on S" 
+          using holX \<open>h \<in> X\<close> by auto
+        then have "h holomorphic_on cball w e"
+          by (metis e holomorphic_on_subset)
+        moreover have "(\<lambda>z. w + complex_of_real e * z) ` cball 0 1 \<subseteq> cball w e"
+          using that \<open>e > 0\<close> by (auto simp: dist_norm norm_mult)
+        ultimately show "h holomorphic_on (\<lambda>z. w + complex_of_real e * z) ` cball 0 1"
+          by (rule holomorphic_on_subset)
+      qed
       have norm_le_r: "cmod ((h \<circ> (\<lambda>z. w + complex_of_real e * z)) 0) \<le> r"
         by (auto simp: r \<open>h \<in> Y\<close>)
       have le12: "norm (of_real(inverse e) * (z - w)) \<le> 1/2"
         using that \<open>e > 0\<close> by (simp add: inverse_eq_divide dist_norm norm_minus_commute norm_divide)
-      have non01: "\<And>z::complex. cmod z \<le> 1 \<Longrightarrow> h (w + e * z) \<noteq> 0 \<and> h (w + e * z) \<noteq> 1"
-        apply (rule X01 [OF \<open>h \<in> X\<close>])
-          apply (rule subsetD [OF e])
-        using \<open>0 < e\<close>  by (auto simp: dist_norm norm_mult)
+      have non01: "h (w + e * z) \<noteq> 0 \<and> h (w + e * z) \<noteq> 1" if "z \<in> cball 0 1" for z::complex
+      proof (rule X01 [OF \<open>h \<in> X\<close>])
+        have "w + complex_of_real e * z \<in> cball w e"
+          using \<open>0 < e\<close> that by (auto simp: dist_norm norm_mult)
+        then show "w + complex_of_real e * z \<in> S"
+          by (rule subsetD [OF e])
+      qed
       have "cmod (h z) \<le> cmod (h (w + of_real e * (inverse e * (z - w))))"
         using \<open>0 < e\<close> by (simp add: field_split_simps)
       also have "... \<le> exp (pi * exp (pi * (14 + 2 * r)))"
@@ -1313,8 +1301,7 @@
     proof -
       obtain B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" 
         and  "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-        apply (rule GPicard1 [OF S zero_less_one \<open>Y \<subseteq> X\<close> holX])
-        using no_hw_le1 X01 by force+
+        using GPicard1 [OF S zero_less_one \<open>Y \<subseteq> X\<close> holX] X01 no_hw_le1 by blast
       then show ?thesis
         unfolding U_def using \<open>w \<in> S\<close> by blast
     qed
@@ -1331,9 +1318,10 @@
         by metis
       define \<G> where "\<G> \<equiv> \<lambda>n z. inverse(\<F> n z)"
       have hol\<G>: "\<G> n holomorphic_on S" for n
-        apply (simp add: \<G>_def)
-        using FY X01 \<open>Y \<subseteq> X\<close> holX apply (blast intro: holomorphic_on_inverse)
-        done
+      proof (simp add: \<G>_def)
+        show "(\<lambda>z. inverse (\<F> n z)) holomorphic_on S"
+          using FY X01 \<open>Y \<subseteq> X\<close> holX by (blast intro: holomorphic_on_inverse)
+      qed
       have \<G>not0: "\<G> n z \<noteq> 0" and \<G>not1: "\<G> n z \<noteq> 1" if "z \<in> S" for n z
         using FY X01 \<open>Y \<subseteq> X\<close> that by (force simp: \<G>_def)+
       have \<G>_le1: "cmod (\<G> n v) \<le> 1" for n 
@@ -1387,7 +1375,8 @@
               and "\<And>h z'. \<lbrakk>h \<in> Y; z' \<in> T\<rbrakk> \<Longrightarrow> cmod (h z') \<le> C"
               using \<open>y \<in> U\<close> by (auto simp: U_def)
             then have le_C: "\<And>n. cmod (\<F> n y) \<le> C"
-              using FY by blast                
+              using FY by blast
+
             have "\<forall>\<^sub>F n in sequentially. dist (\<G> (j n) y) (h y) < inverse C"
               using uniform_limitD [OF ulim [of "{y}"], of "inverse C"] \<open>C > 0\<close> y
               by (simp add: dist_commute)
@@ -1396,11 +1385,10 @@
             moreover
             have "h y = h v"
               by (metis \<open>h v = c\<close> dist_commute that y)
-            ultimately have "norm (\<G> (j n) y) < inverse C"
-              by (simp add: \<open>h v = 0\<close>)
+            ultimately have "cmod (inverse (\<F> (j n) y)) < inverse C"
+              by (simp add: \<open>h v = 0\<close> \<G>_def)
             then have "C < norm (\<F> (j n) y)"
-              apply (simp add: \<G>_def)
-              by (metis FY X01 \<open>0 < C\<close> \<open>y \<in> S\<close> \<open>Y \<subseteq> X\<close> inverse_less_iff_less norm_inverse subsetD zero_less_norm_iff)
+              by (metis \<G>_def \<G>not0 \<open>y \<in> S\<close> inverse_less_imp_less inverse_zero norm_inverse zero_less_norm_iff)
             show False
               using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast
           qed
@@ -1413,11 +1401,14 @@
       qed (use \<open>e > 0\<close> in auto)
       with \<open>h v = 0\<close> show False by blast
     qed
-    then show "v \<in> U"
-      apply (clarsimp simp add: U_def v)
-      apply (rule GPicard1[OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> _ \<open>Y \<subseteq> X\<close> holX])
-      using X01 no_hw_le1 apply (meson | force simp: not_less)+
-      done
+    then obtain r where "0 < r" and r: "\<And>h. h \<in> Y \<Longrightarrow> cmod (h v) \<le> r"
+      by (metis not_le)
+    moreover     
+    obtain B Z where "0 < B" "open Z" "v \<in> Z" "Z \<subseteq> S" "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
+      using X01 
+      by (auto simp: r intro: GPicard1[OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> \<open>r>0\<close> \<open>Y \<subseteq> X\<close> holX] X01)
+    ultimately show "v \<in> U"
+      using v by (simp add: U_def) meson
   qed
   have "\<And>x. x \<in> K \<longrightarrow> x \<in> U"
     using \<open>U = S\<close> \<open>K \<subseteq> S\<close> by blast
@@ -1436,10 +1427,10 @@
     case True with L show ?thesis by simp
   next
     case False
-    with \<open>finite L\<close> show ?thesis 
-      apply (rule_tac x = "Max (F ` L)" in exI)
-      apply (simp add: linorder_class.Max_ge_iff)
-      using * F  by (metis L UN_E subsetD)
+    then have "\<forall>h z. h \<in> Y \<and> z \<in> K \<longrightarrow> (\<exists>x\<in>L. cmod (h z) \<le> F x)"
+      by (metis "*" L UN_E subset_iff)
+    with False \<open>finite L\<close> show ?thesis 
+      by (rule_tac x = "Max (F ` L)" in exI) (simp add: linorder_class.Max_ge_iff)
   qed
   with that show ?thesis by metis
 qed
@@ -1467,15 +1458,15 @@
       have *: "norm(f w) \<le> B" if "w \<in> cball 0 \<epsilon> - ball 0 d" for w
       proof (rule maximum_modulus_frontier [of f "cball 0 \<epsilon> - ball 0 d"])
         show "f holomorphic_on interior (cball 0 \<epsilon> - ball 0 d)"
-          apply (rule holomorphic_on_subset [OF holf])
-          using \<open>\<epsilon> < k\<close> \<open>0 < d\<close> that by auto
+          using \<open>\<epsilon> < k\<close> \<open>0 < d\<close> that by (auto intro:  holomorphic_on_subset [OF holf])
         show "continuous_on (closure (cball 0 \<epsilon> - ball 0 d)) f"
-          apply (rule holomorphic_on_imp_continuous_on)
-          apply (rule holomorphic_on_subset [OF holf])
-          using \<open>0 < d\<close> \<open>\<epsilon> < k\<close> by auto
+        proof (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holf])
+          show "closure (cball 0 \<epsilon> - ball 0 d) \<subseteq> ball 0 k - {0}"
+            using \<open>0 < d\<close> \<open>\<epsilon> < k\<close> by auto
+        qed
         show "\<And>z. z \<in> frontier (cball 0 \<epsilon> - ball 0 d) \<Longrightarrow> cmod (f z) \<le> B"
-          apply (simp add: frontier_def)
-          using \<epsilon> d less_eq_real_def by blast
+          unfolding frontier_def
+          using \<epsilon> d less_eq_real_def by force
       qed (use that in auto)
       show ?thesis
         using * \<open>d < cmod \<xi>\<close> that by auto
@@ -1505,9 +1496,8 @@
       by (intro holomorphic_intros) auto
   qed
   have h01: "\<And>n z. z \<in> ball 0 1 - {0} \<Longrightarrow> h n z \<noteq> 0 \<and> h n z \<noteq> 1" 
-    unfolding h_def
-    apply (rule f01)
-    using * by force
+    unfolding h_def 
+    using * by (force intro!: f01)
   obtain w where w: "w \<in> ball 0 1 - {0::complex}"
     by (rule_tac w = "1/2" in that) auto
   consider "infinite {n. norm(h n w) \<le> 1}" | "infinite {n. 1 \<le> norm(h n w)}"
@@ -1521,11 +1511,8 @@
     obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (h \<circ> r)\<rbrakk> \<Longrightarrow> norm(j z) \<le> B"
     proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
       show "range (h \<circ> r) \<subseteq> 
-            {g. g holomorphic_on ball 0 1 - {0} \<and> (\<forall>z\<in>ball 0 1 - {0}. g z \<noteq> 0 \<and> g z \<noteq> 1)}"
-        apply clarsimp
-        apply (intro conjI holomorphic_intros holomorphic_on_compose holh)
-        using h01 apply auto
-        done
+            {g. g holomorphic_on ball 0 1 - {0} \<and> (\<forall>z \<in> ball 0 1 - {0}. g z \<noteq> 0 \<and> g z \<noteq> 1)}"
+        using h01 by (auto intro: holomorphic_intros holomorphic_on_compose holh)
       show "connected (ball 0 1 - {0::complex})"
         by (simp add: connected_open_delete)
     qed (use r in auto)        
@@ -1558,8 +1545,7 @@
     have "0 < \<bar>B\<bar> + 1"
       by simp
     then show ?thesis
-      apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>])
-      using \<epsilon> by auto 
+      using \<epsilon> by (force intro!: that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>])
   next
     case 2
     with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" 
@@ -1569,10 +1555,7 @@
     proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
       show "range (\<lambda>n. inverse \<circ> h (r n)) \<subseteq> 
             {g. g holomorphic_on ball 0 1 - {0} \<and> (\<forall>z\<in>ball 0 1 - {0}. g z \<noteq> 0 \<and> g z \<noteq> 1)}"
-        apply clarsimp
-        apply (intro conjI holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose)
-        using h01 apply auto
-        done
+        using h01 by (auto intro!: holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose)
       show "connected (ball 0 1 - {0::complex})"
         by (simp add: connected_open_delete)
       show "\<And>j. j \<in> range (\<lambda>n. inverse \<circ> h (r n)) \<Longrightarrow> cmod (j w) \<le> 1"
@@ -1621,8 +1604,8 @@
     then have "inverse B > 0"
       by (simp add: field_split_simps)
     then show ?thesis
-      apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>])
-      using \<epsilon> by auto 
+      using \<epsilon> that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>]
+      by (metis Diff_iff dist_0_norm insert_iff mem_ball)
   qed
 qed
 
@@ -1641,13 +1624,14 @@
     and B: "(\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<le> B) \<or> (\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<ge> B)"
   proof (rule GPicard5)
     show "?g holomorphic_on ball 0 1 - {0}"
-      apply (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf])
-      using \<open>0 < r\<close> \<open>a \<noteq> 0\<close> r
-      by (auto simp: dist_norm norm_mult subset_eq)
+    proof (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf])
+      show "(\<lambda>x. z + complex_of_real r * x) ` (ball 0 1 - {0}) \<subseteq> M - {z}"
+        using \<open>0 < r\<close> r
+        by (auto simp: dist_norm norm_mult subset_eq)
+    qed (use \<open>a \<noteq> 0\<close> in auto)
     show "\<And>w. w \<in> ball 0 1 - {0} \<Longrightarrow> f (z + of_real r * w) / a \<noteq> 0 \<and> f (z + of_real r * w) / a \<noteq> 1"
-      apply (simp add: field_split_simps \<open>a \<noteq> 0\<close>)
-      apply (rule f0a)
-      using \<open>0 < r\<close> r by (auto simp: dist_norm norm_mult subset_eq)
+      using f0a \<open>0 < r\<close> \<open>a \<noteq> 0\<close> r
+      by (auto simp: field_split_simps dist_norm norm_mult subset_eq)
   qed
   show ?thesis
   proof
@@ -1697,50 +1681,50 @@
       by (intro holomorphic_intros holf)
   qed (use fab in auto)
   have holfb: "f holomorphic_on ball z r - {z}"
-    apply (rule holomorphic_on_subset [OF holf])
-    using zrM by auto
+    using zrM by (auto intro: holomorphic_on_subset [OF holf])
   have holfb_i: "(\<lambda>z. inverse(f z - a)) holomorphic_on ball z r - {z}"
-    apply (intro holomorphic_intros holfb)
-    using fab zrM by fastforce
+    using fab zrM by (fastforce intro!: holomorphic_intros holfb)
   show ?thesis
     using r
   proof              
     assume "bounded ((\<lambda>z. f z - a) ` (ball z r - {z}))"
     then obtain B where B: "\<And>w. w \<in> (\<lambda>z. f z - a) ` (ball z r - {z}) \<Longrightarrow> norm w \<le> B"
       by (force simp: bounded_iff)
-    have "\<forall>\<^sub>F w in at z. cmod (f w - a) \<le> B"
-      apply (simp add: eventually_at)
-      apply (rule_tac x=r in exI)
-      using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B)
-    then have "\<exists>B. \<forall>\<^sub>F w in at z. cmod (f w) \<le> B"
-      apply (rule_tac x="B + norm a" in exI)
-        apply (erule eventually_mono)
+    then have "\<forall>x. x \<noteq> z \<and> dist x z < r \<longrightarrow> cmod (f x - a) \<le> B"
+      by (simp add: dist_commute)
+    with \<open>0 < r\<close> have "\<forall>\<^sub>F w in at z. cmod (f w - a) \<le> B"
+      by (force simp add: eventually_at)
+    moreover have "\<And>x. cmod (f x - a) \<le> B \<Longrightarrow> cmod (f x) \<le> B + cmod a"
       by (metis add.commute add_le_cancel_right norm_triangle_sub order.trans)
+    ultimately have "\<exists>B. \<forall>\<^sub>F w in at z. cmod (f w) \<le> B"
+      by (metis (mono_tags, lifting) eventually_at)
     then obtain g where holg: "g holomorphic_on ball z r" and gf: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w = f w"
       using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb] by auto
     then have "g \<midarrow>z\<rightarrow> g z"
-      apply (simp add: continuous_at [symmetric])
-      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
+      unfolding continuous_at [symmetric]
+      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at 
+            holomorphic_on_imp_differentiable_at by blast
     then have "(f \<longlongrightarrow> g z) (at z)"
-      apply (rule Lim_transform_within_open [of g "g z" z UNIV "ball z r"])
-      using  \<open>0 < r\<close> by (auto simp: gf)
+      using Lim_transform_within_open [of g "g z" z]
+      using \<open>0 < r\<close> centre_in_ball gf by blast
     then show ?thesis
       using that by blast
   next
     assume "bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
     then obtain B where B: "\<And>w. w \<in> (inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}) \<Longrightarrow> norm w \<le> B"
       by (force simp: bounded_iff)
-    have "\<forall>\<^sub>F w in at z. cmod (inverse (f w - a)) \<le> B"
-      apply (simp add: eventually_at)
-      apply (rule_tac x=r in exI)
-      using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B)
+    then have "\<forall>x. x \<noteq> z \<and> dist x z < r \<longrightarrow> cmod (inverse (f x - a)) \<le> B"
+      by (simp add: dist_commute)
+    with \<open>0 < r\<close> have "\<forall>\<^sub>F w in at z. cmod (inverse (f w - a)) \<le> B"
+      by (auto simp add: eventually_at)
     then have "\<exists>B. \<forall>\<^sub>F z in at z. cmod (inverse (f z - a)) \<le> B"
       by blast
     then obtain g where holg: "g holomorphic_on ball z r" and gf: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w = inverse (f w - a)"
       using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb_i] by auto
     then have gz: "g \<midarrow>z\<rightarrow> g z"
-      apply (simp add: continuous_at [symmetric])
-      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
+      unfolding continuous_at [symmetric]
+      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at 
+            holomorphic_on_imp_differentiable_at by blast
     have gnz: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w \<noteq> 0"
       using gf fab zrM by fastforce
     show ?thesis
@@ -1764,8 +1748,7 @@
         have "(f \<longlongrightarrow> 0) (at z)"
         proof (rule Lim_transform_within_open [of "\<lambda>w. (1 + a * g w) / g w" _ _ _ "ball z r"])
           show "(\<lambda>w. (1 + a * g w) / g w) \<midarrow>z\<rightarrow> 0"
-            apply (rule tendsto_eq_intros refl gz \<open>g z \<noteq> 0\<close>)+
-            by (simp add: True)
+            by (rule tendsto_eq_intros refl gz \<open>g z \<noteq> 0\<close> | simp add: True)+
           show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> (1 + a * g x) / g x = f x"
             using fab fab zrM by (fastforce simp add: gf field_split_simps)
         qed (use \<open>0 < r\<close> in auto)
@@ -1793,8 +1776,8 @@
   assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
     and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
   obtains a where "- {a} \<subseteq> f ` (M - {z})"
-  apply (simp add: subset_iff image_iff)
-  by (metis great_Picard [OF M _ holf] non)
+unfolding subset_iff image_iff
+  by (metis great_Picard [OF M _ holf] non Compl_iff insertI1)
     
 
 corollary great_Picard_infinite:
@@ -1815,8 +1798,7 @@
       proof (cases "{x \<in> M - {z}. f x \<in> {a, b}} = {}")
         case True
         then show ?thesis
-          apply (rule_tac r=e in that)
-          using e \<open>e > 0\<close> by auto
+          using e \<open>e > 0\<close> that by fastforce
       next
         case False
         let ?r = "min e (Min (dist z ` {x \<in> M - {z}. f x \<in> {a,b}}))"