Theorem: deriv_ne_zero_of_inj_aux (RMT4/deriv_inj.lean)

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
⊢ deriv g z₀ ≠ 0
Tactic:
obtain ⟨p, hp⟩ : AnalyticAt ℂ g z₀ := hg.analyticAt (hU.mem_nhds hz₀)
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₀
⊢ deriv g z₀ ≠ 0

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₀
⊢ deriv g z₀ ≠ 0
Tactic:
have h25 : ∀ᶠ z in 𝓝[≠] z₀, g z ≠ 0 := by
  simp only [eventually_nhdsWithin_iff]
  filter_upwards [hU.eventually_mem hz₀] with z hz hzz₀
  simpa only [hgz₀] using hi.ne hz hz₀ hzz₀
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
⊢ deriv g z₀ ≠ 0

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
⊢ deriv g z₀ ≠ 0
Tactic:
have h17 : p ≠ 0 := by
  simpa [← hp.locally_zero_iff.not] using h25.frequently.filter_mono nhdsWithin_le_nhds
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
⊢ deriv g z₀ ≠ 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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₀
e2 : deriv (fun z => g z + ε) z ≠ 0
⊢ (cindex z₀ r fun z => g z + ε) = 1
Tactic:
refine crucial hU h20 hz (h18 ε) hgz e2 (λ w hw hwz => ?_)
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
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : w ≠ z
⊢ g w + ε ≠ 0

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₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : w ≠ z
⊢ g w + ε ≠ 0
Tactic:
contrapose! hwz
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
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : g w + ε = 0
⊢ w = z

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₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : g w + ε = 0
⊢ w = z
Tactic:
exact hi (h20 hw) ((ball_subset_closedBall.trans h20) hz) (add_right_cancel (hwz.trans hgz.symm))
State after:
no goals

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
⊢ FormalMultilinearSeries.order p ≠ 0
Tactic:
linarith
State after:
no goals

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
⊢ cindex z₀ r g ≠ 0
Tactic:
simp [h8, h24]
State after:
no goals

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
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
⊢ z ≠ z₀
Tactic:
rintro rfl
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : g z + ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : g z + ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Tactic:
rw [hgz₀, zero_add] at hgz
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Tactic:
exact hε hgz
State after:
no goals

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
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
⊢ deriv (fun z => g z + ε) z ≠ 0
Tactic:
simpa using h14 z (ball_subset_closedBall hz) e1
State after:
no goals