[GOAL]
p : ℝ[X]
⊢ Finset.card (Multiset.toFinset (roots p)) ≤
    Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1
[PROOFSTEP]
cases' eq_or_ne (derivative p) 0 with hp' hp'
[GOAL]
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
[PROOFSTEP]
rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
[GOAL]
case inl
p : ℝ[X]
hp' : ↑derivative p = 0
⊢ 0 ≤ Finset.card (Multiset.toFinset (roots (↑derivative (↑C (coeff p 0)))) \ ∅) + 1
[PROOFSTEP]
exact zero_le _
[GOAL]
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
[PROOFSTEP]
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
[GOAL]
p : ℝ[X]
hp' : ↑derivative p ≠ 0
⊢ ↑derivative p ≠ ↑derivative 0
[PROOFSTEP]
rwa [derivative_zero]
[GOAL]
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
[PROOFSTEP]
refine' Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => _
[GOAL]
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 ∈ Set.Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy 
[GOAL]
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 ∈ Set.Ioo x y
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
[GOAL]
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 ∈ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ ∃ z, z ∈ Multiset.toFinset (roots (↑derivative p)) ∧ x < z ∧ z < y
[PROOFSTEP]
refine' ⟨z, _, hz1⟩
[GOAL]
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 ∈ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : deriv (fun x => eval x p) z = 0
⊢ z ∈ Multiset.toFinset (roots (↑derivative p))
[PROOFSTEP]
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), (Multiset.count x (roots p) - 1 + 1) =
    ∑ x in Multiset.toFinset (roots p), (rootMultiplicity x p - 1) + Finset.card (Multiset.toFinset (roots p))
[PROOFSTEP]
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), rootMultiplicity x (↑derivative p) +
      (Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1) ≤
    ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1)
[PROOFSTEP]
simp only [← count_roots]
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (Finset.card (Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)) + 1) ≤
    ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1)
[PROOFSTEP]
refine' add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le _) _) _
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p), 1 ≤
    ∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
      Multiset.count x (roots (↑derivative p))
[PROOFSTEP]
refine' Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| _
[GOAL]
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ 0 < Multiset.count x (roots (↑derivative p))
[PROOFSTEP]
rw [Multiset.count_pos, ← Multiset.mem_toFinset]
[GOAL]
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ x ∈ Multiset.toFinset (roots (↑derivative p))
[PROOFSTEP]
exact (Finset.mem_sdiff.1 hx).1
[GOAL]
p : ℝ[X]
⊢ ∑ x in Multiset.toFinset (roots p), Multiset.count x (roots (↑derivative p)) +
      (∑ x in Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p),
          Multiset.count x (roots (↑derivative p)) +
        1) =
    ↑Multiset.card (roots (↑derivative p)) + 1
[PROOFSTEP]
rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
  Multiset.toFinset_sum_count_eq, ← Finset.sum_subset (Finset.subset_union_right _ _)]
[GOAL]
p : ℝ[X]
⊢ ∀ (x : ℝ),
    x ∈ Multiset.toFinset (roots p) ∪ Multiset.toFinset (roots (↑derivative p)) →
      ¬x ∈ Multiset.toFinset (roots (↑derivative p)) → Multiset.count x (roots (↑derivative p)) = 0
[PROOFSTEP]
intro x _ hx₂
[GOAL]
p : ℝ[X]
x : ℝ
a✝ : x ∈ Multiset.toFinset (roots p) ∪ Multiset.toFinset (roots (↑derivative p))
hx₂ : ¬x ∈ Multiset.toFinset (roots (↑derivative p))
⊢ Multiset.count x (roots (↑derivative p)) = 0
[PROOFSTEP]
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂
[GOAL]
F : Type u_1
inst✝¹ : CommRing F
inst✝ : Algebra F ℝ
p : F[X]
⊢ Fintype.card ↑(rootSet p ℝ) ≤ Fintype.card ↑(rootSet (↑derivative p) ℝ) + 1
[PROOFSTEP]
simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
  card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))
