no goals
K : Type ?u.9648
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : Fintype R
p : R[X]
hp : 0 < degree p
a : R
x✝ : a ∈ image (fun x => eval x p) univ
⊢ filter (fun x => eval x p = a) univ = Multiset.toFinset (roots (p - ↑C a))
simp [Finset.ext_iff, ← mem_roots_sub_C hp]