R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = -Multiset.sum t
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = -Multiset.sum t
nontriviality R
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    nextCoeff (prod (Multiset.map (fun x => X - ↑C x) t))
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = -Multiset.sum t
convert multiset_prod_X_sub_C_nextCoeff (by assumption)
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    if natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0 then 0
    else coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    nextCoeff (prod (Multiset.map (fun x => X - ↑C x) t))
rw [nextCoeff]
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0

case h.e'_2.inr
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
case h.e'_2
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    if natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0 then 0
    else coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
split_ifs with h
case h.e'_2.inr.e_a.e_a
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ↑Multiset.card t = natDegree (prod (Multiset.map (fun x => X - ↑C x) t))
case h.e'_2.inr
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) =
    coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) - 1)
congr
no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
⊢ Multiset ?m.820577
assumption
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0

case h.e'_2.inl.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
rw [natDegree_multiset_prod_of_monic] at h <;> simp only [Multiset.mem_map] at *
case h.e'_2.inl.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f

case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0

case h.e'_2.inl.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f
swap
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ∀ (x : ℕ), (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) → x = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : Multiset.sum (Multiset.map (fun x => natDegree x) (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map] at h
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ∀ (x : ℕ), (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) → x = 0
⊢ coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) = 0
contrapose! h
case h.e'_2.inl.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
x : R
hx : x ∈ t
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
case h.e'_2.inl
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
no goals
case h.e'_2.inl.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : coeff (prod (Multiset.map (fun x => X - ↑C x) t)) (↑Multiset.card t - 1) ≠ 0
x : R
hx : x ∈ t
⊢ ∃ x, (∃ a, (∃ a_1, a_1 ∈ t ∧ X - ↑C a_1 = a) ∧ natDegree a = x) ∧ x ≠ 0
exact ⟨_, ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩, one_ne_zero⟩
case h.e'_2.inl.h.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
w✝ : R
left✝ : w✝ ∈ t
⊢ Monic (X - ↑C w✝)
case h.e'_2.inl.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), (∃ a, a ∈ t ∧ X - ↑C a = f) → Monic f
rintro _ ⟨_, _, rfl⟩
no goals
case h.e'_2.inl.h.intro.intro
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
w✝ : R
left✝ : w✝ ∈ t
⊢ Monic (X - ↑C w✝)
apply monic_X_sub_C
no goals
case h.e'_2.inr.e_a.e_a.h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
ht : 0 < ↑Multiset.card t
✝ : Nontrivial R
h : ¬natDegree (prod (Multiset.map (fun x => X - ↑C x) t)) = 0
⊢ ∀ (f : R[X]), f ∈ Multiset.map (fun x => X - ↑C x) t → Monic f
simp [natDegree_X_sub_C, monic_X_sub_C]