Theorem: two_le_order_of_deriv_eq_zero (RMT4/deriv_inj.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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