Theorem: local_hurwitz (RMT4/hurwitz.lean)

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

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

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

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

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

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

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

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

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

State before:
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
Tactic:
cases F_noz n z (h2 (ball_subset_closedBall (mem_ball.mpr h5))) h6
State after:
no goals

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
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 > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
Tactic:
rw [eventually_nhdsWithin_iff, eventually_nhds_iff_eventually_closed_ball] at h
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
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0

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
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
Tactic:
have h4 := cindex_eventually_eq_order hp
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
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0

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
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
Tactic:
have h5 : ∀ᶠ 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 : 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0

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
h : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
Tactic:
obtain ⟨r, h6, h7, h8, h9⟩ := (h.and (h4.and h5)).exists'
State after:
case 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0

State before:
case 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ ∃ r > 0, closedBall z₀ r ⊆ U ∧ (∀ z ∈ sphere z₀ r, f z ≠ 0) ∧ cindex z₀ r f ≠ 0
Tactic:
refine ⟨r, h6, h9, ?_, ?_⟩
State after:
case intro.intro.intro.intro.refine_1
ι : 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ ∀ z ∈ sphere z₀ r, f z ≠ 0

case intro.intro.intro.intro.refine_2
ι : 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ cindex z₀ r f ≠ 0

State before:
case intro.intro.intro.intro.refine_1
ι : 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ ∀ z ∈ sphere z₀ r, f z ≠ 0
Tactic:
exact λ z hz => h7 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz h6.lt.ne.symm)
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2
ι : 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 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
pf : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f pf z₀
hh : ∃ᶠ (x : ℂ) in 𝓝 z₀, ¬f x = 0
h1 : 0 < FormalMultilinearSeries.order pf
h4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h5 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, closedBall z₀ r ⊆ U
r : ℝ
h6 : r > 0
h7 : ∀ z ∈ closedBall z₀ r, z ∈ {z₀}ᶜ → f z ≠ 0
h8 : cindex z₀ r f = ↑(FormalMultilinearSeries.order pf)
h9 : closedBall z₀ r ⊆ U
⊢ cindex z₀ r f ≠ 0
Tactic:
simp [h8, h1.ne.symm]
State after:
no goals