no goals
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))
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
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)
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)
simp only [← count_roots]
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))
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)
refine' add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le _) _) _
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ 0 < Multiset.count x (roots (↑derivative p))
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))
refine' Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| _
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ x ∈ Multiset.toFinset (roots (↑derivative p))
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ 0 < Multiset.count x (roots (↑derivative p))
rw [Multiset.count_pos, ← Multiset.mem_toFinset]
no goals
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots (↑derivative p)) \ Multiset.toFinset (roots p)
⊢ x ∈ Multiset.toFinset (roots (↑derivative p))
exact (Finset.mem_sdiff.1 hx).1
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
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
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 _ _)]
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
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
intro x _ hx₂
no goals
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
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂