-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem MvPolynomial.prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
    (∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) : Polynomial _).coeff k =
    MvPolynomial.esymm σ R (card σ - k)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Tactic:
rw [this] at h ⊢

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (s.card - k)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Tactic:
have : Fintype.card σ = Multiset.card s := by
  rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ (Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val).prod.coeff k =
    (Multiset.map X univ.val).esymm (s.card - k)

Tactic:
convert Multiset.prod_X_add_C_coeff s h

Result:
case h.e'_2.h.e'_3.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r => Polynomial.X + Polynomial.C r) s

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Tactic:
let s := Finset.univ.val.map fun i => (MvPolynomial.X i : MvPolynomial σ R)

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ Fintype.card σ = s.card

Tactic:
rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Result:
no goals

Proof state:
case h.e'_2.h.e'_3.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r => Polynomial.X + Polynomial.C r) s

Tactic:
simp_rw [s, Multiset.map_map, Function.comp_apply]

Result:
no goals

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ (∏ i : σ, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (s.card - k)

Tactic:
rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ (Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val).prod.coeff k =
    (Multiset.map X univ.val).esymm (s.card - k)