-- Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean
theorem card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : ℝ[X]) :
    p.roots.toFinset.card ≤ (p.derivative.roots.toFinset \ p.roots.toFinset).card + 1

Proof state:
p : ℝ[X]
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'

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

case inr
p : ℝ[X]
hp' : derivative p ≠ 0
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Proof state:
case inr.intro.intro
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ (derivative p).roots.toFinset

Tactic:
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]

Result:
no goals

Proof state:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Tactic:
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])

Result:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Proof state:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
⊢ p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1

Tactic:
refine Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => ?_

Result:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : x ∈ p.roots.toFinset
y : ℝ
hy : y ∈ p.roots.toFinset
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

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

Tactic:
rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]

Result:
case inl
p : ℝ[X]
hp' : derivative p = 0
⊢ 0 ≤ ((derivative (C (p.coeff 0))).roots.toFinset \ ∅).card + 1

Proof state:
p : ℝ[X]
hp' : derivative p ≠ 0
⊢ derivative p ≠ derivative 0

Tactic:
rwa [derivative_zero]

Result:
no goals

Proof state:
case inl
p : ℝ[X]
hp' : derivative p = 0
⊢ 0 ≤ ((derivative (C (p.coeff 0))).roots.toFinset \ ∅).card + 1

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : x ∈ p.roots.toFinset
y : ℝ
hy : y ∈ p.roots.toFinset
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

Tactic:
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy

Result:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

Proof state:
case inr
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)

Result:
case inr.intro.intro
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

Proof state:
case inr.intro.intro
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y

Tactic:
refine ⟨z, ?_, hz1⟩

Result:
case inr.intro.intro
p : ℝ[X]
hp' : derivative p ≠ 0
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ (derivative p).roots.toFinset