R : Type u_2
σ : Type u_1
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 in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
let s := Finset.univ.val.map fun i : σ => (MvPolynomial.X i : MvPolynomial σ R)
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
R : Type u_2
σ : Type u_1
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 in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
have : Fintype.card σ = Multiset.card s := by
  rw [Multiset.card_map, ←Finset.card_univ, Finset.card_def]
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.prod (Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val) =
    ∑ x in range (↑Multiset.card (Multiset.map (fun i => X i) univ.val) + 1),
      ↑Polynomial.C (Multiset.esymm (Multiset.map X univ.val) x) *
        Polynomial.X ^ (↑Multiset.card (Multiset.map (fun i => X i) univ.val) - x)
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
simp_rw [this, MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
case h.e'_2.h.e'_3
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val =
    Multiset.map (fun r => Polynomial.X + ↑Polynomial.C r) s
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.prod (Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val) =
    ∑ x in range (↑Multiset.card (Multiset.map (fun i => X i) univ.val) + 1),
      ↑Polynomial.C (Multiset.esymm (Multiset.map X univ.val) x) *
        Polynomial.X ^ (↑Multiset.card (Multiset.map (fun i => X i) univ.val) - x)
convert Multiset.prod_X_add_C_eq_sum_esymm s
no goals
case h.e'_2.h.e'_3
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val =
    Multiset.map (fun r => Polynomial.X + ↑Polynomial.C r) s
simp_rw [Multiset.map_map, Function.comp_apply]
no goals
R : Type u_2
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ Fintype.card σ = ↑Multiset.card s
rw [Multiset.card_map, ←Finset.card_univ, Finset.card_def]