Theorem: hurwitz3 (RMT4/hurwitz.lean)

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
by_cases h : NeBot p
State after:
case pos
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

case neg
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
case neg => simp at h; simp [h]
State after:
no goals

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
case pos =>
  have H1 := (hf.differentiableOn hF hU).analyticAt (hU.mem_nhds hz₀)
  have H5 := cindex_pos H1 h1 h2
  rw [eventually_nhdsWithin_iff] at h2
  have h3 := eventually_nhds_iff_eventually_closed_ball.1 h2
  have h4 : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ U :=
    (eventually_closedBall_subset (hU.mem_nhds hz₀)).filter_mono nhdsWithin_le_nhds
  have h4' : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ s :=
    (eventually_closedBall_subset hs).filter_mono nhdsWithin_le_nhds
  obtain ⟨r, hr, h5, h6, h7, h9⟩ := (h3.and (h4.and (H5.and h4'))).exists'
  have h8 : ∀ z ∈ sphere z₀ r, f z ≠ 0 := by
    exact λ z hz => h5 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz hr.lt.ne.symm)
  refine (hurwitz2 hU hF hf hr h6 h8 h7).mono ?_
  rintro n ⟨z, hz, hFnz⟩
  refine ⟨z, h9 (ball_subset_closedBall hz), hFnz⟩
State after:
no goals

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
simp at h
State after:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : p = ⊥
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : p = ⊥
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
simp [h]
State after:
no goals

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have H1 := (hf.differentiableOn hF hU).analyticAt (hU.mem_nhds hz₀)
State after:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have H5 := cindex_pos H1 h1 h2
State after:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
H5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
hs : s ∈ 𝓝 z₀
h : NeBot p
H1 : AnalyticAt ℂ f z₀
H5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
rw [eventually_nhdsWithin_iff] at h2
State after:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have h3 := eventually_nhds_iff_eventually_closed_ball.1 h2
State after:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have h4 : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ U :=
  (eventually_closedBall_subset (hU.mem_nhds hz₀)).filter_mono nhdsWithin_le_nhds
State after:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have h4' : ∀ᶠ r in 𝓝[>] 0, closedBall z₀ r ⊆ s :=
  (eventually_closedBall_subset hs).filter_mono nhdsWithin_le_nhds
State after:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
obtain ⟨r, hr, h5, h6, h7, h9⟩ := (h3.and (h4.and (H5.and h4'))).exists'
State after:
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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0

State before:
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
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
have h8 : ∀ z ∈ sphere z₀ r, f z ≠ 0 := by
  exact λ z hz => h5 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz hr.lt.ne.symm)
State after:
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

State before:
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
Tactic:
refine (hurwitz2 hU hF hf hr h6 h8 h7).mono ?_
State after:
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

State before:
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
Tactic:
rintro n ⟨z, hz, hFnz⟩
State after:
case intro.intro.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 : ι
z : ℂ
hz : z ∈ ball z₀ r
hFnz : F n z = 0
⊢ ∃ z ∈ s, F n z = 0

State before:
case intro.intro.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 : ι
z : ℂ
hz : z ∈ ball z₀ r
hFnz : F n z = 0
⊢ ∃ z ∈ s, F n z = 0
Tactic:
refine ⟨z, h9 (ball_subset_closedBall hz), hFnz⟩
State after:
no goals

State before:
ι : 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
⊢ ∀ z ∈ sphere z₀ r, f z ≠ 0
Tactic:
exact λ z hz => h5 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz hr.lt.ne.symm)
State after:
no goals