refine (hurwitz2 hU hF hf hr h6 h8 h7).mono ?_
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r✝ : ℝ
U s : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
h1 : f z₀ = 0
h2 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
H5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
h3 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
h4' : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ s
r : ℝ
hr : r > 0
h5 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h6 : closedBall z₀ r ⊆ U
h7 : cindex z₀ r f ≠ 0
h9 : closedBall z₀ r ⊆ s
h8 : ∀ z ∈ sphere z₀ r, f z ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r✝ : ℝ
U s : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
h1 : f z₀ = 0
h2 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
H5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
h3 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
h4' : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ s
r : ℝ
hr : r > 0
h5 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h6 : closedBall z₀ r ⊆ U
h7 : cindex z₀ r f ≠ 0
h9 : closedBall z₀ r ⊆ s
h8 : ∀ z ∈ sphere z₀ r, f z ≠ 0
⊢ ∀ (x : ι), (∃ z ∈ ball z₀ r, F x z = 0) → ∃ z ∈ s, F x z = 0