R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod
      (Multiset.map (fun a => X - ↑C a) (Multiset.replicate (Multiset.count b (Multiset.map (↑f) (roots p))) b)) ∣
    map f p
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity b (map f p)
rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ←
  Multiset.map_replicate fun a => X - C a]
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.filter (Eq b) (Multiset.map (↑f) (roots p)))) ∣ map f p
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod
      (Multiset.map (fun a => X - ↑C a) (Multiset.replicate (Multiset.count b (Multiset.map (↑f) (roots p))) b)) ∣
    map f p
rw [← Multiset.filter_eq]
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.map (↑f) (roots p))) ∣ map f p
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.filter (Eq b) (Multiset.map (↑f) (roots p)))) ∣ map f p
refine
  (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_
case h.e'_3
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.map (↑f) (roots p))) =
    map f (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)))
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.map (↑f) (roots p))) ∣ map f p
convert Polynomial.map_dvd f p.prod_multiset_X_sub_C_dvd
case h.e'_3
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map ((fun x => X - ↑C x) ∘ fun x => ↑f x) (roots p)) =
    Multiset.prod (Multiset.map (map f ∘ fun x => X - ↑C x) (roots p))
case h.e'_3
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.map (↑f) (roots p))) =
    map f (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)))
simp only [Polynomial.map_multiset_prod, Multiset.map_map]
case h.e'_3.e_a.e_f
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ ((fun x => X - ↑C x) ∘ fun x => ↑f x) = map f ∘ fun x => X - ↑C x
case h.e'_3
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ Multiset.prod (Multiset.map ((fun x => X - ↑C x) ∘ fun x => ↑f x) (roots p)) =
    Multiset.prod (Multiset.map (map f ∘ fun x => X - ↑C x) (roots p))
congr
case h.e'_3.e_a.e_f.h
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
x✝ : A
⊢ ((fun x => X - ↑C x) ∘ fun x => ↑f x) x✝ = (map f ∘ fun x => X - ↑C x) x✝
case h.e'_3.e_a.e_f
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ ((fun x => X - ↑C x) ∘ fun x => ↑f x) = map f ∘ fun x => X - ↑C x
ext1
no goals
case h.e'_3.e_a.e_f.h
R : Type u
S : Type v
T : Type w
a b✝ : R
n : ℕ
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : IsDomain A
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
x✝ : A
⊢ ((fun x => X - ↑C x) ∘ fun x => ↑f x) x✝ = (map f ∘ fun x => X - ↑C x) x✝
simp only [Function.comp_apply, Polynomial.map_sub, map_X, map_C]