-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem MvPolynomial.prod_C_add_X_eq_sum_esymm :
    (∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i))) =
      ∑ j ∈ range (card σ + 1), Polynomial.C
        (MvPolynomial.esymm σ R j) * Polynomial.X ^ (card σ - j)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
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:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i : σ, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

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

Result:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ (Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val).prod =
    ∑ x ∈ range (s.card + 1), Polynomial.C ((Multiset.map X univ.val).esymm x) * Polynomial.X ^ (s.card - x)

Proof state:
case h.e'_2.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
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 σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ (Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val).prod =
    ∑ x ∈ range (s.card + 1), Polynomial.C ((Multiset.map X univ.val).esymm x) * Polynomial.X ^ (s.card - x)

Tactic:
convert Multiset.prod_X_add_C_eq_sum_esymm s

Result:
case h.e'_2.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
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 σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ ∏ i : σ, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

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 σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i : σ, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

Proof state:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ ∏ i : σ, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

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 σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ ∏ i : σ, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)