-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem exists_multiset_roots [DecidableEq R] :
    ∀ {p : R[X]} (_ : p ≠ 0), ∃ s : Multiset R,
      (Multiset.card s : WithBot ℕ) ≤ degree p ∧ ∀ a, s.count a = rootMultiplicity a p
  | p, hp =>
    haveI := Classical.propDecidable (∃ x, IsRoot p x)
    if h : ∃ x, IsRoot p x then
      let ⟨x, hx⟩ := h
      have hpd : 0 < degree p := degree_pos_of_root hp hx
      have hd0 : p /ₘ (X - C x) ≠ 0 := fun h => by
        rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp; exact hp rfl
      have wf : degree (p /ₘ (X - C x)) < degree p :=
        degree_divByMonic_lt _ (monic_X_sub_C x) hp ((degree_X_sub_C x).symm ▸ by decide)
      let ⟨t, htd, htr⟩ := @exists_multiset_roots _ (p /ₘ (X - C x)) hd0
      have hdeg : degree (X - C x) ≤ degree p

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ 1 + ↑t.card ≤ 1 + (p /ₘ (X - C x)).degree

Tactic:
exact add_le_add (le_refl (1 : WithBot ℕ)) htd

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ¬∃ x, p.IsRoot x
a : R
⊢ count a 0 = rootMultiplicity a p

Tactic:
rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p

Tactic:
conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))

Proof state:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t

Tactic:
rw [ha, count_cons_self, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
x✝² : (p : R[X]) ×' p ≠ 0
a✝¹ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y x✝² →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p✝ : R[X]
x✝¹ : p✝ ≠ 0
a✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p✝, x✝¹⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
x✝ :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p, hp⟩ →
      ∃ s, ↑s.card ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree
⊢ ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p

Tactic:
intro a

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ¬∃ x, p.IsRoot x
⊢ ∀ (a : R), count a 0 = rootMultiplicity a p

Tactic:
intro a

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ¬∃ x, p.IsRoot x
a : R
⊢ count a 0 = rootMultiplicity a p