Lagrange power moment eq hsymm

import Mathlib.Data.Finset.Insert
import Mathlib.Data.Sym.Basic
import Mathlib.LinearAlgebra.Lagrange
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

section
open Polynomial Finset

namespace D1Bound5










theorem _root_.D1Bound5.lagrange_power_moment_eq_hsymm
    {F ι : Type*} [Field F] [DecidableEq ι]
    (s : Finset ι) (a : ι → F) (hs : s.Nonempty)
    (hinj : Set.InjOn a s) (k : ℕ) :
    (∑ i ∈ s, (a i) ^ (s.card - 1 + k) /
      (∏ j ∈ s.erase i, (a i - a j))) =
      MvPolynomial.aeval (fun i : s => a i) (MvPolynomial.hsymm s F k) := by sorry

end D1Bound5
end