-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem multiset_prod_X_sub_C_coeff_card_pred (t : Multiset R) (ht : 0 < Multiset.card t) :
    (t.map fun x => X - C x).prod.coeff ((Multiset.card t) - 1) = -t.sum

Proof state:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x => X - C x) t).prod.natDegree = 0

Tactic:
rw [natDegree_multiset_prod_of_monic]

Result:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x => X - C x) t)).sum = 0

case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) t, f.Monic

Proof state:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0

Tactic:
obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht

Result:
case h.e'_2.hnc.intro
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
x : R
hx : x ∈ t
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0

Proof state:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x => X - C x) t)).sum = 0

case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) t, f.Monic

Tactic:
swap

Result:
case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) t, f.Monic

case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x => X - C x) t)).sum = 0

Proof state:
case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) t, f.Monic

Tactic:
simp only [Multiset.mem_map]

Result:
case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ (f : R[X]), (∃ a ∈ t, X - C a = f) → f.Monic

Proof state:
case h.e'_2.e_a.e_a.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x => X - C x) t, f.Monic

Tactic:
simp [natDegree_X_sub_C, monic_X_sub_C]

Result:
no goals

Proof state:
case h.e'_2
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x => X - C x) t).prod.coeff ((Multiset.map (fun x => X - C x) t).prod.natDegree - 1)

Tactic:
congr

Result:
case h.e'_2.e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map (fun x => X - C x) t).prod.natDegree

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) = -t.sum

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) = -t.sum

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ Multiset ?m.93638

Tactic:
assumption

Result:
no goals

Proof state:
case h.e'_2.hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ (f : R[X]), (∃ a ∈ t, X - C a = f) → f.Monic

Tactic:
rintro _ ⟨_, _, rfl⟩

Result:
case h.e'_2.hnc.h.intro.intro
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
w✝ : R
left✝ : w✝ ∈ t
⊢ (X - C w✝).Monic

Proof state:
case h.e'_2.hnc.intro
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
x : R
hx : x ∈ t
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0

Tactic:
exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩

Result:
no goals

Proof state:
case h.e'_2
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x => X - C x) t).prod.coeff ((Multiset.map (fun x => X - C x) t).prod.natDegree - 1)

case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x => X - C x) t).prod.natDegree = 0

Tactic:
swap

Result:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x => X - C x) t).prod.natDegree = 0

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

Proof state:
case h.e'_2.hnc.h.intro.intro
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
w✝ : R
left✝ : w✝ ∈ t
⊢ (X - C w✝).Monic

Tactic:
apply monic_X_sub_C

Result:
no goals

Proof state:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x => X - C x) t)).sum = 0

Tactic:
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]

Result:
case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) = -t.sum

Tactic:
convert multiset_prod_X_sub_C_nextCoeff (by assumption)

Result:
case h.e'_2
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) = (Multiset.map (fun x => X - C x) t).prod.nextCoeff

Proof state:
case h.e'_2
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) = (Multiset.map (fun x => X - C x) t).prod.nextCoeff

Tactic:
rw [nextCoeff, if_neg]

Result:
case h.e'_2
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x => X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x => X - C x) t).prod.coeff ((Multiset.map (fun x => X - C x) t).prod.natDegree - 1)

case h.e'_2.hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x => X - C x) t).prod.natDegree = 0