internlm/Lean-Github huggingface dataset:
Theorem: hurwitz3
Proof 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]
Proof state after:
no goals
Theorem: hurwitz3
Proof 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⟩
Proof state after:
no goals
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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]
Proof state after:
no goals
Theorem: hurwitz3
Proof 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₀)
Proof 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
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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
Proof 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
Theorem: hurwitz3
Proof 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'
Proof 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
Theorem: hurwitz3
Proof 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)
Proof 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
Theorem: hurwitz3
Proof 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 ?_
Proof 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
Theorem: hurwitz3
Proof 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⟩
Proof 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
Theorem: hurwitz3
Proof 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⟩
Proof state after:
no goals
Theorem: hurwitz3
Proof 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)
Proof state after:
no goals
Theorem: local_hurwitz
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
have H1 := (F_conv.differentiableOn F_holo hU).analyticAt (hU.mem_nhds hz₀)
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Theorem: local_hurwitz
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
cases H1.eventually_eq_zero_or_eventually_ne_zero
Proof state after:
case inl
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
h✝ : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0

case inr
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
h✝ : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Theorem: local_hurwitz
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
h✝ : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
case inl => assumption
Proof state after:
no goals
Theorem: local_hurwitz
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
h✝ : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: local_hurwitz
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
H1 : AnalyticAt ℂ f z₀
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
obtain ⟨pf, hp⟩ := H1
Proof state after:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Theorem: local_hurwitz
Proof state before:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
by_contra hh
Proof state after:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ False
Theorem: local_hurwitz
Proof state before:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ False
Tactic:
rw [Filter.not_eventually] at hh
Proof state after:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
⊢ False
Theorem: local_hurwitz
Proof state before:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
⊢ False
Tactic:
have h1 := (order_pos_iff hp hfz₀).2 hh
Proof state after:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
⊢ False
Theorem: local_hurwitz
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r✝ : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1✝ : 0 < FormalMultilinearSeries.order pf
r : ℝ
h1 : r > 0
h2 : closedBall z₀ r ⊆ U
h3 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h4 : cindex z₀ r f ≠ 0
⊢ False
Tactic:
obtain ⟨n, z, h5, h6⟩ := (hurwitz2 hU F_holo F_conv h1 h2 h3 h4).exists
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r✝ : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0
F_conv : TendstoLocallyUniformlyOn F f p U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
h : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1✝ : 0 < FormalMultilinearSeries.order pf
r : ℝ
h1 : r > 0
h2 : closedBall z₀ r ⊆ U
h3 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h4 : cindex z₀ r f ≠ 0
n : ι
z : ℂ
h5 : z ∈ ball z₀ r
h6 : F n z = 0
⊢ False