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
s : Multiset R
h : Multiset.prod (Multiset.map (fun a => X - ↑C a) s) ∣ p
r : R
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.filter (Eq r) s)) ∣ 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]
hp : p ≠ 0
s : Multiset R
h : Multiset.prod (Multiset.map (fun a => X - ↑C a) s) ∣ p
r : R
⊢ Multiset.count r s ≤ Multiset.count r (roots p)
rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
  Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
no goals
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
s : Multiset R
h : Multiset.prod (Multiset.map (fun a => X - ↑C a) s) ∣ p
r : R
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.filter (Eq r) s)) ∣ p
exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h