internlm/Lean-Github huggingface dataset:
Theorem: crucial
Proof state before:
case e_a.hg.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ContinuousOn (fun z => g z) (sphere c r)
Tactic:
exact h1.continuousOn.mono (sphere_subset_closedBall.trans hcr)
Proof state after:
no goals
Theorem: crucial
Proof state before:
case e_a.hg.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ∀ x ∈ sphere c r, g x ≠ 0
Tactic:
exact λ z hz => h2 z (sphere_subset_closedBall hz)
Proof state after:
no goals
Theorem: bla
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
have h1 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).mem_nhds hf
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Theorem: bla
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
obtain ⟨ε, hε, h⟩ := Metric.mem_nhds_iff.1 (h1.and hf'.eventually_eq_zero)
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Theorem: bla
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
refine Metric.mem_nhds_iff.2 ⟨ε, hε, λ z hz => ?_⟩
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Theorem: bla
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
have h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0 := by
  rintro z hz
  rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hz) ((h hz).1.differentiableAt)]
  ext1
  simpa [fderiv_deriv] using (h hz).2
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Theorem: bla
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
have h4 : DifferentiableOn ℂ f (ball z₀ ε) := λ z hz => (h hz).1.differentiableWithinAt
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
h4 : DifferentiableOn ℂ f (ball z₀ ε)
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Theorem: bla
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
h4 : DifferentiableOn ℂ f (ball z₀ ε)
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
exact Convex.is_const_of_fderivWithin_eq_zero (convex_ball z₀ ε) h4 h3 hz (mem_ball_self hε)
Proof state after:
no goals
Theorem: bla
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
Tactic:
rintro z hz
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderivWithin ℂ f (ball z₀ ε) z = 0
Theorem: bla
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderivWithin ℂ f (ball z₀ ε) z = 0
Tactic:
rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hz) ((h hz).1.differentiableAt)]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderiv ℂ f z = 0
Theorem: bla
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderiv ℂ f z = 0
Tactic:
ext1
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ (fderiv ℂ f z) 1 = 0 1
Theorem: bla
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ (fderiv ℂ f z) 1 = 0 1
Tactic:
simpa [fderiv_deriv] using (h hz).2
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Tactic:
classical
have h1 : p.coeff 1 = 0 := by simpa only [hg'] using hgp.deriv.symm
have h2 : p 0 = 0 := by ext1 x; simpa only [hg] using hgp.coeff_zero x
have h3 : p 1 = 0 := by ext1; simp [h1]
rw [FormalMultilinearSeries.order_eq_find' hp, Nat.le_find_iff]
intro n hn
cases n
case zero => simp [h2]
case succ n =>
  cases n
  case zero => simpa using h3
  case succ => linarith
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Tactic:
have h1 : p.coeff 1 = 0 := by simpa only [hg'] using hgp.deriv.symm
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Tactic:
have h2 : p 0 = 0 := by ext1 x; simpa only [hg] using hgp.coeff_zero x
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Tactic:
have h3 : p 1 = 0 := by ext1; simp [h1]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
⊢ 2 ≤ FormalMultilinearSeries.order p
Tactic:
rw [FormalMultilinearSeries.order_eq_find' hp, Nat.le_find_iff]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
⊢ ∀ m < 2, ¬p m ≠ 0 m
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
⊢ ∀ m < 2, ¬p m ≠ 0 m
Tactic:
intro n hn
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n : ℕ
hn : n < 2
⊢ ¬p n ≠ 0 n
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n : ℕ
hn : n < 2
⊢ ¬p n ≠ 0 n
Tactic:
cases n
Proof state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.zero < 2
⊢ ¬p Nat.zero ≠ 0 Nat.zero

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n✝ : ℕ
hn : Nat.succ n✝ < 2
⊢ ¬p (Nat.succ n✝) ≠ 0 (Nat.succ n✝)
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.zero < 2
⊢ ¬p Nat.zero ≠ 0 Nat.zero
Tactic:
case zero => simp [h2]
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n : ℕ
hn : Nat.succ n < 2
⊢ ¬p (Nat.succ n) ≠ 0 (Nat.succ n)
Tactic:
case succ n =>
  cases n
  case zero => simpa using h3
  case succ => linarith
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
⊢ FormalMultilinearSeries.coeff p 1 = 0
Tactic:
simpa only [hg'] using hgp.deriv.symm
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
⊢ p 0 = 0
Tactic:
ext1 x
Proof state after:
case H
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
x : Fin 0 → ℂ
⊢ (p 0) x = 0 x
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
case H
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
x : Fin 0 → ℂ
⊢ (p 0) x = 0 x
Tactic:
simpa only [hg] using hgp.coeff_zero x
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
⊢ p 1 = 0
Tactic:
ext1
Proof state after:
case H
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
x✝ : Fin 1 → ℂ
⊢ (p 1) x✝ = 0 x✝
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
case H
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
x✝ : Fin 1 → ℂ
⊢ (p 1) x✝ = 0 x✝
Tactic:
simp [h1]
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.zero < 2
⊢ ¬p Nat.zero ≠ 0 Nat.zero
Tactic:
simp [h2]
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n : ℕ
hn : Nat.succ n < 2
⊢ ¬p (Nat.succ n) ≠ 0 (Nat.succ n)
Tactic:
cases n
Proof state after:
case zero
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.succ Nat.zero < 2
⊢ ¬p (Nat.succ Nat.zero) ≠ 0 (Nat.succ Nat.zero)

case succ
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n✝ : ℕ
hn : Nat.succ (Nat.succ n✝) < 2
⊢ ¬p (Nat.succ (Nat.succ n✝)) ≠ 0 (Nat.succ (Nat.succ n✝))
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.succ Nat.zero < 2
⊢ ¬p (Nat.succ Nat.zero) ≠ 0 (Nat.succ Nat.zero)
Tactic:
case zero => simpa using h3
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n✝ : ℕ
hn : Nat.succ (Nat.succ n✝) < 2
⊢ ¬p (Nat.succ (Nat.succ n✝)) ≠ 0 (Nat.succ (Nat.succ n✝))
Tactic:
case succ => linarith
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
hn : Nat.succ Nat.zero < 2
⊢ ¬p (Nat.succ Nat.zero) ≠ 0 (Nat.succ Nat.zero)
Tactic:
simpa using h3
Proof state after:
no goals
Theorem: two_le_order_of_deriv_eq_zero
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hgp : HasFPowerSeriesAt g p z₀
hp : p ≠ 0
hg : g z₀ = 0
hg' : deriv g z₀ = 0
h1 : FormalMultilinearSeries.coeff p 1 = 0
h2 : p 0 = 0
h3 : p 1 = 0
n✝ : ℕ
hn : Nat.succ (Nat.succ n✝) < 2
⊢ ¬p (Nat.succ (Nat.succ n✝)) ≠ 0 (Nat.succ (Nat.succ n✝))
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_uniformly_on_add_const
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
have : Tendsto id (𝓝[≠] (0 : ℂ)) (𝓝 0) := nhdsWithin_le_nhds
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this : Tendsto id (𝓝[≠] 0) (𝓝 0)
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Theorem: tendsto_uniformly_on_add_const
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this : Tendsto id (𝓝[≠] 0) (𝓝 0)
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
have : TendstoUniformlyOn (λ (ε _ : ℂ) => ε) 0 (𝓝[≠] 0) U := this.tendstoUniformlyOn_const U
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this✝ : Tendsto id (𝓝[≠] 0) (𝓝 0)
this : TendstoUniformlyOn (fun ε x => ε) 0 (𝓝[≠] 0) U
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Theorem: tendsto_uniformly_on_add_const
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this✝ : Tendsto id (𝓝[≠] 0) (𝓝 0)
this : TendstoUniformlyOn (fun ε x => ε) 0 (𝓝[≠] 0) U
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
simpa using tendsto_uniformly_on_const.add this
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
⊢ deriv g z₀ ≠ 0
Tactic:
obtain ⟨p, hp⟩ : AnalyticAt ℂ g z₀ := hg.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₀
⊢ deriv g z₀ ≠ 0
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₀
⊢ 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₀
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
⊢ deriv g z₀ ≠ 0
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
⊢ deriv g z₀ ≠ 0
Tactic:
have h17 : p ≠ 0 := by
  simpa [← hp.locally_zero_iff.not] using h25.frequently.filter_mono nhdsWithin_le_nhds
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
⊢ deriv g z₀ ≠ 0