-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
rw₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t
rw₂ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t
rw₃ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t -
      HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
rw₄ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -(HPow.hPow (α := MvPolynomial σ R) (-1) k *
          ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t) =
    0
rw₅ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
rw₆ rw₇ rw₈ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
rw₉ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) 1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
classical
  rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
  nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
  rw [← pow_add, add_comm 1 k, ← left_distrib,
    ← sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
    NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
    neg_one_pow_mul_eq_zero_iff.mpr rfl]

Premises used: Iff.mpr, sub_eq_zero, sub_eq_add_neg, pow_add, eq_comm, add_comm, HPow.hPow, neg_eq_neg_one_mul, pow_one, neg_mul_eq_neg_mul, OfNat.ofNat, neg_one_pow_mul_eq_zero_iff, Neg.neg, rfl, left_distrib