internlm/Lean-Github huggingface dataset:
Theorem: local_hurwitz
Proof 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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'
Proof 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
Theorem: local_hurwitz
Proof 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, ?_, ?_⟩
Proof 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
Theorem: local_hurwitz
Proof 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)
Proof state after:
no goals
Theorem: local_hurwitz
Proof 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]
Proof state after:
no goals
Theorem: hurwitz
Proof 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₀
Proof 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
Theorem: hurwitz
Proof 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
Proof 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
Theorem: hurwitz
Proof 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
Proof 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
Theorem: hurwitz
Proof 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
Proof state after:
no goals
Theorem: hurwitz'
Proof 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
⊢ (∀ z ∈ U, f z ≠ 0) ∨ ∀ z ∈ U, f z = 0
Tactic:
refine or_iff_not_imp_left.mpr (λ h => ?_)
Proof 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
h : ¬∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, f z = 0
Theorem: hurwitz'
Proof 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
h : ¬∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, f z = 0
Tactic:
push_neg at h
Proof 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
h : ∃ z ∈ U, f z = 0
⊢ ∀ z ∈ U, f z = 0
Theorem: hurwitz'
Proof 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
h : ∃ z ∈ U, f z = 0
⊢ ∀ z ∈ U, f z = 0
Tactic:
obtain ⟨z₀, h1, h2⟩ := h
Proof state after:
case intro.intro
ι : 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
z₀ : ℂ
h1 : z₀ ∈ U
h2 : f z₀ = 0
⊢ ∀ z ∈ U, f z = 0
Theorem: hurwitz'
Proof state before:
case intro.intro
ι : 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
z₀ : ℂ
h1 : z₀ ∈ U
h2 : f z₀ = 0
⊢ ∀ z ∈ U, f z = 0
Tactic:
exact hurwitz hU hU' F_holo F_noz F_conv h1 h2
Proof state after:
no goals
Theorem: hurwitz_1
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
⊢ EqOn f 0 U ∨ ∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
Tactic:
refine or_iff_not_imp_right.2 (λ h => ?_)
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ EqOn f 0 U
Theorem: hurwitz_1
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ EqOn f 0 U
Tactic:
obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ U, ∃ᶠ z in 𝓝[≠] z₀, f z = 0 := by simpa [not_forall] using h
Proof state after:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
z₀ : ℂ
h1 : z₀ ∈ U
h2 : ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U
Theorem: hurwitz_1
Proof state before:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
z₀ : ℂ
h1 : z₀ ∈ U
h2 : ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U
Tactic:
exact (hf.analyticOn hU).eqOn_zero_of_preconnected_of_frequently_eq_zero hU' h1 h2
Proof state after:
no goals
Theorem: hurwitz_1
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
h : ¬∀ z₀ ∈ U, ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∃ z₀ ∈ U, ∃ᶠ (z : ℂ) in 𝓝[≠] z₀, f z = 0
Tactic:
simpa [not_forall] using h
Proof state after:
no goals
Theorem: hurwitz_inj
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
⊢ (∃ w, ∀ z ∈ U, f z = w) ∨ InjOn f U
Tactic:
refine or_iff_not_imp_right.2 (λ h => ?_)
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
⊢ ∃ w, ∀ z ∈ U, f z = w
Theorem: hurwitz_inj
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
obtain ⟨x, hx, y, hy, hfxy, hxy⟩ : ∃ x ∈ U, ∃ y ∈ U, f x = f y ∧ x ≠ y := by
  simp [InjOn] at h
  obtain ⟨x, h1, y, h2, h3, h4⟩ := h
  refine ⟨x, h1, y, h3, h2, h4⟩
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
⊢ ∃ w, ∀ z ∈ U, f z = w
Theorem: hurwitz_inj
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
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
set g : ℂ → ℂ := λ z => f z - f x
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
⊢ ∃ w, ∀ z ∈ U, f z = w
Theorem: hurwitz_inj
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
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
set G : ι → ℂ → ℂ := λ n z => F n z - f x
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
⊢ ∃ w, ∀ z ∈ U, f z = w
Theorem: hurwitz_inj
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
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hG : ∀ᶠ n in p, DifferentiableOn ℂ (G n) U := by
  filter_upwards [hF] with n hF using hF.sub (differentiableOn_const _)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
hG : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
⊢ ∃ w, ∀ z ∈ U, f z = w
Theorem: hurwitz_inj
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
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
hG : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
⊢ ∃ w, ∀ z ∈ U, f z = w
Tactic:
have hg : TendstoLocallyUniformlyOn G g p U :=
  hurwitz4 hf (uniformContinuous_id.sub uniformContinuous_const)
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
inst✝ : NeBot p
hU : IsOpen U
hU' : IsPreconnected U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hi : ∃ᶠ (n : ι) in p, InjOn (F n) U
h : ¬InjOn f U
x : ℂ
hx : x ∈ U
y : ℂ
hy : y ∈ U
hfxy : f x = f y
hxy : x ≠ y
g : ℂ → ℂ := fun z => f z - f x
G : ι → ℂ → ℂ := fun n z => F n z - f x
hG : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (G n) U
hg : TendstoLocallyUniformlyOn G g p U
⊢ ∃ w, ∀ z ∈ U, f z = w