-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem _root_.Polynomial.coeff_eq_esymm_roots_of_card [IsDomain R] {p : R[X]}
    (hroots : Multiset.card p.roots = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) :
    p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Proof state:
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ (map (fun a => X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
convert p.roots.prod_X_sub_C_coeff this using 3 <;> rw [hroots]

Result:
no goals

Proof state:
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (map (fun a => X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
have : k ≤ card (roots p) := by rw [hroots]; exact h

Result:
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ (map (fun a => X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (C p.leadingCoeff * (map (fun a => X - C a) p.roots).prod).coeff k =
    p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
rw [coeff_C_mul, mul_assoc]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a => X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * ((-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (C p.leadingCoeff * (map (fun a => X - C a) p.roots).prod).coeff k =
    p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.roots.card

Tactic:
rw [hroots]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.natDegree

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.natDegree

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a => X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * ((-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k))

Tactic:
congr

Result:
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (map (fun a => X - C a) p.roots).prod.coeff k = (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)