-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem mul_esymm_eq_sum (k : ℕ) :
    k * esymm σ R k = (-1) ^ (k + 1) *
      ∑ a ∈ antidiagonal k with a.1 < k, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ ↑k * esymm σ R k =
    (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
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)]

Result:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) *
        ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t +
      -1 * (-1) ^ k *
        ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t =
    0

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) *
        ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t +
      (-1) ^ 1 * (-1) ^ k *
        ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t =
    0

Tactic:
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]

Result:
no goals

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) *
        ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t +
      -1 * (-1) ^ k *
        ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t =
    0

Tactic:
nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]

Result:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ (-1) ^ (k + 1) *
        ∑ t ∈ filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t +
      (-1) ^ 1 * (-1) ^ k *
        ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k),
          MvPolynomial.NewtonIdentities.weight σ R k t =
    0

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
⊢ ↑k * esymm σ R k =
    (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-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]

Result:
no goals