-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem prod_X_add_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
    (s.map fun r => X + C r).prod.coeff k = s.esymm (Multiset.card s - k)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun r => X + C r) s).prod.coeff k = s.esymm (s.card - k)

Tactic:
convert Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = (∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)).coeff k

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)

Tactic:
rw [Finset.mem_range]

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k < s.card + 1

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = (∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)).coeff k

Tactic:
simp_rw [finset_sum_coeff, coeff_C_mul_X_pow]

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

Tactic:
rw [if_pos (Nat.sub_sub_self h).symm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k < s.card + 1

Tactic:
exact Nat.lt_succ_of_le (Nat.sub_le (Multiset.card s) k)

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

Tactic:
intro j hj1 hj2

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
⊢ (if k = s.card - j then s.esymm j else 0) = 0

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
⊢ (if k = s.card - j then s.esymm j else 0) = 0

Tactic:
suffices k ≠ card s - j by rw [if_neg this]

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
⊢ k ≠ s.card - j

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
hn : k = s.card - j
⊢ False

Tactic:
rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ j
hn : k = s.card - j
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
this : k ≠ s.card - j
⊢ (if k = s.card - j then s.esymm j else 0) = 0

Tactic:
rw [if_neg this]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ j
hn : k = s.card - j
⊢ False

Tactic:
exact Ne.irrefl hj2

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0

Tactic:
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
⊢ k ≠ s.card - j

Tactic:
intro hn

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
j : ℕ
hj1 : j ∈ Finset.range (s.card + 1)
hj2 : j ≠ s.card - k
hn : k = s.card - j
⊢ False