-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
rw₅ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₆ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₇ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + k) * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₈ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HMul.hMul (α := MvPolynomial σ R) 1 (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₉ rw₁₀ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t

Tactic:
rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]

Premises used: Finset.mul_sum, mul_assoc, pow_add, MvPolynomial.esymm, Even.neg_one_pow, Nat.cast, HPow.hPow, _private.0.MvPolynomial.NewtonIdentities.esymm_summand_to_weight, Exists.intro, mul_comm, _private.0.MvPolynomial.NewtonIdentities.sum_filter_pairs_eq_sum_powersetCard_sum, OfNat.ofNat, Finset.sum_congr, Neg.neg, one_mul, rfl, _private.0.MvPolynomial.NewtonIdentities.weight