-- 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
this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}
sub_both_sides :
  (-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 =
    psum σ R 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:
exact sub_both_sides.symm

Result:
no goals

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 =
    (-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

Tactic:
simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] 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
this : filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k) = {(0, k)}
sub_both_sides :
  (-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 =
    psum σ R 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
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
⊢ (0, k).1 + (0, k).2 = k ∧ (0, k).1 < k ∧ ¬0 < (0, k).1

Tactic:
omega

Result:
no goals

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
a : ℕ × ℕ
⊢ a = (0, k) → a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1

Tactic:
rintro rfl

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 =
    ∑ a ∈ filter (fun a => a.1 < k ∧ ¬0 < a.1) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
⊢ (0, k).1 + (0, k).2 = k ∧ (0, k).1 < k ∧ ¬0 < (0, k).1