Theorem: hurwitz (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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 ∈ U, f z = 0
Tactic:
have := local_hurwitz hU F_holo F_noz F_conv hz₀ hfz₀
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ ∀ z ∈ U, f z = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
⊢ ∀ z ∈ U, f z = 0
Tactic:
have h1 : DifferentiableOn ℂ f U := F_conv.differentiableOn F_holo hU
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
h1 : DifferentiableOn ℂ f U
⊢ ∀ z ∈ U, f z = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
h1 : DifferentiableOn ℂ f U
⊢ ∀ z ∈ U, f z = 0
Tactic:
have h2 := h1.analyticOn hU
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
h1 : DifferentiableOn ℂ f U
h2 : AnalyticOn ℂ f U
⊢ ∀ z ∈ U, f z = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected 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
this : ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
h1 : DifferentiableOn ℂ f U
h2 : AnalyticOn ℂ f U
⊢ ∀ z ∈ U, f z = 0
Tactic:
exact h2.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU' hz₀ this
State after:
no goals