R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ (Multiset.bind s fun a => roots (X - ↑C a)) = s

case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ¬0 ∈ Multiset.map (fun a => X - ↑C a) s
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ roots (prod (Multiset.map (fun a => X - ↑C a) s)) = s
rw [roots_multiset_prod, Multiset.bind_map]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ (Multiset.bind s fun a => {a}) = s
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ (Multiset.bind s fun a => roots (X - ↑C a)) = s
simp_rw [roots_X_sub_C]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ (Multiset.bind s fun a => {a}) = s
rw [Multiset.bind_singleton, Multiset.map_id']
case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ¬∃ a, a ∈ s ∧ X - ↑C a = 0
case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ¬0 ∈ Multiset.map (fun a => X - ↑C a) s
rw [Multiset.mem_map]
case a.intro.intro
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
a : R
h : X - ↑C a = 0
⊢ False
case a
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
⊢ ¬∃ a, a ∈ s ∧ X - ↑C a = 0
rintro ⟨a, -, h⟩
no goals
case a.intro.intro
R : Type u
S : Type v
T : Type w
a✝ b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Multiset R
a : R
h : X - ↑C a = 0
⊢ False
exact X_sub_C_ne_zero a h