case pos
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
hf : Function.Injective ↑f
b : B
hp0 : p = 0
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity b (map f p)

case neg
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
hf : Function.Injective ↑f
b : B
hp0 : ¬p = 0
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity 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
hf : Function.Injective ↑f
b : B
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity b (map f p)
by_cases hp0 : p = 0
no goals
case pos
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
hf : Function.Injective ↑f
b : B
hp0 : p = 0
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity b (map f p)
simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero,
  rootMultiplicity_zero]
no goals
case neg
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
hf : Function.Injective ↑f
b : B
hp0 : ¬p = 0
⊢ Multiset.count b (Multiset.map (↑f) (roots p)) ≤ rootMultiplicity b (map f p)
exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b