Complex.Hadamard.exists_r0_le_norm_divisorZeroIndex₀_val

lemma exists_r0_le_norm_divisorZeroIndex₀_val {f : ℂ → ℂ}    (hf : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0) :    ∃ r0 : ℝ, 0 < r0 ∧      ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ), r0 ≤ ‖divisorZeroIndex₀_val p‖ := by  classical  set U : Set ℂ := (Set.univ : Set ℂ)  set D : Function.locallyFinsuppWithin U ℤ := MeromorphicOn.divisor f U  have hDnonneg : 0 ≤ D := by    simpa [D, U] using (Differentiable.divisor_nonneg (f := f) hf)  have hzero : ∀ p : divisorZeroIndex₀ f U, f (divisorZeroIndex₀_val p) = 0 := by    intro p    set z : ℂ := divisorZeroIndex₀_val p    have hneTop : meromorphicOrderAt f z ≠ ⊤ := by      have hzAnal : AnalyticAt ℂ f z := hf.analyticAt z      have hzA : analyticOrderAt f z ≠ ⊤ :=        analyticOrderAt_ne_top_of_exists_ne_zero (f := f) (hf := hf) hnot (z := z)      intro htop      have hm : meromorphicOrderAt f z = (analyticOrderAt f z).map (↑) :=        hzAnal.meromorphicOrderAt_eq (𝕜 := ℂ)      cases h : analyticOrderAt f z with      | top =>          exact hzA (by simp [h])      | coe n =>          have : (analyticOrderAt f z).map (↑) ≠ (⊤ : WithTop ℤ) := by            simp [h]          exact this (by simpa [hm] using htop)    have hmon : MeromorphicOn f U := by      intro w hw; exact (hf.analyticAt w).meromorphicAt    have hdiv : MeromorphicOn.divisor f U z = (meromorphicOrderAt f z).untop₀ := by      simpa [U] using (MeromorphicOn.divisor_apply (f := f) (U := U) (z := z) hmon (by aesop))    have hDz : MeromorphicOn.divisor f U z ≠ 0 := by      have hzsup : z ∈ (MeromorphicOn.divisor f U).support := by        simp [z]      simpa [Function.mem_support] using hzsup    have hposZ : (0 : ℤ) < (meromorphicOrderAt f z).untop₀ := by      have hge0 : 0 ≤ (meromorphicOrderAt f z).untop₀ := by        have : 0 ≤ MeromorphicOn.divisor f U z := by          simpa [D, U, z] using hDnonneg z        simpa [hdiv] using this      have hne0 : (meromorphicOrderAt f z).untop₀ ≠ 0 := by        simpa [hdiv] using hDz      exact lt_of_le_of_ne hge0 (by simpa [eq_comm] using hne0)    have hpos : (0 : WithTop ℤ) < meromorphicOrderAt f z := by      have : (0 : WithTop ℤ) < ((meromorphicOrderAt f z).untop₀ : WithTop ℤ) :=        WithTop.coe_lt_coe.2 hposZ      simpa [WithTop.coe_untop₀_of_ne_top hneTop] using this    have htend0 : Tendsto f (𝓝[≠] z) (𝓝 (0 : ℂ)) :=      tendsto_zero_of_meromorphicOrderAt_pos (f := f) (x := z) hpos    have hcontz : ContinuousAt f z := (hf z).continuousAt    have htendz : Tendsto f (𝓝[≠] z) (𝓝 (f z)) :=      (hcontz.tendsto.mono_left (nhdsWithin_le_nhds : 𝓝[≠] z ≤ 𝓝 z))    exact tendsto_nhds_unique htendz htend0  by_cases h0 : f 0 = 0  · have hD0 : D 0 ≠ 0 := by      have hmero0 : MeromorphicAt f (0 : ℂ) := (hf.analyticAt 0).meromorphicAt      have hneTop0 : meromorphicOrderAt f (0 : ℂ) ≠ ⊤ := by        have hA0 : analyticOrderAt f (0 : ℂ) ≠ ⊤ :=          analyticOrderAt_ne_top_of_exists_ne_zero (f := f) (hf := hf) hnot (z := 0)        intro htop        have hm : meromorphicOrderAt f (0 : ℂ) = (analyticOrderAt f (0 : ℂ)).map (↑) :=          (hf.analyticAt 0).meromorphicOrderAt_eq (𝕜 := ℂ)        cases h : analyticOrderAt f (0 : ℂ) with        | top => exact Ne.elim hA0 h        | coe n =>            have : (analyticOrderAt f (0 : ℂ)).map (↑) ≠ (⊤ : WithTop ℤ) := by              simp [h]            exact this (by simpa [hm] using htop)      have htend0 : Tendsto f (𝓝[≠] (0 : ℂ)) (𝓝 (0 : ℂ)) := by        have hcont0 : ContinuousAt f (0 : ℂ) := (hf 0).continuousAt        have : Tendsto f (𝓝 (0 : ℂ)) (𝓝 (0 : ℂ)) := by simpa [h0] using hcont0.tendsto        exact this.mono_left (nhdsWithin_le_nhds : 𝓝[≠] (0 : ℂ) ≤ 𝓝 (0 : ℂ))      have hpos0 : (0 : WithTop ℤ) < meromorphicOrderAt f (0 : ℂ) :=        (tendsto_zero_iff_meromorphicOrderAt_pos hmero0).1 htend0      have hpos0' : (0 : ℤ) < (meromorphicOrderAt f (0 : ℂ)).untop₀ := by        have : (0 : WithTop ℤ) < ((meromorphicOrderAt f (0 : ℂ)).untop₀ : WithTop ℤ) := by          simpa [WithTop.coe_untop₀_of_ne_top hneTop0] using hpos0        simpa using (WithTop.coe_lt_coe.1 this)      have hdiv0 : D 0 = (meromorphicOrderAt f (0 : ℂ)).untop₀ := by        have hmon : MeromorphicOn f U := by          intro w hw; exact (hf.analyticAt w).meromorphicAt        simpa [D, U] using          (MeromorphicOn.divisor_apply (f := f) (U := U) (z := (0 : ℂ))            hmon (by aesop))      exact by        have : (meromorphicOrderAt f (0 : ℂ)).untop₀ ≠ 0 := ne_of_gt hpos0'        simpa [hdiv0] using this    have hmem0 : (0 : ℂ) ∈ D.support := by      simp [Function.mem_support, hD0]    have hdisc : IsDiscrete D.support := by      simpa [D] using (D.discreteSupport)    rcases Metric.exists_ball_inter_eq_singleton_of_mem_discrete hdisc hmem0 with ⟨r0, hr0pos, hr0⟩    refine ⟨r0, hr0pos, ?_⟩    intro p    have hp : divisorZeroIndex₀_val p ∈ D.support := by      simp [D, divisorZeroIndex₀_val_mem_divisor_support (f := f) (U := U) p]    have hnotBall : divisorZeroIndex₀_val p ∉ Metric.ball (0 : ℂ) r0 := by      intro hball      have : divisorZeroIndex₀_val p ∈ Metric.ball (0 : ℂ) r0 ∩ D.support := ⟨hball, hp⟩      have : divisorZeroIndex₀_val p ∈ ({(0 : ℂ)} : Set ℂ) := by simp [hr0] at this      have : divisorZeroIndex₀_val p = 0 := by simp [Set.mem_singleton_iff] at this      exact (divisorZeroIndex₀_val_ne_zero p) this    have : r0 ≤ ‖divisorZeroIndex₀_val p‖ := by      have : ¬ ‖divisorZeroIndex₀_val p‖ < r0 := by        intro hlt        exact hnotBall (by simpa [Metric.mem_ball, dist_zero_right] using hlt)      exact le_of_not_gt this    exact this  · have hcont0 : ContinuousAt f (0 : ℂ) := (hf 0).continuousAt    have hne : ∀ᶠ z in 𝓝 (0 : ℂ), f z ≠ 0 := hcont0.eventually_ne h0    rcases Metric.mem_nhds_iff.1 hne with ⟨r0, hr0pos, hr0⟩    refine ⟨r0, hr0pos, ?_⟩    intro p    have : ¬ ‖divisorZeroIndex₀_val p‖ < r0 := by      intro hlt      have hzball : divisorZeroIndex₀_val p ∈ Metric.ball (0 : ℂ) r0 := by        simpa [Metric.mem_ball, dist_zero_right] using hlt      have : f (divisorZeroIndex₀_val p) ≠ 0 := hr0 hzball      exact this (hzero p)    exact le_of_not_gt this