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
⊢ deriv g z₀ ≠ 0
Tactic:
by_contra h
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
⊢ False
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
⊢ False
Tactic:
have h6 : 2 ≤ p.order := two_le_order_of_deriv_eq_zero hp h17 hgz₀ h
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
⊢ False
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
⊢ False
Tactic:
obtain ⟨r, h7, h8, h14, h21, h20⟩ : ∃ r > 0,
    cindex z₀ r g = p.order ∧
    (∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0) ∧
    (∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0) ∧
    closedBall z₀ r ⊆ U
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 > 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

case intro.intro.intro.intro.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
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0 :=
  λ z hz => h21 z (sphere_subset_closedBall hz) (ne_of_mem_sphere hz h7.lt.ne.symm)
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have h18 : ∀ ε, DifferentiableOn ℂ (λ z => g z + ε) U := λ ε => hg.add_const ε
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have h19 : TendstoLocallyUniformlyOn (λ ε z => g z + ε) g (𝓝[≠] 0) U :=
  tendsto_uniformly_on_add_const.tendstoLocallyUniformlyOn
Proof state after:
case intro.intro.intro.intro.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
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
⊢ False
Tactic:
have h9 : ∀ᶠ ε in 𝓝[≠] 0, cindex z₀ r (λ z => g z + ε) = 1 := by
  have h24 : p.order ≠ 0 := by linarith
  have := hurwitz2 hU (eventually_of_forall h18) h19 h7 h20 h22 (by simp [h8, h24])
  simp only [eventually_nhdsWithin_iff] at this ⊢
  filter_upwards [this] with ε h hε
  obtain ⟨z, hz, hgz⟩ := h hε
  have e1 : z ≠ z₀ := by rintro rfl; rw [hgz₀, zero_add] at hgz; exact hε hgz
  have e2 : deriv (λ z => g z + ε) z ≠ 0 := by simpa using h14 z (ball_subset_closedBall hz) e1
  refine crucial hU h20 hz (h18 ε) hgz e2 (λ w hw hwz => ?_)
  contrapose! hwz
  exact hi (h20 hw) ((ball_subset_closedBall.trans h20) hz) (add_right_cancel (hwz.trans hgz.symm))
Proof state after:
case intro.intro.intro.intro.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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
⊢ False
Tactic:
have h10 : Tendsto (λ ε => cindex z₀ r (λ z => g z + ε)) (𝓝[≠] 0) (𝓝 (cindex z₀ r g)) :=
  hurwitz2_2 hU (eventually_of_forall h18) h19 h7 (sphere_subset_closedBall.trans h20) h22
Proof state after:
case intro.intro.intro.intro.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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
⊢ False
Tactic:
rw [tendsto_nhds_unique (Tendsto.congr' h9 h10) tendsto_const_nhds] at h8
Proof state after:
case intro.intro.intro.intro.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 : 1 = ↑(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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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 : 1 = ↑(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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
⊢ False
Tactic:
norm_cast at h8
Proof state after:
case intro.intro.intro.intro.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
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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
h8 : 1 = FormalMultilinearSeries.order p
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case intro.intro.intro.intro.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
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
h9 : ∀ᶠ (ε : ℂ) in 𝓝[≠] 0, (cindex z₀ r fun z => g z + ε) = 1
h10 : Tendsto (fun ε => cindex z₀ r fun z => g z + ε) (𝓝[≠] 0) (𝓝 (cindex z₀ r g))
h8 : 1 = FormalMultilinearSeries.order p
⊢ False
Tactic:
linarith
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₀
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
Tactic:
simp only [eventually_nhdsWithin_iff]
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₀
⊢ ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ {z₀}ᶜ → g x ≠ 0
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₀
⊢ ∀ᶠ (x : ℂ) in 𝓝 z₀, x ∈ {z₀}ᶜ → g x ≠ 0
Tactic:
filter_upwards [hU.eventually_mem hz₀] with z hz hzz₀
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₀
z : ℂ
hz : z ∈ U
hzz₀ : z ∈ {z₀}ᶜ
⊢ g z ≠ 0
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₀
z : ℂ
hz : z ∈ U
hzz₀ : z ∈ {z₀}ᶜ
⊢ g z ≠ 0
Tactic:
simpa only [hgz₀] using hi.ne hz hz₀ hzz₀
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
⊢ p ≠ 0
Tactic:
simpa [← hp.locally_zero_iff.not] using h25.frequently.filter_mono nhdsWithin_le_nhds
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 > 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:
obtain ⟨q, hq⟩ : AnalyticAt ℂ (deriv g) z₀ := (hg.deriv hU).analyticAt (hU.mem_nhds 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₀
⊢ ∃ 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₀
⊢ ∃ 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 h26 : q ≠ 0 := by
  rintro rfl
  simpa [hgz₀] using (((bla ⟨p, hp⟩ hq).filter_mono nhdsWithin_le_nhds).and h25).exists
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
⊢ ∃ 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
⊢ ∃ 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 e1 := cindex_eventually_eq_order hp
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)
⊢ ∃ 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