Homogeneous Multiset Sum insert

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

section
open Polynomial Finset

namespace D1Bound5




theorem _root_.D1Bound5.homogeneousMultisetSum_insert
    {ι R : Type*} [DecidableEq ι] [CommSemiring R]
    (s : Finset ι) (a : ι → R) (t : ι) (ht : t ∉ s) (n : ℕ) :
    homogeneousMultisetSum (fun i : (insert t s : Finset ι) => a i) (n + 1) =
      a t * homogeneousMultisetSum (fun i : (insert t s : Finset ι) => a i) n +
        homogeneousMultisetSum (fun i : s => a i) (n + 1) := by sorry







end D1Bound5
end