internlm/Lean-Github huggingface dataset:
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H6 : ∀ᶠ n in p, ContinuousOn (deriv (F n)) (sphere z₀ r) := by
  filter_upwards [hF] with n h using (h.deriv hU).continuousOn.mono hr2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 (hf.deriv hF hU) _ hr2 H1
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H8 : ContinuousOn (deriv f) (sphere z₀ r) :=
  (H3.deriv hU).continuousOn.mono hr2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
refine Tendsto.const_mul _ (TendstoUniformlyOn.tendsto_circle_integral hr1 ?_ ?_)
Proof state after:
case refine_1
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (fun z => deriv (F n) z / F n z) (sphere z₀ r)

case refine_2
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ TendstoUniformlyOn (fun k z => deriv (F k) z / F k z) (fun z => deriv f z / f z) p (sphere z₀ r)
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
Tactic:
filter_upwards [hF] with n h using h.continuousOn.mono hr2
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
Tactic:
filter_upwards [hF] with n h using (h.deriv hU).continuousOn.mono hr2
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
case refine_1
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (fun z => deriv (F n) z / F n z) (sphere z₀ r)
Tactic:
filter_upwards [hurwitz2_1 H1 H2 H4 hf1, H6, H5] with n hn H6 H5 using ContinuousOn.div H6 H5 hn
Proof state after:
no goals
Theorem: hurwitz2_2
Proof state before:
case refine_2
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ TendstoUniformlyOn (fun k z => deriv (F k) z / F k z) (fun z => deriv f z / f z) p (sphere z₀ r)
Tactic:
exact TendstoUniformlyOn.div_of_compact H7 H2 H8 H4 hf1 H1
Proof state after:
no goals
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
by_cases h : NeBot p
Proof state after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
case neg => simp at h; simp [h]
Proof state after:
no goals
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
case pos =>
  have H1 : IsCompact (sphere z₀ r) := isCompact_sphere z₀ r
  have H2 : sphere z₀ r ⊆ U := sphere_subset_closedBall.trans hr2
  have H3 : TendstoUniformlyOn F f p (sphere z₀ r) :=
    (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 hf _ H2 H1
  have H4 : ContinuousOn f (sphere z₀ r) :=
    (hf.differentiableOn hF hU).continuousOn.mono H2
  have H5 : ∀ᶠ n in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0 := hurwitz2_1 H1 H3 H4 hf1
  filter_upwards [(hurwitz2_2 hU hF hf hr1 H2 hf1).eventually_ne hf2, H5, hF] with n h h' hF
  contrapose! h
  have : ∀ (z : ℂ), z ∈ ball z₀ r ∪ sphere z₀ r → F n z ≠ 0 := λ z hz => hz.casesOn (h z) (h' z)
  refine cindex_eq_zero hU hr1 hr2 hF (by rwa [← ball_union_sphere])
Proof state after:
no goals
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : ¬NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
simp at h
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : p = ⊥
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : p = ⊥
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
have H1 : IsCompact (sphere z₀ r) := isCompact_sphere z₀ r
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
have H2 : sphere z₀ r ⊆ U := sphere_subset_closedBall.trans hr2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
have H3 : TendstoUniformlyOn F f p (sphere z₀ r) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 hf _ H2 H1
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
have H4 : ContinuousOn f (sphere z₀ r) :=
  (hf.differentiableOn hF hU).continuousOn.mono H2
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
have H5 : ∀ᶠ n in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0 := hurwitz2_1 H1 H3 H4 hf1
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
filter_upwards [(hurwitz2_2 hU hF hf hr1 H2 hf1).eventually_ne hf2, H5, hF] with n h h' hF
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h : (cindex z₀ r ∘ fun n => F n) n ≠ 0
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
⊢ ∃ z ∈ ball z₀ r, F n z = 0
Theorem: hurwitz2
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h : (cindex z₀ r ∘ fun n => F n) n ≠ 0
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
⊢ ∃ z ∈ ball z₀ r, F n z = 0
Tactic:
contrapose! h
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0
Theorem: hurwitz2
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0
Tactic:
have : ∀ (z : ℂ), z ∈ ball z₀ r ∪ sphere z₀ r → F n z ≠ 0 := λ z hz => hz.casesOn (h z) (h' z)
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
this : ∀ z ∈ ball z₀ r ∪ sphere z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0
Theorem: hurwitz2
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
this : ∀ z ∈ ball z₀ r ∪ sphere z₀ r, F n z ≠ 0
⊢ (cindex z₀ r ∘ fun n => F n) n = 0
Tactic:
refine cindex_eq_zero hU hr1 hr2 hF (by rwa [← ball_union_sphere])
Proof state after:
no goals
Theorem: hurwitz2
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF✝ : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : closedBall z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
hf2 : cindex z₀ r f ≠ 0
h✝ : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : sphere z₀ r ⊆ U
H3 : TendstoUniformlyOn F f p (sphere z₀ r)
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ∀ z ∈ sphere z₀ r, F n z ≠ 0
n : ι
h' : ∀ z ∈ sphere z₀ r, F n z ≠ 0
hF : DifferentiableOn ℂ (F n) U
h : ∀ z ∈ ball z₀ r, F n z ≠ 0
this : ∀ z ∈ ball z₀ r ∪ sphere z₀ r, F n z ≠ 0
⊢ ∀ z ∈ closedBall z₀ r, (fun n => F n) n z ≠ 0
Tactic:
rwa [← ball_union_sphere]
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₀
⊢ ∀ᶠ (n : ι) in p, ∃ z ∈ s, F n z = 0
Tactic:
by_cases h : NeBot p
Proof 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