-- Mathlib/Algebra/Polynomial/Roots.lean
theorem count_map_roots [IsDomain A] [DecidableEq B] {p : A[X]} {f : A →+* B} (hmap : map f p ≠ 0)
    (b : B) :
    (p.roots.map f).count b ≤ rootMultiplicity b (p.map f)

Proof state:
case h.e'_3
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod =
    map f (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
simp only [Polynomial.map_multiset_prod, Multiset.map_map]

Result:
case h.e'_3
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map ((fun a => X - C a) ∘ ⇑f) p.roots).prod = (Multiset.map (map f ∘ fun a => X - C a) p.roots).prod

Proof state:
case h.e'_3.e_a.e_f.h
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
x✝ : A
⊢ ((fun a => X - C a) ∘ ⇑f) x✝ = (map f ∘ fun a => X - C a) x✝

Tactic:
simp only [Function.comp_apply, Polynomial.map_sub, map_X, map_C]

Result:
no goals

Proof state:
case h.e'_3
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map ((fun a => X - C a) ∘ ⇑f) p.roots).prod = (Multiset.map (map f ∘ fun a => X - C a) p.roots).prod

Tactic:
congr

Result:
case h.e'_3.e_a.e_f
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (fun a => X - C a) ∘ ⇑f = map f ∘ fun a => X - C a

Proof state:
case h.e'_3.e_a.e_f
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (fun a => X - C a) ∘ ⇑f = map f ∘ fun a => X - C a

Tactic:
ext1

Result:
case h.e'_3.e_a.e_f.h
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
x✝ : A
⊢ ((fun a => X - C a) ∘ ⇑f) x✝ = (map f ∘ fun a => X - C a) x✝

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ←
  Multiset.map_replicate fun a => X - C a]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (replicate (count b (Multiset.map (⇑f) p.roots)) b)).prod ∣ map f p

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (replicate (count b (Multiset.map (⇑f) p.roots)) b)).prod ∣ map f p

Tactic:
rw [← Multiset.filter_eq]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.filter (Eq b) (Multiset.map (⇑f) p.roots))).prod ∣ map f p

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.filter (Eq b) (Multiset.map (⇑f) p.roots))).prod ∣ map f p

Tactic:
refine
  (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod ∣ map f p

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod ∣ map f p

Tactic:
convert Polynomial.map_dvd f p.prod_multiset_X_sub_C_dvd

Result:
case h.e'_3
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod =
    map f (Multiset.map (fun a => X - C a) p.roots).prod