Lemma about bind of degree-bound MvPolynomial

Stream: Is there code for X?

[Bolton Bailey]

I am trying to prove this lemma. The proof in my head is that the coefficients of the polynomial we get from the bind match up 1-to-1 with the coefficients of p where each coefficient with a X sample_removed in it turns into X sample_target ^ d, and none of these overlap because of the degree bound.

Is there some type to represent these collections of polynomials that I can draw an equivalence between?

lemma MvPolynomial.bind₁_ite_pow_eq_zero_of {σ F : Type} [Field F] [DecidableEq σ]
    (p : MvPolynomial σ F)
    (d : ℕ)  (hd : 0 < d)
    (sample_removed sample_target : σ)
    (hsa : sample_target ≠ sample_removed)
    (h : MvPolynomial.bind₁
          ((fun x => (if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)))
          p = 0)
    (hdegree : p.degreeOf sample_target < d) :
    p = 0 := by sorry

[Bolton Bailey]

I have been trying to prove it via unfold-bash, but the proof is getting very long, and I don't understand it anymore. I thought I would have to apply induction at some point to prove that none of the coefficients overlap, but I that seems like a messy approach.

lemma MvPolynomial.bind₁_ite_pow_eq_zero_of {σ F : Type} [Field F] [DecidableEq σ]
    (p : MvPolynomial σ F)
    (d : ℕ)  (hd : 0 < d)
    (sample_removed sample_target : σ)
    (hsa : sample_target ≠ sample_removed)
    (h : MvPolynomial.bind₁
          ((fun x => (if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)))
          p = 0)
    (hdegree : p.degreeOf sample_target < d) :
    p = 0 := by
  ext m
  simp only [coeff_zero]
  have :
      coeff m p
        =
      coeff
        (m.erase sample_removed + Finsupp.single sample_target (d * m sample_removed))
        ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p) := by
    unfold MvPolynomial.bind₁
    nth_rewrite 2 [<-MvPolynomial.support_sum_monomial_coeff p]
    rw [aeval_sum]
    simp_rw [aeval_monomial]
    simp only [Finsupp.mem_support_iff, ne_eq, not_not, ite_pow]
    simp [algebraMap_eq]
    rw [coeff_sum]
    simp only [Finsupp.mem_support_iff, ne_eq, not_not, coeff_C_mul]
    unfold Finsupp.prod
    simp_rw [Finset.prod_ite]
    simp [Finset.filter_eq']
    simp_rw [apply_ite Finset.prod] -- doesn't work without the argument
    simp_rw [ite_apply]
    simp only [Finsupp.mem_support_iff, ne_eq, not_not, Finset.prod_empty, Finset.prod_singleton,
      ite_mul, one_mul]
    simp_rw [MvPolynomial.foobar]
    -- simp_rw [apply_ite]
    simp_rw [X]
    simp [MvPolynomial.monomial_pow]
    simp [MvPolynomial.coeff_monomial_mul']
    simp_rw [Finset.sum_ite]
    simp
    simp [hsa]
    simp_rw [←MvPolynomial.X_pow_eq_monomial]
    simp_rw [MvPolynomial.foobaz sample_removed]
    simp
    simp_rw [Finset.sum_ite]
    simp
    rw [eq_comm]
    rw [MvPolynomial.degreeOf_lt_iff hd] at hdegree
    rw [Finset.filter_filter]
    sorry
  rw [this]
  rw [h]
  simp

[Bolton Bailey]

I guess for a concrete "is there code" question: Do we have a submodule of degree-bound mvpolynomials like we have degreeLT for polynomials? What should that look like?