case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p = 0
⊢ count a (roots p) = rootMultiplicity a p

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : ¬p = 0
⊢ count a (roots p) = rootMultiplicity a p
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
⊢ count a (roots p) = rootMultiplicity a p
by_cases hp : p = 0
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose (_ : ∃ s, ↑(↑Multiset.card s) ≤ degree p ∧ ∀ (a : R), count a s = rootMultiplicity a p)) =
    rootMultiplicity a p
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : ¬p = 0
⊢ count a (roots p) = rootMultiplicity a p
rw [roots, dif_neg hp]
no goals
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose (_ : ∃ s, ↑(↑Multiset.card s) ≤ degree p ∧ ∀ (a : R), count a s = rootMultiplicity a p)) =
    rootMultiplicity a p
exact (Classical.choose_spec (exists_multiset_roots hp)).2 a
no goals
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p✝ q p : R[X]
hp : p = 0
⊢ count a (roots p) = rootMultiplicity a p
simp [hp]