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

Proof state:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ filter (fun x => 0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) *
        ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) *
      ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
rw [this, sum_singleton] at sub_both_sides

Result:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ filter (fun x => 0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) *
        ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) *
      ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}
⊢ psum σ R k =
    (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ x ∈ filter (fun a => a.1 < k ∧ 0 < a.1) (antidiagonal k), (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2

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

Tactic:
simp only [Set.Ioo, Set.mem_setOf_eq, and_comm]

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

Proof state:
case h.intro.intro
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ filter (fun x => 0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) *
        ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
          (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) *
      ∑ a ∈ filter (fun x => ¬0 < x.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ filter (fun a => 0 < a.1) (filter (fun a => a.1 < k) (antidiagonal k)),
        (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left✝ : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, k)

Tactic:
rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]

Result:
no goals