case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1

case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
p : ℝ[X]
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
cases' eq_or_ne (derivative p) 0 with hp' hp'
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : x ∈ Multiset.toFinset (roots p)
y : ℝ
hy : y ∈ Multiset.toFinset (roots p)
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
refine' Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => _
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : x ∈ Multiset.toFinset (roots p)
y : ℝ
hy : y ∈ Multiset.toFinset (roots p)
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
z : ℝ
hz1 : z ∈ Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
case inr
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
obtain ⟨z, hz1, hz2⟩ :=
  exists_deriv_eq_zero (fun x : ℝ => eval x p) hxy p.continuousOn (hx.trans hy.symm)
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
z : ℝ
hz1 : z ∈ Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ Multiset.toFinset (roots (↑derivative p))
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
z : ℝ
hz1 : z ∈ Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
refine' ⟨z, _, hz1⟩
no goals
case inr.intro.intro
p : ℝ[X]
hp' : ↑derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : IsRoot p x
y : ℝ
hy : IsRoot p y
hxy : x < y
hxy' : ∀ (z : ℝ), z ∈ Multiset.toFinset (roots p) → ¬z ∈ Ioo x y
z : ℝ
hz1 : z ∈ Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ Multiset.toFinset (roots (↑derivative p))
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ 0 ≤ Finset.card (Multiset.toFinset (roots (↑derivative (↑C (coeff p 0)))) \ ∅) + 1
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
no goals
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ 0 ≤ Finset.card (Multiset.toFinset (roots (↑derivative (↑C (coeff p 0)))) \ ∅) + 1
exact zero_le _
no goals
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ ↑derivative p ≠ ↑derivative 0
rwa [derivative_zero]