-- Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean
theorem card_roots_le_derivative (p : ℝ[X]) :
    Multiset.card p.roots ≤ Multiset.card (derivative p).roots + 1 :=
  calc
    Multiset.card p.roots = ∑ x ∈ p.roots.toFinset, p.roots.count x :=
      (Multiset.toFinset_sum_count_eq _).symm
    _ = ∑ x ∈ p.roots.toFinset, (p.roots.count x - 1 + 1) :=
      (Eq.symm <| Finset.sum_congr rfl fun _ hx => tsub_add_cancel_of_le <|
        Nat.succ_le_iff.2 <| Multiset.count_pos.2 <| Multiset.mem_toFinset.1 hx)
    _ = (∑ x ∈ p.roots.toFinset, (p.rootMultiplicity x - 1)) + p.roots.toFinset.card

Proof state:
p : ℝ[X]
x : ℝ
hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset
⊢ 0 < Multiset.count x (derivative p).roots

Tactic:
rw [Multiset.count_pos, ← Multiset.mem_toFinset]

Result:
p : ℝ[X]
x : ℝ
hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset
⊢ x ∈ (derivative p).roots.toFinset

Proof state:
p : ℝ[X]
⊢ ∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, 1 ≤
    ∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots

Tactic:
refine Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| ?_

Result:
p : ℝ[X]
x : ℝ
hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset
⊢ 0 < Multiset.count x (derivative p).roots

Proof state:
p : ℝ[X]
x : ℝ
a✝ : x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset
hx₂ : x ∉ (derivative p).roots.toFinset
⊢ Multiset.count x (derivative p).roots = 0

Tactic:
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂

Result:
no goals

Proof state:
p : ℝ[X]
⊢ ∀ x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset,
    x ∉ (derivative p).roots.toFinset → Multiset.count x (derivative p).roots = 0

Tactic:
intro x _ hx₂

Result:
p : ℝ[X]
x : ℝ
a✝ : x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset
hx₂ : x ∉ (derivative p).roots.toFinset
⊢ Multiset.count x (derivative p).roots = 0

Proof state:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, (Multiset.count x p.roots - 1 + 1) =
    ∑ x ∈ p.roots.toFinset, (rootMultiplicity x p - 1) + p.roots.toFinset.card

Tactic:
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]

Result:
no goals

Proof state:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1) =
    (derivative p).roots.card + 1

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

Result:
p : ℝ[X]
⊢ ∀ x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset,
    x ∉ (derivative p).roots.toFinset → Multiset.count x (derivative p).roots = 0

Proof state:
p : ℝ[X]
x : ℝ
hx : x ∈ (derivative p).roots.toFinset \ p.roots.toFinset
⊢ x ∈ (derivative p).roots.toFinset

Tactic:
exact (Finset.mem_sdiff.1 hx).1

Result:
no goals

Proof state:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)

Tactic:
refine add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le ?_) _) _

Result:
p : ℝ[X]
⊢ ∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, 1 ≤
    ∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots

Proof state:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, rootMultiplicity x (derivative p) +
      (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)

Tactic:
simp only [← count_roots]

Result:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)