Theorem: hurwitz2 (RMT4/hurwitz.lean)

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
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

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]
State after:
no goals

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])
State after:
no goals

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
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

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]
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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)
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

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])
State after:
no goals

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]
State after:
no goals