# Theory Great_Picard

theory Great_Picard
imports Conformal_Mappings Further_Topology
section‹The Great Picard Theorem and its Applications›

text‹Ported from HOL Light (cauchy.ml) by L C Paulson, 2017›

theory Great_Picard
imports Conformal_Mappings Further_Topology

begin

subsection‹Schottky's theorem›

lemma Schottky_lemma0:
assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a ∈ S"
and f: "⋀z. z ∈ S ⟹ f z ≠ 1 ∧ f z ≠ -1"
obtains g where "g holomorphic_on S"
"norm(g a) ≤ 1 + norm(f a) / 3"
"⋀z. z ∈ S ⟹ f z = cos(of_real pi * g z)"
proof -
obtain g where holg: "g holomorphic_on S" and g: "norm(g a) ≤ pi + norm(f a)"
and f_eq_cos: "⋀z. z ∈ S ⟹ f z = cos(g z)"
using contractible_imp_holomorphic_arccos_bounded [OF assms]
by blast
show ?thesis
proof
show "(λz. g z / pi) holomorphic_on S"
by (auto intro: holomorphic_intros holg)
have "3 ≤ pi"
using pi_approx by force
have "3 * norm(g a) ≤ 3 * (pi + norm(f a))"
using g by auto
also have "... ≤  pi * 3 + pi * cmod (f a)"
using ‹3 ≤ pi› by (simp add: mult_right_mono algebra_simps)
finally show "cmod (g a / complex_of_real pi) ≤ 1 + cmod (f a) / 3"
show "⋀z. z ∈ S ⟹ f z = cos (complex_of_real pi * (g z / complex_of_real pi))"
qed
qed

lemma Schottky_lemma1:
fixes n::nat
assumes "0 < n"
shows "0 < n + sqrt(real n ^ 2 - 1)"
proof -
have "(n-1)^2 ≤ n^2 - 1"
using assms by (simp add: algebra_simps power2_eq_square)
then have "real (n - 1) ≤ sqrt (real (n⇧2 - 1))"
by (metis of_nat_le_iff of_nat_power real_le_rsqrt)
then have "n-1 ≤ sqrt(real n ^ 2 - 1)"
by (simp add: Suc_leI assms of_nat_diff)
then show ?thesis
using assms by linarith
qed

lemma Schottky_lemma2:
fixes x::real
assumes "0 ≤ x"
obtains n where "0 < n" "¦x - ln (real n + sqrt ((real n)⇧2 - 1)) / pi¦ < 1/2"
proof -
obtain n0::nat where "0 < n0" "ln(n0 + sqrt(real n0 ^ 2 - 1)) / pi ≤ x"
proof
show "ln(real 1 + sqrt(real 1 ^ 2 - 1))/pi ≤ x"
by (auto simp: assms)
qed auto
moreover
obtain M::nat where "⋀n. ⟦0 < n; ln(n + sqrt(real n ^ 2 - 1)) / pi ≤ x⟧ ⟹ n ≤ M"
proof
fix n::nat
assume "0 < n" "ln (n + sqrt ((real n)⇧2 - 1)) / pi ≤ x"
then have "ln (n + sqrt ((real n)⇧2 - 1)) ≤ x * pi"
then have *: "exp (ln (n + sqrt ((real n)⇧2 - 1))) ≤ exp (x * pi)"
by blast
have 0: "0 ≤ sqrt ((real n)⇧2 - 1)"
using ‹0 < n› by auto
have "n + sqrt ((real n)⇧2 - 1) = exp (ln (n + sqrt ((real n)⇧2 - 1)))"
also have "... ≤ exp (x * pi)"
using "*" by blast
finally have "real n ≤ exp (x * pi)"
using 0 by linarith
then show "n ≤ nat (ceiling (exp(x * pi)))"
by linarith
qed
ultimately obtain n where
"0 < n" and le_x: "ln(n + sqrt(real n ^ 2 - 1)) / pi ≤ x"
and le_n: "⋀k. ⟦0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi ≤ x⟧ ⟹ k ≤ n"
using bounded_Max_nat [of "λn. 0<n ∧ ln (n + sqrt ((real n)⇧2 - 1)) / pi ≤ x"] by metis
define a where "a ≡ ln(n + sqrt(real n ^ 2 - 1)) / pi"
define b where "b ≡ ln (1 + real n + sqrt ((1 + real n)⇧2 - 1)) / pi"
have le_xa: "a ≤ x"
and le_na: "⋀k. ⟦0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi ≤ x⟧ ⟹ k ≤ n"
using le_x le_n by (auto simp: a_def)
moreover have "x < b"
using le_n [of "Suc n"] by (force simp: b_def)
moreover have "b - a < 1"
proof -
have "ln (1 + real n + sqrt ((1 + real n)⇧2 - 1)) - ln (real n + sqrt ((real n)⇧2 - 1)) =
ln ((1 + real n + sqrt ((1 + real n)⇧2 - 1)) / (real n + sqrt ((real n)⇧2 - 1)))"
also have "... ≤ 3"
proof (cases "n = 1")
case True
have "sqrt 3 ≤ 2"
then have "(2 + sqrt 3) ≤ 4"
by simp
also have "... ≤ exp 3"
using exp_ge_add_one_self [of "3::real"] by simp
finally have "ln (2 + sqrt 3) ≤ 3"
dbl_simps(3) exp_gt_zero ln_exp ln_le_cancel_iff real_sqrt_ge_0_iff zero_le_one zero_less_one)
then show ?thesis
next
case False with ‹0 < n› have "1 < n" "2 ≤ n"
by linarith+
then have 1: "1 ≤ real n * real n"
by (metis less_imp_le_nat one_le_power power2_eq_square real_of_nat_ge_one_iff)
have *: "4 + (m+2) * 2 ≤ (m+2) * ((m+2) * 3)" for m::nat
by simp
have "4 + n * 2 ≤ n * (n * 3)"
using * [of "n-2"]  ‹2 ≤ n›
then have **: "4 + real n * 2 ≤ real n * (real n * 3)"
by (metis (mono_tags, hide_lams) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral)
have "sqrt ((1 + real n)⇧2 - 1) ≤ 2 * sqrt ((real n)⇧2 - 1)"
by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **)
then
have "((1 + real n + sqrt ((1 + real n)⇧2 - 1)) / (real n + sqrt ((real n)⇧2 - 1))) ≤ 2"
using Schottky_lemma1 ‹0 < n›  by (simp add: divide_simps)
then have "ln ((1 + real n + sqrt ((1 + real n)⇧2 - 1)) / (real n + sqrt ((real n)⇧2 - 1))) ≤ ln 2"
apply (subst ln_le_cancel_iff)
using Schottky_lemma1 ‹0 < n› by auto (force simp: divide_simps)
also have "... ≤ 3"
using ln_add_one_self_le_self [of 1] by auto
finally show ?thesis .
qed
also have "... < pi"
using pi_approx by simp
finally show ?thesis
by (simp add: a_def b_def divide_simps)
qed
ultimately have "¦x - a¦ < 1/2 ∨ ¦x - b¦ < 1/2"
by (auto simp: abs_if)
then show thesis
proof
assume "¦x - a¦ < 1 / 2"
then show ?thesis
by (rule_tac n=n in that) (auto simp: a_def ‹0 < n›)
next
assume "¦x - b¦ < 1 / 2"
then show ?thesis
by (rule_tac n="Suc n" in that) (auto simp: b_def ‹0 < n›)
qed
qed

lemma Schottky_lemma3:
fixes z::complex
assumes "z ∈ (⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
∪ (⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
shows "cos(pi * cos(pi * z)) = 1 ∨ cos(pi * cos(pi * z)) = -1"
proof -
have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x ≥ 0" for x::real
by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
have 1: "∃k. exp (𝗂 * (of_int m * complex_of_real pi) -
(ln (real n + sqrt ((real n)⇧2 - 1)))) +
inverse
(exp (𝗂 * (of_int m * complex_of_real pi) -
(ln (real n + sqrt ((real n)⇧2 - 1))))) = of_int k * 2"
if "n > 0" for m n
proof -
have eeq: "e ≠ 0 ⟹ e + inverse e = n*2 ⟷ inverse e^2 - 2 * n*inverse e + 1 = 0" for n e::complex
by (auto simp: field_simps power2_eq_square)
have [simp]: "1 ≤ 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
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: "∃k. exp (𝗂 * (of_int m * complex_of_real pi) +
(ln (real n + sqrt ((real n)⇧2 - 1)))) +
inverse
(exp (𝗂 * (of_int m * complex_of_real pi) +
(ln (real n + sqrt ((real n)⇧2 - 1))))) = of_int k * 2"
if "n > 0" for m n
proof -
have eeq: "e ≠ 0 ⟹ e + inverse e = n*2 ⟷ e^2 - 2 * n*e + 1 = 0" for n e::complex
by (auto simp: field_simps power2_eq_square)
have [simp]: "1 ≤ 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
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
qed
have "∃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: algebra_simps dest: 1 2)
done
then have "sin(pi * cos(pi * z)) ^ 2 = 0"
then have "1 - cos(pi * cos(pi * z)) ^ 2 = 0"
then show ?thesis
using power2_eq_1_iff by auto
qed

theorem Schottky:
assumes holf: "f holomorphic_on cball 0 1"
and nof0: "norm(f 0) ≤ r"
and not01: "⋀z. z ∈ cball 0 1 ⟹ ¬(f z = 0 ∨ f z = 1)"
and "0 < t" "t < 1" "norm z ≤ t"
shows "norm(f z) ≤ exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
proof -
obtain h where holf: "h holomorphic_on cball 0 1"
and nh0: "norm (h 0) ≤ 1 + norm(2 * f 0 - 1) / 3"
and h:   "⋀z. z ∈ cball 0 1 ⟹ 2 * f z - 1 = cos(of_real pi * h z)"
proof (rule Schottky_lemma0 [of "λz. 2 * f z - 1" "cball 0 1" 0])
show "(λz. 2 * f z - 1) holomorphic_on cball 0 1"
by (intro holomorphic_intros holf)
show "contractible (cball (0::complex) 1)"
by (auto simp: convex_imp_contractible)
show "⋀z. z ∈ cball 0 1 ⟹ 2 * f z - 1 ≠ 1 ∧ 2 * f z - 1 ≠ - 1"
using not01 by force
qed auto
obtain g where holg: "g holomorphic_on cball 0 1"
and ng0:  "norm(g 0) ≤ 1 + norm(h 0) / 3"
and g:    "⋀z. z ∈ cball 0 1 ⟹ h z = cos(of_real pi * g z)"
proof (rule Schottky_lemma0 [OF holf convex_imp_contractible, of 0])
show "⋀z. z ∈ cball 0 1 ⟹ h z ≠ 1 ∧ h z ≠ - 1"
using h not01 by fastforce+
qed auto
have g0_2_f0: "norm(g 0) ≤ 2 + norm(f 0)"
proof -
have "cmod (2 * f 0 - 1) ≤ cmod (2 * f 0) + 1"
by (metis norm_one norm_triangle_ineq4)
also have "... ≤ 2 + cmod (f 0) * 3"
by simp
finally have "1 + norm(2 * f 0 - 1) / 3 ≤ (2 + norm(f 0) - 1) * 3"
using norm_ge_zero [of "2 * f 0 - 1"]
by linarith
with nh0 have "norm(h 0) ≤ (2 + norm(f 0) - 1) * 3"
by linarith
then have "1 + norm(h 0) / 3 ≤ 2 + norm(f 0)"
by simp
with ng0 show ?thesis
by auto
qed
have "z ∈ ball 0 1"
using assms by auto
have norm_g_12: "norm(g z - g 0) ≤ (12 * t) / (1 - t)"
proof -
obtain g' where g': "⋀x. x ∈ cball 0 1 ⟹ (g has_field_derivative g' x) (at x within cball 0 1)"
using holg [unfolded holomorphic_on_def field_differentiable_def] by metis
have int_g': "(g' has_contour_integral g z - g 0) (linepath 0 z)"
using contour_integral_primitive [OF g' valid_path_linepath, of 0 z]
using ‹z ∈ ball 0 1› segment_bound1 by fastforce
have "cmod (g' w) ≤ 12 / (1 - t)" if "w ∈ closed_segment 0 z" for w
proof -
have w: "w ∈ ball 0 1"
using segment_bound [OF that] ‹z ∈ ball 0 1› by simp
have ttt: "⋀z. z ∈ frontier (cball 0 1) ⟹ 1 - t ≤ dist w z"
using ‹norm z ≤ t› segment_bound1 [OF ‹w ∈ closed_segment 0 z›]
by (metis diff_left_mono dist_commute dist_complex_def norm_triangle_ineq2 order_trans)
have *: "⟦⋀b. (∃w ∈ T ∪ U. w ∈ ball b 1); ⋀x. x ∈ D ⟹ g x ∉ T ∪ U⟧ ⟹ ∄b. ball b 1 ⊆ g  D" for T U D
by force
have "∄b. ball b 1 ⊆ g  cball 0 1"
proof (rule *)
show "(∃w ∈ (⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) ∪
(⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)}). w ∈ ball b 1)" for b
proof -
obtain m where m: "m ∈ ℤ" "¦Re b - m¦ ≤ 1/2"
by (metis Ints_of_int abs_minus_commute of_int_round_abs_le)
show ?thesis
proof (cases "0::real" "Im b" rule: le_cases)
case le
then obtain n where "0 < n" and n: "¦Im b - ln (n + sqrt ((real n)⇧2 - 1)) / pi¦ < 1/2"
using Schottky_lemma2 [of "Im b"] by blast
have "dist b (Complex m (Im b)) ≤ 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 (Im b)) (Complex m (ln (n + sqrt ((real n)⇧2 - 1)) / pi)) < 1/2"
using n by (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq)
ultimately have "dist b (Complex m (ln (real n + sqrt ((real n)⇧2 - 1)) / pi)) < 1"
by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
with le m ‹0 < n› show ?thesis
apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)⇧2 - 1)) / pi)" in bexI)
apply (simp_all del: Complex_eq greaterThan_0)
by blast
next
case ge
then obtain n where "0 < n" and n: "¦- Im b - ln (real n + sqrt ((real n)⇧2 - 1)) / pi¦ < 1/2"
using Schottky_lemma2 [of "- Im b"] by auto
have "dist b (Complex m (Im b)) ≤ 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)⇧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)
ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)⇧2 - 1)) / pi)) < 1"
by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
with ge m ‹0 < n› show ?thesis
apply (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)⇧2 - 1)) / pi)" in bexI)
apply (simp_all del: Complex_eq greaterThan_0)
by blast
qed
qed
show "g v ∉ (⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) ∪
(⋃m ∈ Ints. ⋃n ∈ {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
if "v ∈ cball 0 1" for v
using not01 [OF that]
by (force simp: g [OF that, symmetric] h [OF that, symmetric] dest!: Schottky_lemma3 [of "g v"])
qed
then have 12: "(1 - t) * cmod (deriv g w) / 12 < 1"
using Bloch_general [OF holg _ ttt, of 1] w by force
have "g field_differentiable at w within cball 0 1"
using holg w by (simp add: holomorphic_on_def)
then have "g field_differentiable at w within ball 0 1"
using ball_subset_cball field_differentiable_within_subset by blast
with w have der_gw: "(g has_field_derivative deriv g w) (at w)"
by (simp add: field_differentiable_within_open [of _ "ball 0 1"] field_differentiable_derivI)
with DERIV_unique [OF der_gw] g' w have "deriv g w = g' w"
by (metis open_ball at_within_open ball_subset_cball has_field_derivative_subset subsetCE)
then show "cmod (g' w) ≤ 12 / (1 - t)"
using g' 12 ‹t < 1› by (simp add: field_simps)
qed
then have "cmod (g z - g 0) ≤ 12 / (1 - t) * cmod z"
using has_contour_integral_bound_linepath [OF int_g', of "12/(1 - t)"] assms
by simp
with ‹cmod z ≤ t› ‹t < 1› show ?thesis
qed
have fz: "f z = (1 + cos(of_real pi * h z)) / 2"
using h ‹z ∈ ball 0 1› by (auto simp: field_simps)
have "cmod (f z) ≤ exp (cmod (complex_of_real pi * h z))"
by (simp add: fz mult.commute norm_cos_plus1_le)
also have "... ≤ exp (pi * exp (pi * (2 + 2 * r + 12 * t / (1 - t))))"
have "cmod (g z - g 0) ≤ 12 * t / (1 - t)"
using norm_g_12 ‹t < 1› by (simp add: norm_mult)
then have "cmod (g z) - cmod (g 0) ≤ 12 * t / (1 - t)"
using norm_triangle_ineq2 order_trans by blast
then have *: "cmod (g z) ≤ 2 + 2 * r + 12 * t / (1 - t)"
using g0_2_f0 norm_ge_zero [of "f 0"] nof0
by linarith
have "cmod (h z) ≤ exp (cmod (complex_of_real pi * g z))"
using ‹z ∈ ball 0 1› by (simp add: g norm_cos_le)
also have "... ≤ exp (pi * (2 + 2 * r + 12 * t / (1 - t)))"
using ‹t < 1› nof0 * by (simp add: norm_mult)
finally show "cmod (h z) ≤ exp (pi * (2 + 2 * r + 12 * t / (1 - t)))" .
qed
finally show ?thesis .
qed

subsection‹The Little Picard Theorem›

lemma Landau_Picard:
obtains R
where "⋀z. 0 < R z"
"⋀f. ⟦f holomorphic_on cball 0 (R(f 0));
⋀z. norm z ≤ R(f 0) ⟹ f z ≠ 0 ∧ f z ≠ 1⟧ ⟹ norm(deriv f 0) < 1"
proof -
define R where "R ≡ λz. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
show ?thesis
proof
show Rpos: "⋀z. 0 < R z"
by (auto simp: R_def)
show "norm(deriv f 0) < 1"
if holf: "f holomorphic_on cball 0 (R(f 0))"
and Rf:  "⋀z. norm z ≤ R(f 0) ⟹ f z ≠ 0 ∧ f z ≠ 1" for f
proof -
let ?r = "R(f 0)"
define g where "g ≡ f ∘ (λz. of_real ?r * z)"
have "0 < ?r"
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)
have *: "norm(g z) ≤ exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12 * t / (1 - t))))"
if "0 < t" "t < 1" "norm z ≤ t" for t z
proof (rule Schottky [OF holg])
show "cmod (g 0) ≤ cmod (f 0)"
show "⋀z. z ∈ cball 0 1 ⟹ ¬ (g z = 0 ∨ 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)"
by (rule holomorphic_on_subset [OF holg]) auto
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) ≤ R (f 0) / 3" if "cmod (0 - z) = 1/2" for z
proof -
have "norm(g z) ≤ exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12)))"
using * [of "1/2"] that by simp
also have "... = ?r / 3"
finally show ?thesis .
qed
then have cmod_g'_le: "cmod (deriv g 0) * 3 ≤ R (f 0) * 2"
using Cauchy_inequality [OF C1 C2 _ C3, of 1] by simp
have holf': "f holomorphic_on ball 0 (R(f 0))"
by (rule holomorphic_on_subset [OF holf]) auto
then have fd0: "f field_differentiable at 0"
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)
by (metis 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
qed
qed

lemma little_Picard_01:
assumes holf: "f holomorphic_on UNIV" and f01: "⋀z. f z ≠ 0 ∧ f z ≠ 1"
obtains c where "f = (λx. c)"
proof -
obtain R
where Rpos: "⋀z. 0 < R z"
and R:    "⋀h. ⟦h holomorphic_on cball 0 (R(h 0));
⋀z. norm z ≤ R(h 0) ⟹ h z ≠ 0 ∧ h z ≠ 1⟧ ⟹ norm(deriv h 0) < 1"
using Landau_Picard by metis
have contf: "continuous_on UNIV f"
show ?thesis
proof (cases "∀x. deriv f x = 0")
case True
obtain c where "⋀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
then show ?thesis
using that by auto
next
case False
then obtain w where w: "deriv f w ≠ 0" by auto
define fw where "fw ≡ (f ∘ (λz. w + z / deriv f w))"
have norm_let1: "norm(deriv fw 0) < 1"
proof (rule R)
show "fw holomorphic_on cball 0 (R (fw 0))"
unfolding fw_def
by (intro holomorphic_intros holomorphic_on_compose w holomorphic_on_subset [OF holf] subset_UNIV)
show "fw z ≠ 0 ∧ fw z ≠ 1" if "cmod z ≤ R (fw 0)" for z
using f01 by (simp add: fw_def)
qed
have "(fw has_field_derivative deriv f w * inverse (deriv f w)) (at 0)"
apply (rule DERIV_chain)
using holf holomorphic_derivI apply force
apply (intro derivative_eq_intros w)
apply (auto simp: field_simps)
done
then show ?thesis
using norm_let1 w by (simp add: DERIV_imp_deriv)
qed
qed

theorem little_Picard:
assumes holf: "f holomorphic_on UNIV"
and "a ≠ b" "range f ∩ {a,b} = {}"
obtains c where "f = (λx. c)"
proof -
let ?g = "λx. 1/(b - a)*(f x - b) + 1"
obtain c where "?g = (λx. c)"
proof (rule little_Picard_01)
show "?g holomorphic_on UNIV"
by (intro holomorphic_intros holf)
show "⋀z. ?g z ≠ 0 ∧ ?g z ≠ 1"
using assms by (auto simp: field_simps)
qed auto
then have "?g x = c" for x
by meson
then have "f x = c * (b-a) + a" for x
using assms by (auto simp: field_simps)
then show ?thesis
using that by blast
qed

text‹A couple of little applications of Little Picard›

lemma holomorphic_periodic_fixpoint:
assumes holf: "f holomorphic_on UNIV"
and "p ≠ 0" and per: "⋀z. f(z + p) = f z"
obtains x where "f x = x"
proof -
have False if non: "⋀x. f x ≠ x"
proof -
obtain c where "(λz. f z - z) = (λz. c)"
proof (rule little_Picard)
show "(λz. f z - z) holomorphic_on UNIV"
show "range (λz. f z - z) ∩ {p,0} = {}"
using assms non by auto (metis add.commute diff_eq_eq)
qed (auto simp: assms)
with per show False
qed
then show ?thesis
using that by blast
qed

lemma holomorphic_involution_point:
assumes holfU: "f holomorphic_on UNIV" and non: "⋀a. f ≠ (λx. a + x)"
obtains x where "f(f x) = x"
proof -
{ assume non_ff [simp]: "⋀x. f(f x) ≠ x"
then have non_fp [simp]: "f z ≠ z" for z
by metis
have holf: "f holomorphic_on X" for X
using assms holomorphic_on_subset by blast
obtain c where c: "(λx. (f(f x) - x)/(f x - x)) = (λx. c)"
proof (rule little_Picard_01)
show "(λ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
qed auto
then obtain "c ≠ 0" "c ≠ 1"
by (metis (no_types, hide_lams) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
have eq: "f(f x) - c * f x = x*(1 - c)" for x
using fun_cong [OF c, of x] by (simp add: field_simps)
have df_times_dff: "deriv f z * (deriv f (f z) - c) = 1 * (1 - c)" for z
proof (rule DERIV_unique)
show "((λ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
show "((λx. f (f x) - c * f x) has_field_derivative 1 * (1 - c)) (at z)"
qed
{ fix z::complex
obtain k where k: "deriv f ∘ f = (λx. k)"
proof (rule little_Picard)
show "(deriv f ∘ f) holomorphic_on UNIV"
by (meson holfU holomorphic_deriv holomorphic_on_compose holomorphic_on_subset open_UNIV subset_UNIV)
obtain "deriv f (f x) ≠ 0" "deriv f (f x) ≠ c"  for x
using df_times_dff ‹c ≠ 1› eq_iff_diff_eq_0
by (metis lambda_one mult_zero_left mult_zero_right)
then show "range (deriv f ∘ f) ∩ {0,c} = {}"
by force
qed (use ‹c ≠ 0› in auto)
have "¬ f constant_on UNIV"
by (meson UNIV_I non_ff constant_on_def)
with holf open_mapping_thm have "open(range f)"
by blast
obtain l where l: "⋀x. f x - k * x = l"
proof (rule DERIV_zero_connected_constant [of UNIV "{}" "λx. f x - k * x"], simp_all)
have "deriv f w - k = 0" for w
proof (rule analytic_continuation [OF _ open_UNIV connected_UNIV subset_UNIV, of "λz. deriv f z - k" "f z" "range f" w])
show "(λz. deriv f z - k) holomorphic_on UNIV"
by (intro holomorphic_intros holf open_UNIV)
show "f z islimpt range f"
by (metis (no_types, lifting) IntI UNIV_I ‹open (range f)› image_eqI inf.absorb_iff2 inf_aci(1) islimpt_UNIV islimpt_eq_acc_point open_Int top_greatest)
show "⋀z. z ∈ range f ⟹ deriv f z - k = 0"
by (metis comp_def diff_self image_iff k)
qed auto
moreover
have "((λx. f x - k * x) has_field_derivative deriv f x - k) (at x)" for x
by (metis DERIV_cmult_Id Deriv.field_differentiable_diff UNIV_I field_differentiable_derivI holf holomorphic_on_def)
ultimately
show "∀x. ((λx. f x - k * x) has_field_derivative 0) (at x)"
by auto
show "continuous_on UNIV (λx. f x - k * x)"
by (simp add: continuous_on_diff holf holomorphic_on_imp_continuous_on)
qed (auto simp: connected_UNIV)
have False
proof (cases "k=1")
case True
then have "∃x. k * x + l ≠ a + x" for a
using l non [of a] ext [of f "(+) a"]
with True show ?thesis by auto
next
case False
have "⋀x. (1 - k) * x ≠ f 0"
using l [of 0] apply (simp add: algebra_simps)
by (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
}
}
then show thesis
using that by blast
qed

subsection‹The ArzelÃ --Ascoli theorem›

lemma subsequence_diagonalization_lemma:
fixes P :: "nat ⇒ (nat ⇒ 'a) ⇒ bool"
assumes sub: "⋀i r. ∃k. strict_mono (k :: nat ⇒ nat) ∧ P i (r ∘ k)"
and P_P:  "⋀i r::nat ⇒ 'a. ⋀k1 k2 N.
⟦P i (r ∘ k1); ⋀j. N ≤ j ⟹ ∃j'. j ≤ j' ∧ k2 j = k1 j'⟧ ⟹ P i (r ∘ k2)"
obtains k where "strict_mono (k :: nat ⇒ nat)" "⋀i. P i (r ∘ k)"
proof -
obtain kk where "⋀i r. strict_mono (kk i r :: nat ⇒ nat) ∧ P i (r ∘ (kk i r))"
using sub by metis
then have sub_kk: "⋀i r. strict_mono (kk i r)" and P_kk: "⋀i r. P i (r ∘ (kk i r))"
by auto
define rr where "rr ≡ rec_nat (kk 0 r) (λn x. x ∘ kk (Suc n) (r ∘ x))"
then have [simp]: "rr 0 = kk 0 r" "⋀n. rr(Suc n) = rr n ∘ kk (Suc n) (r ∘ rr n)"
by auto
show thesis
proof
have sub_rr: "strict_mono (rr i)" for i
using sub_kk  by (induction i) (auto simp: strict_mono_def o_def)
have P_rr: "P i (r ∘ rr i)" for i
using P_kk  by (induction i) (auto simp: o_def)
have "i ≤ i+d ⟹ rr i n ≤ rr (i+d) n" for d i n
proof (induction d)
case 0 then show ?case
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
qed
then have "⋀i j n. i ≤ j ⟹ rr i n ≤ rr j n"
show "strict_mono (λn. rr n n)"
by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr)
have "∃j. i ≤ j ∧ 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)
then have "⋀m n i. n ≤ m ⟹ ∃j. i ≤ j ∧ rr m i = rr n j"
then show "P i (r ∘ (λn. rr n n))" for i
by (meson P_rr P_P)
qed
qed

lemma function_convergent_subsequence:
fixes f :: "[nat,'a] ⇒ 'b::{real_normed_vector,heine_borel}"
assumes "countable S" and M: "⋀n::nat. ⋀x. x ∈ S ⟹ norm(f n x) ≤ M"
obtains k where "strict_mono (k::nat⇒nat)" "⋀x. x ∈ S ⟹ ∃l. (λn. f (k n) x) ⇢ l"
proof (cases "S = {}")
case True
then show ?thesis
using strict_mono_id that by fastforce
next
case False
with ‹countable S› obtain σ :: "nat ⇒ 'a" where σ: "S = range σ"
using uncountable_def by blast
obtain k where "strict_mono k" and k: "⋀i. ∃l. (λn. (f ∘ k) n (σ i)) ⇢ l"
proof (rule subsequence_diagonalization_lemma
[of "λi r. ∃l. ((λn. (f ∘ r) n (σ i)) ⤏ l) sequentially" id])
show "∃k::nat⇒nat. strict_mono k ∧ (∃l. (λn. (f ∘ (r ∘ k)) n (σ i)) ⇢ l)" for i r
proof -
have "f (r n) (σ i) ∈ cball 0 M" for n
then show ?thesis
using compact_def [of "cball (0::'b) M"] apply simp
apply (drule_tac x="(λn. f (r n) (σ i))" in spec)
apply (force simp: o_def)
done
qed
show "⋀i r k1 k2 N.
⟦∃l. (λn. (f ∘ (r ∘ k1)) n (σ i)) ⇢ l; ⋀j. N ≤ j ⟹ ∃j'≥j. k2 j = k1 j'⟧
⟹ ∃l. (λn. (f ∘ (r ∘ k2)) n (σ i)) ⇢ l"
apply (erule ex_forward all_forward imp_forward)+
apply auto
by (metis (no_types, hide_lams) le_cases order_trans)
qed auto
with σ that show ?thesis
by force
qed

theorem Arzela_Ascoli:
fixes ℱ :: "[nat,'a::euclidean_space] ⇒ 'b::{real_normed_vector,heine_borel}"
assumes "compact S"
and M: "⋀n x. x ∈ S ⟹ norm(ℱ n x) ≤ M"
and equicont:
"⋀x e. ⟦x ∈ S; 0 < e⟧
⟹ ∃d. 0 < d ∧ (∀n y. y ∈ S ∧ norm(x - y) < d ⟶ norm(ℱ n x - ℱ n y) < e)"
obtains g k where "continuous_on S g" "strict_mono (k :: nat ⇒ nat)"
"⋀e. 0 < e ⟹ ∃N. ∀n x. n ≥ N ∧ x ∈ S ⟶ norm(ℱ(k n) x - g x) < e"
proof -
have UEQ: "⋀e. 0 < e ⟹ ∃d. 0 < d ∧ (∀n. ∀x ∈ S. ∀x' ∈ S. dist x' x < d ⟶ dist (ℱ n x') (ℱ n x) < e)"
apply (rule compact_uniformly_equicontinuous [OF ‹compact S›, of "range ℱ"])
using equicont by (force simp: dist_commute dist_norm)+
have "continuous_on S g"
if "⋀e. 0 < e ⟹ ∃N. ∀n x. n ≥ N ∧ x ∈ S ⟶ norm(ℱ(r n) x - g x) < e"
for g:: "'a ⇒ 'b" and r :: "nat ⇒ nat"
proof (rule uniform_limit_theorem [of _ "ℱ ∘ r"])
show "∀⇩F n in sequentially. continuous_on S ((ℱ ∘ r) n)"
apply (rule_tac x=0 in exI)
using UEQ apply (force simp: continuous_on_iff)
done
show "uniform_limit S (ℱ ∘ r) g sequentially"
by (metis dist_norm that)
qed auto
moreover
obtain R where "countable R" "R ⊆ S" and SR: "S ⊆ closure R"
by (metis separable that)
obtain k where "strict_mono k" and k: "⋀x. x ∈ R ⟹ ∃l. (λn. ℱ (k n) x) ⇢ l"
apply (rule function_convergent_subsequence [OF ‹countable R› M])
using ‹R ⊆ S› apply force+
done
then have Cauchy: "Cauchy ((λn. ℱ (k n) x))" if "x ∈ R" for x
using convergent_eq_Cauchy that by blast
have "∃N. ∀m n x. N ≤ m ∧ N ≤ n ∧ x ∈ S ⟶ dist ((ℱ ∘ k) m x) ((ℱ ∘ k) n x) < e"
if "0 < e" for e
proof -
obtain d where "0 < d"
and d: "⋀n. ∀x ∈ S. ∀x' ∈ S. dist x' x < d ⟶ dist (ℱ n x') (ℱ n x) < e/3"
by (metis UEQ ‹0 < e› divide_pos_pos zero_less_numeral)
obtain T where "T ⊆ R" and "finite T" and T: "S ⊆ (⋃c∈T. ball c d)"
proof (rule compactE_image [OF  ‹compact S›, of R "(λx. ball x d)"])
have "closure R ⊆ (⋃c∈R. ball c d)"
apply clarsimp
using ‹0 < d› closure_approachable by blast
with SR show "S ⊆ (⋃c∈R. ball c d)"
by auto
qed auto
have "∃M. ∀m≥M. ∀n≥M. dist (ℱ (k m) x) (ℱ (k n) x) < e/3" if "x ∈ R" for x
using Cauchy ‹0 < e› that unfolding Cauchy_def
by (metis less_divide_eq_numeral1(1) mult_zero_left)
then obtain MF where MF: "⋀x m n. ⟦x ∈ R; m ≥ MF x; n ≥ MF x⟧ ⟹ norm (ℱ (k m) x - ℱ (k n) x) < e/3"
using dist_norm by metis
have "dist ((ℱ ∘ k) m x) ((ℱ ∘ k) n x) < e"
if m: "Max (MF  T) ≤ m" and n: "Max (MF  T) ≤ n" "x ∈ S" for m n x
proof -
obtain t where "t ∈ T" and t: "x ∈ ball t d"
using ‹x ∈ S› T by auto
have "norm(ℱ (k m) t - ℱ (k m) x) < e / 3"
by (metis ‹R ⊆ S› ‹T ⊆ R› ‹t ∈ T› d dist_norm mem_ball subset_iff t ‹x ∈ S›)
moreover
have "norm(ℱ (k n) t - ℱ (k n) x) < e / 3"
by (metis ‹R ⊆ S› ‹T ⊆ R› ‹t ∈ T› subsetD d dist_norm mem_ball t ‹x ∈ S›)
moreover
have "norm(ℱ (k m) t - ℱ (k n) t) < e / 3"
proof (rule MF)
show "t ∈ R"
using ‹T ⊆ R› ‹t ∈ T› by blast
show "MF t ≤ m" "MF t ≤ n"
by (meson Max_ge ‹finite T› ‹t ∈ T› finite_imageI imageI le_trans m n)+
qed
ultimately
show ?thesis
unfolding dist_norm [symmetric] o_def
by (metis dist_triangle_third dist_commute)
qed
then show ?thesis
by force
qed
then have "∃g. ∀e>0. ∃N. ∀n≥N. ∀x ∈ S. norm(ℱ(k n) x - g x) < e"
using uniformly_convergent_eq_cauchy [of "λx. x ∈ S" "ℱ ∘ k"]
by meson
ultimately show thesis
by (metis that ‹strict_mono k›)
qed

subsubsection‹Montel's theorem›

text‹a sequence of holomorphic functions uniformly bounded
on compact subsets of an open set S has a subsequence that converges to a
holomorphic function, and converges \emph{uniformly} on compact subsets of S.›

theorem Montel:
fixes ℱ :: "[nat,complex] ⇒ complex"
assumes "open S"
and ℋ: "⋀h. h ∈ ℋ ⟹ h holomorphic_on S"
and bounded: "⋀K. ⟦compact K; K ⊆ S⟧ ⟹ ∃B. ∀h ∈ ℋ. ∀ z ∈ K. norm(h z) ≤ B"
and rng_f: "range ℱ ⊆ ℋ"
obtains g r
where "g holomorphic_on S" "strict_mono (r :: nat ⇒ nat)"
"⋀x. x ∈ S ⟹ ((λn. ℱ (r n) x) ⤏ g x) sequentially"
"⋀K. ⟦compact K; K ⊆ S⟧ ⟹ uniform_limit K (ℱ ∘ r) g sequentially"
proof -
obtain K where comK: "⋀n. compact(K n)" and KS: "⋀n::nat. K n ⊆ S"
and subK: "⋀X. ⟦compact X; X ⊆ S⟧ ⟹ ∃N. ∀n≥N. X ⊆ K n"
using open_Union_compact_subsets [OF ‹open S›] by metis
then have "⋀i. ∃B. ∀h ∈ ℋ. ∀ z ∈ K i. norm(h z) ≤ B"
then obtain B where B: "⋀i h z. ⟦h ∈ ℋ; z ∈ K i⟧ ⟹ norm(h z) ≤ B i"
by metis
have *: "∃r g. strict_mono (r::nat⇒nat) ∧ (∀e > 0. ∃N. ∀n≥N. ∀x ∈ K i. norm((ℱ ∘ r) n x - g x) < e)"
if "⋀n. ℱ n ∈ ℋ" for ℱ i
proof -
obtain g k where "continuous_on (K i) g" "strict_mono (k::nat⇒nat)"
"⋀e. 0 < e ⟹ ∃N. ∀n≥N. ∀x ∈ K i. norm(ℱ(k n) x - g x) < e"
proof (rule Arzela_Ascoli [of "K i" "ℱ" "B i"])
show "∃d>0. ∀n y. y ∈ K i ∧ cmod (z - y) < d ⟶ cmod (ℱ n z - ℱ n y) < e"
if z: "z ∈ K i" and "0 < e" for z e
proof -
obtain r where "0 < r" and r: "cball z r ⊆ S"
using z KS [of i] ‹open S› by (force simp: open_contains_cball)
have "cball z (2 / 3 * r) ⊆ cball z r"
using ‹0 < r› by (simp add: cball_subset_cball_iff)
then have z23S: "cball z (2 / 3 * r) ⊆ S"
using r by blast
obtain M where "0 < M" and M: "⋀n w. dist z w ≤ 2/3 * r ⟹ norm(ℱ n w) ≤ M"
proof -
obtain N where N: "∀n≥N. cball z (2/3 * r) ⊆ K n"
using subK compact_cball [of z "(2 / 3 * r)"] z23S by force
have "cmod (ℱ n w) ≤ ¦B N¦ + 1" if "dist z w ≤ 2 / 3 * r" for n w
proof -
have "w ∈ K N"
using N mem_cball that by blast
then have "cmod (ℱ n w) ≤ B N"
using B ‹⋀n. ℱ n ∈ ℋ› by blast
also have "... ≤ ¦B N¦ + 1"
by simp
finally show ?thesis .
qed
then show ?thesis
by (rule_tac M="¦B N¦ + 1" in that) auto
qed
have "cmod (ℱ n z - ℱ n y) < e"
if "y ∈ K i" and y_near_z: "cmod (z - y) < r/3" "cmod (z - y) < e * r / (6 * M)"
for n y
proof -
have "((λw. ℱ n w / (w - ξ)) has_contour_integral
(2 * pi) * 𝗂 * winding_number (circlepath z (2 / 3 * r)) ξ * ℱ n ξ)
(circlepath z (2 / 3 * r))"
if "dist ξ z < (2 / 3 * r)" for ξ
proof (rule Cauchy_integral_formula_convex_simple)
have "ℱ n holomorphic_on S"
by (simp add: ℋ ‹⋀n. ℱ n ∈ ℋ›)
with z23S show "ℱ n holomorphic_on cball z (2 / 3 * r)"
using holomorphic_on_subset by blast
qed (use that ‹0 < r› in ‹auto simp: dist_commute›)
then have *: "((λw. ℱ n w / (w - ξ)) has_contour_integral (2 * pi) * 𝗂 * ℱ n ξ)
(circlepath z (2 / 3 * r))"
if "dist ξ z < (2 / 3 * r)" for ξ
using that by (simp add: winding_number_circlepath dist_norm)
have y: "((λw. ℱ n w / (w - y)) has_contour_integral (2 * pi) * 𝗂 * ℱ n y)
(circlepath z (2 / 3 * r))"
apply (rule *)
using that ‹0 < r› by (simp only: dist_norm norm_minus_commute)
have z: "((λw. ℱ n w / (w - z)) has_contour_integral (2 * pi) * 𝗂 * ℱ n z)
(circlepath z (2 / 3 * r))"
apply (rule *)
using ‹0 < r› by simp
have le_er: "cmod (ℱ n x / (x - y) - ℱ n x / (x - z)) ≤ e / r"
if "cmod (x - z) = r/3 + r/3" for x
proof -
have "~ (cmod (x - y) < r/3)"
using y_near_z(1) that ‹M > 0› ‹r > 0›
by (metis (full_types) norm_diff_triangle_less norm_minus_commute order_less_irrefl)
then have r4_le_xy: "r/4 ≤ cmod (x - y)"
using ‹r > 0› by simp
then have neq: "x ≠ y" "x ≠ z"
using that ‹r > 0› by (auto simp: divide_simps norm_minus_commute)
have leM: "cmod (ℱ n x) ≤ M"
by (simp add: M dist_commute dist_norm that)
have "cmod (ℱ n x / (x - y) - ℱ n x / (x - z)) = cmod (ℱ n x) * cmod (1 / (x - y) - 1 / (x - z))"
by (metis (no_types, lifting) divide_inverse mult.left_neutral norm_mult right_diff_distrib')
also have "... = cmod (ℱ n x) * cmod ((y - z) / ((x - y) * (x - z)))"
using neq by (simp add: divide_simps)
also have "... = cmod (ℱ n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
by (simp add: norm_mult norm_divide that)
also have "... ≤ M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
apply (rule mult_mono)
apply (rule leM)
using ‹r > 0› ‹M > 0› 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) ‹M > 0› ‹r > 0› neq
apply (simp add: field_simps mult_less_0_iff norm_minus_commute)
done
also have "... ≤ e/r"
using ‹e > 0› ‹r > 0› r4_le_xy by (simp add: divide_simps)
finally show ?thesis by simp
qed
have "(2 * pi) * cmod (ℱ n y - ℱ n z) = cmod ((2 * pi) * 𝗂 * ℱ n y - (2 * pi) * 𝗂 * ℱ n z)"
by (simp add: right_diff_distrib [symmetric] norm_mult)
also have "cmod ((2 * pi) * 𝗂 * ℱ n y - (2 * pi) * 𝗂 * ℱ n z) ≤ 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 ‹e > 0› ‹r > 0› le_er by auto
also have "... = (2 * pi) * e * ((2 / 3))"
using ‹r > 0› by (simp add: divide_simps)
finally have "cmod (ℱ n y - ℱ n z) ≤ e * (2 / 3)"
by simp
also have "... < e"
using ‹e > 0› by simp
finally show ?thesis by (simp add: norm_minus_commute)
qed
then show ?thesis
apply (rule_tac x="min (r/3) ((e * r)/(6 * M))" in exI)
using ‹0 < e› ‹0 < r› ‹0 < M› by simp
qed
show "⋀n x.  x ∈ K i ⟹ cmod (ℱ n x) ≤ B i"
using B ‹⋀n. ℱ n ∈ ℋ› by blast
qed (use comK in ‹fastforce+›)
then show ?thesis
by fastforce
qed
have "∃k g. strict_mono (k::nat⇒nat) ∧ (∀e > 0. ∃N. ∀n≥N. ∀x ∈ K i. norm((ℱ ∘ r ∘ k) n x - g x) < e)"
for i r
apply (rule *)
using rng_f by auto
then have **: "⋀i r. ∃k. strict_mono (k::nat⇒nat) ∧ (∃g. ∀e>0. ∃N. ∀n≥N. ∀x ∈ K i. norm((ℱ ∘ (r ∘ k)) n x - g x) < e)"
by (force simp: o_assoc)
obtain k :: "nat ⇒ nat" where "strict_mono k"
and "⋀i. ∃g. ∀e>0. ∃N. ∀n≥N. ∀x∈K i. cmod ((ℱ ∘ (id ∘ k)) n x - g x) < e"
apply (rule subsequence_diagonalization_lemma [OF **, of id])
apply (erule ex_forward all_forward imp_forward)+
apply auto
apply (rule_tac x="max N Na" in exI, fastforce+)
done
then have lt_e: "⋀i. ∃g. ∀e>0. ∃N. ∀n≥N. ∀x∈K i. cmod ((ℱ ∘ k) n x - g x) < e"
by simp
have "∃l. ∀e>0. ∃N. ∀n≥N. norm(ℱ (k n) z - l) < e" if "z ∈ S" for z
proof -
obtain G where G: "⋀i e. e > 0 ⟹ ∃M. ∀n≥M. ∀x∈K i. cmod ((ℱ ∘ k) n x - G i x) < e"
using lt_e by metis
obtain N where "⋀n. n ≥ N ⟹ z ∈ K n"
using subK [of "{z}"] that ‹z ∈ S› by auto
moreover have "⋀e. e > 0 ⟹ ∃M. ∀n≥M. ∀x∈K N. cmod ((ℱ ∘ k) n x - G N x) < e"
using G by auto
ultimately show ?thesis
by (metis comp_apply order_refl)
qed
then obtain g where g: "⋀z e. ⟦z ∈ S; e > 0⟧ ⟹ ∃N. ∀n≥N. norm(ℱ (k n) z - g z) < e"
by metis
show ?thesis
proof
show g_lim: "⋀x. x ∈ S ⟹ (λn. ℱ (k n) x) ⇢ g x"
by (simp add: lim_sequentially g dist_norm)
have dg_le_e: "∃N. ∀n≥N. ∀x∈T. cmod (ℱ (k n) x - g x) < e"
if T: "compact T" "T ⊆ S" and "0 < e" for T e
proof -
obtain N where N: "⋀n. n ≥ N ⟹ T ⊆ K n"
using subK [OF T] by blast
obtain h where h: "⋀e. e>0 ⟹ ∃M. ∀n≥M. ∀x∈K N. cmod ((ℱ ∘ k) n x - h x) < e"
using lt_e by blast
have geq: "g w = h w" if "w ∈ T" for w
apply (rule LIMSEQ_unique [of "λn. ℱ(k n) w"])
using ‹T ⊆ S› g_lim that apply blast
using h N that by (force simp: lim_sequentially dist_norm)
show ?thesis
using T h N ‹0 < e› by (fastforce simp add: geq)
qed
then show "⋀K. ⟦compact K; K ⊆ S⟧
⟹ uniform_limit K (ℱ ∘ k) g sequentially"
by (simp add: uniform_limit_iff dist_norm eventually_sequentially)
show "g holomorphic_on S"
proof (rule holomorphic_uniform_sequence [OF ‹open S› ℋ])
show "⋀n. (ℱ ∘ k) n ∈ ℋ"
show "∃d>0. cball z d ⊆ S ∧ uniform_limit (cball z d) (λn. (ℱ ∘ k) n) g sequentially"
if "z ∈ S" for z
proof -
obtain d where d: "d>0" "cball z d ⊆ S"
using ‹open S› ‹z ∈ S› open_contains_cball by blast
then have "uniform_limit (cball z d) (ℱ ∘ k) g sequentially"
using dg_le_e compact_cball by (auto simp: uniform_limit_iff eventually_sequentially dist_norm)
with d show ?thesis by blast
qed
qed
qed (auto simp: ‹strict_mono k›)
qed

subsection‹Some simple but useful cases of Hurwitz's theorem›

proposition Hurwitz_no_zeros:
assumes S: "open S" "connected S"
and holf: "⋀n::nat. ℱ n holomorphic_on S"
and holg: "g holomorphic_on S"
and ul_g: "⋀K. ⟦compact K; K ⊆ S⟧ ⟹ uniform_limit K ℱ g sequentially"
and nonconst: "~ g constant_on S"
and nz: "⋀n z. z ∈ S ⟹ ℱ n z ≠ 0"
and "z0 ∈ S"
shows "g z0 ≠ 0"
proof
assume g0: "g z0 = 0"
obtain h r m
where "0 < m" "0 < r" and subS: "ball z0 r ⊆ S"
and holh: "h holomorphic_on ball z0 r"
and geq:  "⋀w. w ∈ ball z0 r ⟹ g w = (w - z0)^m * h w"
and hnz:  "⋀w. w ∈ ball z0 r ⟹ h w ≠ 0"
by (blast intro: holomorphic_factor_zero_nonconstant [OF holg S ‹z0 ∈ S› g0 nonconst])
then have holf0: "ℱ n holomorphic_on ball z0 r" for n
by (meson holf holomorphic_on_subset)
have *: "((λz. deriv (ℱ n) z / ℱ n z) has_contour_integral 0) (circlepath z0 (r/2))" for n
proof (rule Cauchy_theorem_disc_simple [of _ z0 r])
show "(λz. deriv (ℱ n) z / ℱ n z) holomorphic_on ball z0 r"
apply (intro holomorphic_intros holomorphic_deriv holf holf0 open_ball nz)
using ‹ball z0 r ⊆ S› by blast
qed (use ‹0 < r› in auto)
have hol_dg: "deriv g holomorphic_on S"
by (simp add: ‹open S› 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 ‹0 < r› subS by 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 ∘ g)"
apply (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg])
using ‹0 < r› subS by auto
then have "compact ((cmod ∘ g)  sphere z0 (r/2))"
by (rule compact_continuous_image [OF _ compact_sphere])
moreover have "(cmod ∘ g)  sphere z0 (r/2) ≠ {}"
using ‹0 < r› by auto
ultimately obtain b where b: "b ∈ (cmod ∘ g)  sphere z0 (r/2)"
"⋀t. t ∈ (cmod ∘ g)  sphere z0 (r/2) ⟹ b ≤ t"
using compact_attains_inf [of "(norm ∘ g)  (sphere z0 (r/2))"] by blast
have "(λn. contour_integral (circlepath z0 (r/2)) (λz. deriv (ℱ n) z / ℱ n z)) ⇢
contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z)"
proof (rule contour_integral_uniform_limit_circlepath)
show "∀⇩F n in sequentially. (λz. deriv (ℱ n) z / ℱ n z) contour_integrable_on circlepath z0 (r/2)"
using * contour_integrable_on_def eventually_sequentiallyI by meson
show "uniform_limit (sphere z0 (r/2)) (λn z. deriv (ℱ n) z / ℱ n z) (λz. deriv g z / g z) sequentially"
proof (rule uniform_lim_divide [OF _ _ bo_dg])
show "uniform_limit (sphere z0 (r/2)) (λa. deriv (ℱ a)) (deriv g) sequentially"
proof (rule uniform_limitI)
fix e::real
assume "0 < e"
have *: "dist (deriv (ℱ n) w) (deriv g w) < e"
if e8: "⋀x. dist z0 x ≤ 3 * r / 4 ⟹ dist (ℱ n x) (g x) * 8 < r * e"
and w: "dist w z0 = r/2"  for n w
proof -
have "ball w (r/4) ⊆ ball z0 r"  "cball w (r/4) ⊆ ball z0 r"
using ‹0 < r› by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff w)
with subS have wr4_sub: "ball w (r/4) ⊆ S" "cball w (r/4) ⊆ S" by force+
moreover
have "(λz. ℱ n z - g z) holomorphic_on S"
by (intro holomorphic_intros holf holg)
ultimately have hol: "(λz. ℱ n z - g z) holomorphic_on ball w (r/4)"
and cont: "continuous_on (cball w (r / 4)) (λz. ℱ n z - g z)"
using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+
have "w ∈ S"
using ‹0 < r› wr4_sub by auto
have "⋀y. dist w y < r / 4 ⟹ dist z0 y ≤ 3 * r / 4"
apply (rule dist_triangle_le [where z=w])
using w by (simp add: dist_commute)
with e8 have in_ball: "⋀y. y ∈ ball w (r/4) ⟹ ℱ n y - g y ∈ ball 0 (r/4 * e/2)"
have "ℱ n field_differentiable at w"
by (metis holomorphic_on_imp_differentiable_at ‹w ∈ S› holf ‹open S›)
moreover
have "g field_differentiable at w"
using ‹w ∈ S› ‹open S› holg holomorphic_on_imp_differentiable_at by auto
moreover
have "cmod (deriv (λw. ℱ n w - g w) w) * 2 ≤ e"
apply (rule Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1, simplified])
using ‹r > 0› by auto
ultimately have "dist (deriv (ℱ n) w) (deriv g w) ≤ e/2"
then show ?thesis
using ‹e > 0› by auto
qed
have "cball z0 (3 * r / 4) ⊆ ball z0 r"
by (simp add: cball_subset_ball_iff ‹0 < r›)
with subS have "uniform_limit (cball z0 (3 * r/4)) ℱ g sequentially"
by (force intro: ul_g)
then have "∀⇩F n in sequentially. ∀x∈cball z0 (3 * r / 4). dist (ℱ n x) (g x) < r / 4 * e / 2"
using ‹0 < e› ‹0 < r› by (force simp: intro!: uniform_limitD)
then show "∀⇩F n in sequentially. ∀x ∈ sphere z0 (r/2). dist (deriv (ℱ n) x) (deriv g x) < e"
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)) ℱ g sequentially"
proof (rule uniform_limitI)
fix e::real
assume "0 < e"
have "sphere z0 (r/2) ⊆ ball z0 r"
using ‹0 < r› by auto
with subS have "uniform_limit (sphere z0 (r/2)) ℱ g sequentially"
by (force intro: ul_g)
then show "∀⇩F n in sequentially. ∀x ∈ sphere z0 (r/2). dist (ℱ n x) (g x) < e"
apply (rule uniform_limitD)
using ‹0 < e› by force
qed
show "b > 0" "⋀x. x ∈ sphere z0 (r/2) ⟹ b ≤ cmod (g x)"
using b ‹0 < r› by (fastforce simp: geq hnz)+
qed
qed (use ‹0 < r› in auto)
then have "(λn. 0) ⇢ contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z)"
by (simp add: contour_integral_unique [OF *])
then have "contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z) = 0"
moreover
have "contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z) =
contour_integral (circlepath z0 (r/2)) (λz. m / (z - z0) + deriv h z / h z)"
proof (rule contour_integral_eq, use ‹0 < r› in simp)
fix w
assume w: "dist z0 w * 2 = r"
then have w_inb: "w ∈ ball z0 r"
using ‹0 < r› by auto
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 ≠ z0"
proof -
have "((λ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 ‹m > 0› ‹0 < r› apply (simp add: divide_simps distrib_right)
apply (metis Suc_pred mult.commute power_Suc)
done
then show ?thesis
apply (rule DERIV_imp_deriv [OF DERIV_transform_within_open [where S = "ball z0 r"]])
using that ‹m > 0› ‹0 < r›
done
qed
with ‹0 < r› ‹0 < m› w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w"
by (auto simp: geq divide_simps hnz)
qed
moreover
have "contour_integral (circlepath z0 (r/2)) (λz. m / (z - z0) + deriv h z / h z) =
2 * of_real pi * 𝗂 * m + 0"
show "((λx. m / (x - z0)) has_contour_integral 2 * of_real pi * 𝗂 * m) (circlepath z0 (r/2))"
by (force simp: ‹0 < r› intro: Cauchy_integral_circlepath_simple)
show "((λ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 ‹0 < r›
apply force+
done
qed
ultimately show False using ‹0 < m› by auto
qed

corollary Hurwitz_injective:
assumes S: "open S" "connected S"
and holf: "⋀n::nat. ℱ n holomorphic_on S"
and holg: "g holomorphic_on S"
and ul_g: "⋀K. ⟦compact K; K ⊆ S⟧ ⟹ uniform_limit K ℱ g sequentially"
and nonconst: "~ g constant_on S"
and inj: "⋀n. inj_on (ℱ n) S"
shows "inj_on g S"
proof -
have False if z12: "z1 ∈ S" "z2 ∈ S" "z1 ≠ z2" "g z2 = g z1" for z1 z2
proof -
obtain z0 where "z0 ∈ S" and z0: "g z0 ≠ g z2"
using constant_on_def nonconst by blast
have "(λz. g z - g z1) holomorphic_on S"
by (intro holomorphic_intros holg)
then obtain r where "0 < r" "ball z2 r ⊆ S" "⋀z. dist z2 z < r ∧ z ≠ z2 ⟹ g z ≠ g z1"
apply (rule isolated_zeros [of "λz. g z - g z1" S z2 z0])
using S ‹z0 ∈ S› z0 z12 by auto
have "g z2 - g z1 ≠ 0"
proof (rule Hurwitz_no_zeros [of "S - {z1}" "λn z. ℱ n z - ℱ n z1" "λz. g z - g z1"])
show "open (S - {z1})"
show "connected (S - {z1})"
by (simp add: connected_open_delete [OF S])
show "⋀n. (λz. ℱ n z - ℱ n z1) holomorphic_on S - {z1}"
by (intro holomorphic_intros holomorphic_on_subset [OF holf]) blast
show "(λz. g z - g z1) holomorphic_on S - {z1}"
by (intro holomorphic_intros holomorphic_on_subset [OF holg]) blast
show "uniform_limit K (λn z. ℱ n z - ℱ n z1) (λz. g z - g z1) sequentially"
if "compact K" "K ⊆ S - {z1}" for K
proof (rule uniform_limitI)
fix e::real
assume "e > 0"
have "uniform_limit K ℱ g sequentially"
using that ul_g by fastforce
then have K: "∀⇩F n in sequentially. ∀x ∈ K. dist (ℱ n x) (g x) < e/2"
using ‹0 < e› by (force simp: intro!: uniform_limitD)
have "uniform_limit {z1} ℱ g sequentially"
then have "∀⇩F n in sequentially. ∀x ∈ {z1}. dist (ℱ n x) (g x) < e/2"
using ‹0 < e› by (force simp: intro!: uniform_limitD)
then have z1: "∀⇩F n in sequentially. dist (ℱ n z1) (g z1) < e/2"
by simp
have "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ 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)
have "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ n z1) (g x - g z1) < e/2 + e/2"
using eventually_conj [OF K z1]
apply (rule eventually_mono)
then
show "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ n z1) (g x - g z1) < e"
by simp
qed
show "¬ (λz. g z - g z1) constant_on S - {z1}"
unfolding constant_on_def
by (metis Diff_iff ‹z0 ∈ S› empty_iff insert_iff right_minus_eq z0 z12)
show "⋀n z. z ∈ S - {z1} ⟹ ℱ n z - ℱ n z1 ≠ 0"
by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 ‹z1 ∈ S›)
show "z2 ∈ S - {z1}"
using ‹z2 ∈ S› ‹z1 ≠ z2› by auto
qed
with z12 show False by auto
qed
then show ?thesis by (auto simp: inj_on_def)
qed

subsection‹The Great Picard theorem›

lemma GPicard1:
assumes S: "open S" "connected S" and "w ∈ S" "0 < r" "Y ⊆ X"
and holX: "⋀h. h ∈ X ⟹ h holomorphic_on S"
and X01:  "⋀h z. ⟦h ∈ X; z ∈ S⟧ ⟹ h z ≠ 0 ∧ h z ≠ 1"
and r:    "⋀h. h ∈ Y ⟹ norm(h w) ≤ r"
obtains B Z where "0 < B" "open Z" "w ∈ Z" "Z ⊆ S" "⋀h z. ⟦h ∈ Y; z ∈ Z⟧ ⟹ norm(h z) ≤ B"
proof -
obtain e where "e > 0" and e: "cball w e ⊆ S"
using assms open_contains_cball_eq by blast
show ?thesis
proof
show "0 < exp(pi * exp(pi * (2 + 2 * r + 12)))"
by simp
show "ball w (e / 2) ⊆ S"
using e ball_divide_subset_numeral ball_subset_cball by blast
show "cmod (h z) ≤ exp (pi * exp (pi * (2 + 2 * r + 12)))"
if "h ∈ Y" "z ∈ ball w (e / 2)" for h z
proof -
have "h ∈ X"
using ‹Y ⊆ X› ‹h ∈ Y›  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 ∘ (λ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 ‹e > 0› by (auto simp: dist_norm norm_mult)
have norm_le_r: "cmod ((h ∘ (λz. w + complex_of_real e * z)) 0) ≤ r"
by (auto simp: r ‹h ∈ Y›)
have le12: "norm (of_real(inverse e) * (z - w)) ≤ 1/2"
using that ‹e > 0› by (simp add: inverse_eq_divide dist_norm norm_minus_commute norm_divide)
have non01: "⋀z::complex. cmod z ≤ 1 ⟹ h (w + e * z) ≠ 0 ∧ h (w + e * z) ≠ 1"
apply (rule X01 [OF ‹h ∈ X›])
apply (rule subsetD [OF e])
using ‹0 < e›  by (auto simp: dist_norm norm_mult)
have "cmod (h z) ≤ cmod (h (w + of_real e * (inverse e * (z - w))))"
using ‹0 < e› by (simp add: divide_simps)
also have "... ≤ exp (pi * exp (pi * (14 + 2 * r)))"
using r [OF ‹h ∈ Y›] Schottky [OF hol_h_o norm_le_r _ _ _ le12] non01 by auto
finally
show ?thesis by simp
qed
qed (use ‹e > 0› in auto)
qed

lemma GPicard2:
assumes "S ⊆ T" "connected T" "S ≠ {}" "open S" "⋀x. ⟦x islimpt S; x ∈ T⟧ ⟹ x ∈ S"
shows "S = T"
by (metis assms open_subset connected_clopen closedin_limpt)

lemma GPicard3:
assumes S: "open S" "connected S" "w ∈ S" and "Y ⊆ X"
and holX: "⋀h. h ∈ X ⟹ h holomorphic_on S"
and X01:  "⋀h z. ⟦h ∈ X; z ∈ S⟧ ⟹ h z ≠ 0 ∧ h z ≠ 1"
and no_hw_le1: "⋀h. h ∈ Y ⟹ norm(h w) ≤ 1"
and "compact K" "K ⊆ S"
obtains B where "⋀h z. ⟦h ∈ Y; z ∈ K⟧ ⟹ norm(h z) ≤ B"
proof -
define U where "U ≡ {z ∈ S. ∃B Z. 0 < B ∧ open Z ∧ z ∈ Z ∧ Z ⊆ S ∧
(∀h z'. h ∈ Y ∧ z' ∈ Z ⟶ norm(h z') ≤ B)}"
then have "U ⊆ S" by blast
have "U = S"
proof (rule GPicard2 [OF ‹U ⊆ S› ‹connected S›])
show "U ≠ {}"
proof -
obtain B Z where "0 < B" "open Z" "w ∈ Z" "Z ⊆ S"
and  "⋀h z. ⟦h ∈ Y; z ∈ Z⟧ ⟹ norm(h z) ≤ B"
apply (rule GPicard1 [OF S zero_less_one ‹Y ⊆ X› holX])
using no_hw_le1 X01 by force+
then show ?thesis
unfolding U_def using ‹w ∈ S› by blast
qed
show "open U"
unfolding open_subopen [of U] by (auto simp: U_def)
fix v
assume v: "v islimpt U" "v ∈ S"
have "~ (∀r>0. ∃h∈Y. r < cmod (h v))"
proof
assume "∀r>0. ∃h∈Y. r < cmod (h v)"
then have "∀n. ∃h∈Y. Suc n < cmod (h v)"
by simp
then obtain ℱ where FY: "⋀n. ℱ n ∈ Y" and ltF: "⋀n. Suc n < cmod (ℱ n v)"
by metis
define 𝒢 where "𝒢 ≡ λn z. inverse(ℱ n z)"
have hol𝒢: "𝒢 n holomorphic_on S" for n
using FY X01 ‹Y ⊆ X› holX apply (blast intro: holomorphic_on_inverse)
done
have 𝒢not0: "𝒢 n z ≠ 0" and 𝒢not1: "𝒢 n z ≠ 1" if "z ∈ S" for n z
using FY X01 ‹Y ⊆ X› that by (force simp: 𝒢_def)+
have 𝒢_le1: "cmod (𝒢 n v) ≤ 1" for n
using less_le_trans linear ltF
by (fastforce simp add: 𝒢_def norm_inverse inverse_le_1_iff)
define W where "W ≡ {h. h holomorphic_on S ∧ (∀z ∈ S. h z ≠ 0 ∧ h z ≠ 1)}"
obtain B Z where "0 < B" "open Z" "v ∈ Z" "Z ⊆ S"
and B: "⋀h z. ⟦h ∈ range 𝒢; z ∈ Z⟧ ⟹ norm(h z) ≤ B"
apply (rule GPicard1 [OF ‹open S› ‹connected S› ‹v ∈ S› zero_less_one, of "range 𝒢" W])
using hol𝒢 𝒢not0 𝒢not1 𝒢_le1 by (force simp: W_def)+
then obtain e where "e > 0" and e: "ball v e ⊆ Z"
by (meson open_contains_ball)
obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j"
and lim:  "⋀x. x ∈ ball v e ⟹ (λn. 𝒢 (j n) x) ⇢ h x"
and ulim: "⋀K. ⟦compact K; K ⊆ ball v e⟧
⟹ uniform_limit K (𝒢 ∘ j) h sequentially"
proof (rule Montel)
show "⋀h. h ∈ range 𝒢 ⟹ h holomorphic_on ball v e"
by (metis ‹Z ⊆ S› e hol𝒢 holomorphic_on_subset imageE)
show "⋀K. ⟦compact K; K ⊆ ball v e⟧ ⟹ ∃B. ∀h∈range 𝒢. ∀z∈K. cmod (h z) ≤ B"
using B e by blast
qed auto
have "h v = 0"
proof (rule LIMSEQ_unique)
show "(λn. 𝒢 (j n) v) ⇢ h v"
using ‹e > 0› lim by simp
have lt_Fj: "real x ≤ cmod (ℱ (j x) v)" for x
by (metis of_nat_Suc ltF ‹strict_mono j› add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
show "(λn. 𝒢 (j n) v) ⇢ 0"
proof (rule Lim_null_comparison [OF eventually_sequentiallyI lim_inverse_n])
show "cmod (𝒢 (j x) v) ≤ inverse (real x)" if "1 ≤ x" for x
using that by (simp add: 𝒢_def norm_inverse_le_norm [OF lt_Fj])
qed
qed
have "h v ≠ 0"
proof (rule Hurwitz_no_zeros [of "ball v e" "𝒢 ∘ j" h])
show "⋀n. (𝒢 ∘ j) n holomorphic_on ball v e"
using ‹Z ⊆ S› e hol𝒢 by force
show "⋀n z. z ∈ ball v e ⟹ (𝒢 ∘ j) n z ≠ 0"
using 𝒢not0 ‹Z ⊆ S› e by fastforce
show "¬ h constant_on ball v e"
proof (clarsimp simp: constant_on_def)
fix c
have False if "⋀z. dist v z < e ⟹ h z = c"
proof -
have "h v = c"
by (simp add: ‹0 < e› that)
obtain y where "y ∈ U" "y ≠ v" and y: "dist y v < e"
using v ‹e > 0› by (auto simp: islimpt_approachable)
then obtain C T where "y ∈ S" "C > 0" "open T" "y ∈ T" "T ⊆ S"
and "⋀h z'. ⟦h ∈ Y; z' ∈ T⟧ ⟹ cmod (h z') ≤ C"
using ‹y ∈ U› by (auto simp: U_def)
then have le_C: "⋀n. cmod (ℱ n y) ≤ C"
using FY by blast
have "∀⇩F n in sequentially. dist (𝒢 (j n) y) (h y) < inverse C"
using uniform_limitD [OF ulim [of "{y}"], of "inverse C"] ‹C > 0› y
then obtain n where "dist (𝒢 (j n) y) (h y) < inverse C"
by (meson eventually_at_top_linorder order_refl)
moreover
have "h y = h v"
by (metis ‹h v = c› dist_commute that y)
ultimately have "norm (𝒢 (j n) y) < inverse C"
by (simp add: ‹h v = 0›)
then have "C < norm (ℱ (j n) y)"
by (metis FY X01 ‹0 < C› ‹y ∈ S› ‹Y ⊆ X› inverse_less_iff_less norm_inverse subsetD zero_less_norm_iff)
show False
using ‹C < cmod (ℱ (j n) y)› le_C not_less by blast
qed
then show "∃x∈ball v e. h x ≠ c" by force
qed
show "h holomorphic_on ball v e"
show "⋀K. ⟦compact K; K ⊆ ball v e⟧ ⟹ uniform_limit K (𝒢 ∘ j) h sequentially"
qed (use ‹e > 0› in auto)
with ‹h v = 0› show False by blast
qed
then show "v ∈ U"
apply (clarsimp simp add: U_def v)
apply (rule GPicard1[OF ‹open S› ‹connected S› ‹v ∈ S› _ ‹Y ⊆ X› holX])
using X01 no_hw_le1 apply (meson | force simp: not_less)+
done
qed
have "⋀x. x ∈ K ⟶ x ∈ U"
using ‹U = S› ‹K ⊆ S› by blast
then have "⋀x. x ∈ K ⟶ (∃B Z. 0 < B ∧ open Z ∧ x ∈ Z ∧
(∀h z'. h ∈ Y ∧ z' ∈ Z ⟶ norm(h z') ≤ B))"
unfolding U_def by blast
then obtain F Z where F: "⋀x. x ∈ K ⟹ open (Z x) ∧ x ∈ Z x ∧
(∀h z'. h ∈ Y ∧ z' ∈ Z x ⟶ norm(h z') ≤ F x)"
by metis
then obtain L where "L ⊆ K" "finite L" and L: "K ⊆ (⋃c ∈ L. Z c)"
by (auto intro: compactE_image [OF ‹compact K›, of K Z])
then have *: "⋀x h z'. ⟦x ∈ L; h ∈ Y ∧ z' ∈ Z x⟧ ⟹ cmod (h z') ≤ F x"
using F by blast
have "∃B. ∀h z. h ∈ Y ∧ z ∈ K ⟶ norm(h z) ≤ B"
proof (cases "L = {}")
case True with L show ?thesis by simp
next
case False
with ‹finite L› show ?thesis
apply (rule_tac x = "Max (F  L)" in exI)
using * F  by (metis L UN_E subsetD)
qed
with that show ?thesis by metis
qed

lemma GPicard4:
assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})"
and AE: "⋀e. ⟦0 < e; e < k⟧ ⟹ ∃d. 0 < d ∧ d < e ∧ (∀z ∈ sphere 0 d. norm(f z) ≤ B)"
obtains ε where "0 < ε" "ε < k" "⋀z. z ∈ ball 0 ε - {0} ⟹ norm(f z) ≤ B"
proof -
obtain ε where "0 < ε" "ε < k/2" and ε: "⋀z. norm z = ε ⟹ norm(f z) ≤ B"
using AE [of "k/2"] ‹0 < k› by auto
show ?thesis
proof
show "ε < k"
using ‹0 < k› ‹ε < k/2› by auto
show "cmod (f ξ) ≤ B" if ξ: "ξ ∈ ball 0 ε - {0}" for ξ
proof -
obtain d where "0 < d" "d < norm ξ" and d: "⋀z. norm z = d ⟹ norm(f z) ≤ B"
using AE [of "norm ξ"] ‹ε < k› ξ by auto
have [simp]: "closure (cball 0 ε - ball 0 d) = cball 0 ε - ball 0 d"
by (blast intro!: closure_closed)
have [simp]: "interior (cball 0 ε - ball 0 d) = ball 0 ε - cball (0::complex) d"
using ‹0 < ε› ‹0 < d› by (simp add: interior_diff)
have *: "norm(f w) ≤ B" if "w ∈ cball 0 ε - ball 0 d" for w
proof (rule maximum_modulus_frontier [of f "cball 0 ε - ball 0 d"])
show "f holomorphic_on interior (cball 0 ε - ball 0 d)"
apply (rule holomorphic_on_subset [OF holf])
using ‹ε < k› ‹0 < d› that by auto
show "continuous_on (closure (cball 0 ε - ball 0 d)) f"
apply (rule holomorphic_on_imp_continuous_on)
apply (rule holomorphic_on_subset [OF holf])
using ‹0 < d› ‹ε < k› by auto
show "⋀z. z ∈ frontier (cball 0 ε - ball 0 d) ⟹ cmod (f z) ≤ B"
using ε d less_eq_real_def by blast
qed (use that in auto)
show ?thesis
using * ‹d < cmod ξ› that by auto
qed
qed (use ‹0 < ε› in auto)
qed

lemma GPicard5:
assumes holf: "f holomorphic_on (ball 0 1 - {0})"
and f01:  "⋀z. z ∈ ball 0 1 - {0} ⟹ f z ≠ 0 ∧ f z ≠ 1"
obtains e B where "0 < e" "e < 1" "0 < B"
"(∀z ∈ ball 0 e - {0}. norm(f z) ≤ B) ∨
(∀z ∈ ball 0 e - {0}. norm(f z) ≥ B)"
proof -
have [simp]: "1 + of_nat n ≠ (0::complex)" for n
using of_nat_eq_0_iff by fastforce
have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
by (metis norm_of_nat of_nat_Suc)
have *: "(λx::complex. x / of_nat (Suc n))  (ball 0 1 - {0}) ⊆ ball 0 1 - {0}" for n
by (auto simp: norm_divide divide_simps split: if_split_asm)
define h where "h ≡ λn z::complex. f (z / (Suc n))"
have holh: "(h n) holomorphic_on ball 0 1 - {0}" for n
unfolding h_def
proof (rule holomorphic_on_compose_gen [unfolded o_def, OF _ holf *])
show "(λx. x / of_nat (Suc n)) holomorphic_on ball 0 1 - {0}"
by (intro holomorphic_intros) auto
qed
have h01: "⋀n z. z ∈ ball 0 1 - {0} ⟹ h n z ≠ 0 ∧ h n z ≠ 1"
unfolding h_def
apply (rule f01)
using * by force
obtain w where w: "w ∈ ball 0 1 - {0::complex}"
by (rule_tac w = "1/2" in that) auto
consider "infinite {n. norm(h n w) ≤ 1}" | "infinite {n. 1 ≤ norm(h n w)}"
by (metis (mono_tags, lifting) infinite_nat_iff_unbounded_le le_cases mem_Collect_eq)
then show ?thesis
proof cases
case 1
with infinite_enumerate obtain r :: "nat ⇒ nat"
where "strict_mono r" and r: "⋀n. r n ∈ {n. norm(h n w) ≤ 1}"
by blast
obtain B where B: "⋀j z. ⟦norm z = 1/2; j ∈ range (h ∘ r)⟧ ⟹ norm(j z) ≤ B"
proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])
show "range (h ∘ r) ⊆
{g. g holomorphic_on ball 0 1 - {0} ∧ (∀z∈ball 0 1 - {0}. g z ≠ 0 ∧ g z ≠ 1)}"
apply clarsimp
apply (intro conjI holomorphic_intros holomorphic_on_compose holh)
using h01 apply auto
done
show "connected (ball 0 1 - {0::complex})"
qed (use r in auto)
have normf_le_B: "cmod(f z) ≤ B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
proof -
have *: "⋀w. norm w = 1/2 ⟹ cmod((f (w / (1 + of_nat (r n))))) ≤ B"
using B by (auto simp: h_def o_def)
have half: "norm (z * (1 + of_nat (r n))) = 1/2"
by (simp add: norm_mult divide_simps that)
show ?thesis
using * [OF half] by simp
qed
obtain ε where "0 < ε" "ε < 1" "⋀z. z ∈ ball 0 ε - {0} ⟹ cmod(f z) ≤ B"
proof (rule GPicard4 [OF zero_less_one holf, of B])
fix e::real
assume "0 < e" "e < 1"
obtain n where "(1/e - 2) / 2 < real n"
using reals_Archimedean2 by blast
also have "... ≤ r n"
using ‹strict_mono r› by (simp add: seq_suble)
finally have "(1/e - 2) / 2 < real (r n)" .
with ‹0 < e› have e: "e > 1 / (2 + 2 * real (r n))"
show "∃d>0. d < e ∧ (∀z∈sphere 0 d. cmod (f z) ≤ B)"
apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
using normf_le_B by (simp add: e)
qed blast
then have ε: "cmod (f z) ≤ ¦B¦ + 1" if "cmod z < ε" "z ≠ 0" for z
using that by fastforce
have "0 < ¦B¦ + 1"
by simp
then show ?thesis
apply (rule that [OF ‹0 < ε› ‹ε < 1›])
using ε by auto
next
case 2
with infinite_enumerate obtain r :: "nat ⇒ nat"
where "strict_mono r" and r: "⋀n. r n ∈ {n. norm(h n w) ≥ 1}"
by blast
obtain B where B: "⋀j z. ⟦norm z = 1/2; j ∈ range (λn. inverse ∘ h (r n))⟧ ⟹ norm(j z) ≤ B"
proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])
show "range (λn. inverse ∘ h (r n)) ⊆
{g. g holomorphic_on ball 0 1 - {0} ∧ (∀z∈ball 0 1 - {0}. g z ≠ 0 ∧ g z ≠ 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
show "connected (ball 0 1 - {0::complex})"
show "⋀j. j ∈ range (λn. inverse ∘ h (r n)) ⟹ cmod (j w) ≤ 1"
using r norm_inverse_le_norm by fastforce
qed (use r in auto)
have norm_if_le_B: "cmod(inverse (f z)) ≤ B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
proof -
have *: "inverse (cmod((f (z / (1 + of_nat (r n)))))) ≤ B" if "norm z = 1/2" for z
using B [OF that] by (force simp: norm_inverse h_def)
have half: "norm (z * (1 + of_nat (r n))) = 1/2"
by (simp add: norm_mult divide_simps that)
show ?thesis
using * [OF half] by (simp add: norm_inverse)
qed
have hol_if: "(inverse ∘ f) holomorphic_on (ball 0 1 - {0})"
by (metis (no_types, lifting) holf comp_apply f01 holomorphic_on_inverse holomorphic_transform)
obtain ε where "0 < ε" "ε < 1" and leB: "⋀z. z ∈ ball 0 ε - {0} ⟹ cmod((inverse ∘ f) z) ≤ B"
proof (rule GPicard4 [OF zero_less_one hol_if, of B])
fix e::real
assume "0 < e" "e < 1"
obtain n where "(1/e - 2) / 2 < real n"
using reals_Archimedean2 by blast
also have "... ≤ r n"
using ‹strict_mono r› by (simp add: seq_suble)
finally have "(1/e - 2) / 2 < real (r n)" .
with ‹0 < e› have e: "e > 1 / (2 + 2 * real (r n))"
show "∃d>0. d < e ∧ (∀z∈sphere 0 d. cmod ((inverse ∘ f) z) ≤ B)"
apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
using norm_if_le_B by (simp add: e)
qed blast
have ε: "cmod (f z) ≥ inverse B" and "B > 0" if "cmod z < ε" "z ≠ 0" for z
proof -
have "inverse (cmod (f z)) ≤ B"
using leB that by (simp add: norm_inverse)
moreover
have "f z ≠ 0"
using ‹ε < 1› f01 that by auto
ultimately show "cmod (f z) ≥ inverse B"
show "B > 0"
using ‹f z ≠ 0› ‹inverse (cmod (f z)) ≤ B› not_le order.trans by fastforce
qed
then have "B > 0"
by (metis ‹0 < ε› dense leI order.asym vector_choose_size)
then have "inverse B > 0"
then show ?thesis
apply (rule that [OF ‹0 < ε› ‹ε < 1›])
using ε by auto
qed
qed

lemma GPicard6:
assumes "open M" "z ∈ M" "a ≠ 0" and holf: "f holomorphic_on (M - {z})"
and f0a: "⋀w. w ∈ M - {z} ⟹ f w ≠ 0 ∧ f w ≠ a"
obtains r where "0 < r" "ball z r ⊆ M"
"bounded(f  (ball z r - {z})) ∨
bounded((inverse ∘ f)  (ball z r - {z}))"
proof -
obtain r where "0 < r" and r: "ball z r ⊆ M"
using assms openE by blast
let ?g = "λw. f (z + of_real r * w) / a"
obtain e B where "0 < e" "e < 1" "0 < B"
and B: "(∀z ∈ ball 0 e - {0}. norm(?g z) ≤ B) ∨ (∀z ∈ ball 0 e - {0}. norm(?g z) ≥ 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 ‹0 < r› ‹a ≠ 0› r
by (auto simp: dist_norm norm_mult subset_eq)
show "⋀w. w ∈ ball 0 1 - {0} ⟹ f (z + of_real r * w) / a ≠ 0 ∧ f (z + of_real r * w) / a ≠ 1"
apply (simp add: divide_simps ‹a ≠ 0›)
apply (rule f0a)
using ‹0 < r› r by (auto simp: dist_norm norm_mult subset_eq)
qed
show ?thesis
proof
show "0 < e*r"
by (simp add: ‹0 < e› ‹0 < r›)
have "ball z (e * r) ⊆ ball z r"
by (simp add: ‹0 < r› ‹e < 1› order.strict_implies_order subset_ball)
then show "ball z (e * r) ⊆ M"
using r by blast
consider "⋀z. z ∈ ball 0 e - {0} ⟹ norm(?g z) ≤ B" | "⋀z. z ∈ ball 0 e - {0} ⟹ norm(?g z) ≥ B"
using B by blast
then show "bounded (f  (ball z (e * r) - {z})) ∨
bounded ((inverse ∘ f)  (ball z (e * r) - {z}))"
proof cases
case 1
have "⟦dist z w < e * r; w ≠ z⟧ ⟹ cmod (f w) ≤ B * norm a" for w
using ‹a ≠ 0› ‹0 < r› 1 [of "(w - z) / r"]
by (simp add: norm_divide dist_norm divide_simps)
then show ?thesis
by (force simp: intro!: boundedI)
next
case 2
have "⟦dist z w < e * r; w ≠ z⟧ ⟹ cmod (f w) ≥ B * norm a" for w
using ‹a ≠ 0› ‹0 < r› 2 [of "(w - z) / r"]
by (simp add: norm_divide dist_norm divide_simps)
then have "⟦dist z w < e * r; w ≠ z⟧ ⟹ inverse (cmod (f w)) ≤ inverse (B * norm a)" for w
by (metis ‹0 < B› ‹a ≠ 0› mult_pos_pos norm_inverse norm_inverse_le_norm zero_less_norm_iff)
then show ?thesis
by (force simp: norm_inverse intro!: boundedI)
qed
qed
qed

theorem great_Picard:
assumes "open M" "z ∈ M" "a ≠ b" and holf: "f holomorphic_on (M - {z})"
and fab: "⋀w. w ∈ M - {z} ⟹ f w ≠ a ∧ f w ≠ b"
obtains l where "(f ⤏ l) (at z) ∨ ((inverse ∘ f) ⤏ l) (at z)"
proof -
obtain r where "0 < r" and zrM: "ball z r ⊆ M"
and r: "bounded((λz. f z - a)  (ball z r - {z})) ∨
bounded((inverse ∘ (λz. f z - a))  (ball z r - {z}))"
proof (rule GPicard6 [OF ‹open M› ‹z ∈ M›])
show "b - a ≠ 0"
using assms by auto
show "(λz. f z - a) holomorphic_on M - {z}"
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
have holfb_i: "(λz. inverse(f z - a)) holomorphic_on ball z r - {z}"
apply (intro holomorphic_intros holfb)
using fab zrM by fastforce
show ?thesis
using r
proof
assume "bounded ((λz. f z - a)  (ball z r - {z}))"
then obtain B where B: "⋀w. w ∈ (λz. f z - a)  (ball z r - {z}) ⟹ norm w ≤ B"
by (force simp: bounded_iff)
have "∀⇩F w in at z. cmod (f w - a) ≤ B"
apply (rule_tac x=r in exI)
using ‹0 < r› by (auto simp: dist_commute intro!: B)
then have "∃B. ∀⇩F w in at z. cmod (f w) ≤ B"
apply (rule_tac x="B + norm a" in exI)
apply (erule eventually_mono)
then obtain g where holg: "g holomorphic_on ball z r" and gf: "⋀w. w ∈ ball z r - {z} ⟹ g w = f w"
using ‹0 < r› holomorphic_on_extend_bounded [OF holfb] by auto
then have "g ─z→ g z"
using ‹0 < r› centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
then have "(f ⤏ g z) (at z)"
apply (rule Lim_transform_within_open [of g "g z" z UNIV "ball z r"])
using  ‹0 < r› by (auto simp: gf)
then show ?thesis
using that by blast
next
assume "bounded((inverse ∘ (λz. f z - a))  (ball z r - {z}))"
then obtain B where B: "⋀w. w ∈ (inverse ∘ (λz. f z - a))  (ball z r - {z}) ⟹ norm w ≤ B"
by (force simp: bounded_iff)
have "∀⇩F w in at z. cmod (inverse (f w - a)) ≤ B"
apply (rule_tac x=r in exI)
using ‹0 < r› by (auto simp: dist_commute intro!: B)
then have "∃B. ∀⇩F z in at z. cmod (inverse (f z - a)) ≤ B"
by blast
then obtain g where holg: "g holomorphic_on ball z r" and gf: "⋀w. w ∈ ball z r - {z} ⟹ g w = inverse (f w - a)"
using ‹0 < r› holomorphic_on_extend_bounded [OF holfb_i] by auto
then have gz: "g ─z→ g z"
using ‹0 < r› centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
have gnz: "⋀w. w ∈ ball z r - {z} ⟹ g w ≠ 0"
using gf fab zrM by fastforce
show ?thesis
proof (cases "g z = 0")
case True
have *: "⟦g ≠ 0; inverse g = f - a⟧ ⟹ g / (1 + a * g) = inverse f" for f g::complex
by (auto simp: field_simps)
have "(inverse ∘ f) ─z→ 0"
proof (rule Lim_transform_within_open [of "λw. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
show "(λw. g w / (1 + a * g w)) ─z→ 0"
using True by (auto simp: intro!: tendsto_eq_intros gz)
show "⋀x. ⟦x ∈ ball z r; x ≠ z⟧ ⟹ g x / (1 + a * g x) = (inverse ∘ f) x"
using * gf gnz by simp
qed (use ‹0 < r› in auto)
with that show ?thesis by blast
next
case False
show ?thesis
proof (cases "1 + a * g z = 0")
case True
have "(f ⤏ 0) (at z)"
proof (rule Lim_transform_within_open [of "λw. (1 + a * g w) / g w" _ _ _ "ball z r"])
show "(λw. (1 + a * g w) / g w) ─z→ 0"
apply (rule tendsto_eq_intros refl gz ‹g z ≠ 0›)+
show "⋀x. ⟦x ∈ ball z r; x ≠ z⟧ ⟹ (1 + a * g x) / g x = f x"
using fab fab zrM by (fastforce simp add: gf divide_simps)
qed (use ‹0 < r› in auto)
then show ?thesis
using that by blast
next
case False
have *: "⟦g ≠ 0; inverse g = f - a⟧ ⟹ g / (1 + a * g) = inverse f" for f g::complex
by (auto simp: field_simps)
have "(inverse ∘ f) ─z→ g z / (1 + a * g z)"
proof (rule Lim_transform_within_open [of "λw. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
show "(λw. g w / (1 + a * g w)) ─z→ g z / (1 + a * g z)"
using False by (auto simp: False intro!: tendsto_eq_intros gz)
show "⋀x. ⟦x ∈ ball z r; x ≠ z⟧ ⟹ g x / (1 + a * g x) = (inverse ∘ f) x"
using * gf gnz by simp
qed (use ‹0 < r› in auto)
with that show ?thesis by blast
qed
qed
qed
qed

corollary great_Picard_alt:
assumes M: "open M" "z ∈ M" and holf: "f holomorphic_on (M - {z})"
and non: "⋀l. ¬ (f ⤏ l) (at z)" "⋀l. ¬ ((inverse ∘ f) ⤏ l) (at z)"
obtains a where "- {a} ⊆ f  (M - {z})"
by (metis great_Picard [OF M _ holf] non)

corollary great_Picard_infinite:
assumes M: "open M" "z ∈ M" and holf: "f holomorphic_on (M - {z})"
and non: "⋀l. ¬ (f ⤏ l) (at z)" "⋀l. ¬ ((inverse ∘ f) ⤏ l) (at z)"
obtains a where "⋀w. w ≠ a ⟹ infinite {x. x ∈ M - {z} ∧ f x = w}"
proof -
have False if "a ≠ b" and ab: "finite {x. x ∈ M - {z} ∧ f x = a}" "finite {x. x ∈ M - {z} ∧ f x = b}" for a b
proof -
have finab: "finite {x. x ∈ M - {z} ∧ f x ∈ {a,b}}"
using finite_UnI [OF ab]  unfolding mem_Collect_eq insert_iff empty_iff
obtain r where "0 < r" and zrM: "ball z r ⊆ M" and r: "⋀x. ⟦x ∈ M - {z}; f x ∈ {a,b}⟧ ⟹ x ∉ ball z r"
proof -
obtain e where "e > 0" and e: "ball z e ⊆ M"
using assms openE by blast
show ?thesis
proof (cases "{x ∈ M - {z}. f x ∈ {a, b}} = {}")
case True
then show ?thesis
apply (rule_tac r=e in that)
using e ‹e > 0› by auto
next
case False
let ?r = "min e (Min (dist z  {x ∈ M - {z}. f x ∈ {a,b}}))"
show ?thesis
proof
show "0 < ?r"
using min_less_iff_conj Min_gr_iff finab False ‹0 < e› by auto
have "ball z ?r ⊆ ball z e"
with e show "ball z ?r ⊆ M" by blast
show "⋀x. ⟦x ∈ M - {z}; f x ∈ {a, b}⟧ ⟹ x ∉ ball z ?r"
using min_less_iff_conj Min_gr_iff finab False ‹0 < e› by auto
qed
qed
qed
have holfb: "f holomorphic_on (ball z r - {z})"
apply (rule holomorphic_on_subset [OF holf])
using zrM by auto
show ?thesis
apply (rule great_Picard [OF open_ball _ ‹a ≠ b› holfb])
using non ‹0 < r› r zrM by auto
qed
with that show thesis
by meson
qed

corollary Casorati_Weierstrass:
assumes "open M" "z ∈ M" "f holomorphic_on (M - {z})"
and "⋀l. ¬ (f ⤏ l) (at z)" "⋀l. ¬ ((inverse ∘ f) ⤏ l) (at z)"
shows "closure(f  (M - {z})) = UNIV"
proof -
obtain a where a: "- {a} ⊆ f  (M - {z})"
using great_Picard_alt [OF assms] .
have "UNIV = closure(- {a})"
also have "... ⊆ closure(f  (M - {z}))"