internlm/Lean-Github huggingface dataset:
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
have e2 := hp.locally_ne_zero h17
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
have e3 := hq.locally_ne_zero h26
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
e3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, deriv g z ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
e3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, deriv g z ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
have e4 := hU.eventually_mem hz₀
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
e3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, deriv g z ≠ 0
e4 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ U
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
e3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, deriv g z ≠ 0
e4 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ U
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
simp only [eventually_nhdsWithin_iff, mem_compl_singleton_iff] at e2 e3
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e4 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ U
e2 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → g x ≠ 0
e3 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → deriv g x ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e4 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ U
e2 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → g x ≠ 0
e3 : ∀ᶠ (x : ℂ) in 𝓝 z₀, x ≠ z₀ → deriv g x ≠ 0
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
simp only [eventually_nhds_iff_eventually_closed_ball] at e2 e3 e4
Proof state after:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
e3 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
e4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ U
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
h26 : q ≠ 0
e1 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
e2 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
e3 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
e4 : ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ z ∈ closedBall z₀ r, z ∈ U
⊢ ∃ r > 0,
    cindex z₀ r g = ↑(FormalMultilinearSeries.order p) ∧
      (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧ (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧ closedBall z₀ r ⊆ U
Tactic:
exact (e1.and (e3.and (e2.and e4))).exists'
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
q : FormalMultilinearSeries ℂ ℂ ℂ
hq : HasFPowerSeriesAt (deriv g) q z₀
⊢ q ≠ 0
Tactic:
rintro rfl
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
hq : HasFPowerSeriesAt (deriv g) 0 z₀
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
hq : HasFPowerSeriesAt (deriv g) 0 z₀
⊢ False
Tactic:
simpa [hgz₀] using (((bla ⟨p, hp⟩ hq).filter_mono nhdsWithin_le_nhds).and h25).exists
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
⊢ ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
Tactic:
have h24 : p.order ≠ 0 := by linarith
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
⊢ ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
⊢ ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
Tactic:
have := hurwitz2 hU (eventually_of_forall h18) h19 h7 h20 h22 (by simp [h8, h24])
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (n : ℂ) in 𝓝[≠] 0, ∃ z ∈ ball z₀ r, g z + n = 0
⊢ ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (n : ℂ) in 𝓝[≠] 0, ∃ z ∈ ball z₀ r, g z + n = 0
⊢ ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
Tactic:
simp only [eventually_nhdsWithin_iff] at this ⊢
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → (cindex z₀ r fun z => g z + x) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → (cindex z₀ r fun z => g z + x) = 1
Tactic:
filter_upwards [this] with ε h hε
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
⊢ (cindex z₀ r fun z => g z + ε) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
⊢ (cindex z₀ r fun z => g z + ε) = 1
Tactic:
obtain ⟨z, hz, hgz⟩ := h hε
Proof state after:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
⊢ (cindex z₀ r fun z => g z + ε) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
⊢ (cindex z₀ r fun z => g z + ε) = 1
Tactic:
have e1 : z ≠ z₀ := by rintro rfl; rw [hgz₀, zero_add] at hgz; exact hε hgz
Proof state after:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
⊢ (cindex z₀ r fun z => g z + ε) = 1
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
⊢ (cindex z₀ r fun z => g z + ε) = 1
Tactic:
have e2 : deriv (λ z => g z + ε) z ≠ 0 := by simpa using h14 z (ball_subset_closedBall hz) e1
Proof state after:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
⊢ (cindex z₀ r fun z => g z + ε) = 1