internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
⊢ p = 0
Tactic:
ext m
Proof state after:
case a
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
⊢ coeff m p = coeff m 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
case a
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
⊢ coeff m p = coeff m 0
Tactic:
simp only [coeff_zero]
Proof state after:
case a
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
⊢ coeff m p = 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
case a
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
⊢ coeff m p = 0
Tactic:
by_cases m_sample_target_bound : m sample_target < d
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p = 0

case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : ¬m sample_target < d
⊢ coeff m p = 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
this :
  coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
⊢ coeff m p = 0
Tactic:
rw [this]
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
this :
  coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
⊢ coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p) =
    0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
this :
  coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
⊢ coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p) =
    0
Tactic:
rw [h]
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
this :
  coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
⊢ coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed)) 0 = 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
this :
  coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
⊢ coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed)) 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p)
Tactic:
unfold MvPolynomial.bind₁
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((aeval fun x => if x = sample_removed then X sample_target ^ d else X x) p)
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((aeval fun x => if x = sample_removed then X sample_target ^ d else X x) p)
Tactic:
nth_rewrite 2 [<-MvPolynomial.support_sum_monomial_coeff p]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((aeval fun x => if x = sample_removed then X sample_target ^ d else X x)
        (p.support.sum fun v => (monomial v) (coeff v p)))
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    coeff (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed))
      ((aeval fun x => if x = sample_removed then X sample_target ^ d else X x)
        (p.support.sum fun v => (monomial v) (coeff v p)))
Tactic:
simp_rw [aeval_sum, aeval_monomial, ite_pow, algebraMap_eq, coeff_sum, coeff_C_mul, Finsupp.prod, Finset.prod_ite, Finset.filter_eq', Finsupp.mem_support_iff, ne_eq, ite_not,apply_ite Finset.prod, ite_apply, Finset.prod_empty, Finset.prod_singleton, ite_mul, one_mul, MvPolynomial.remove_ite_for_casing, X, MvPolynomial.monomial_pow,MvPolynomial.coeff_monomial_mul']
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    p.support.sum fun x =>
      coeff x p *
        if
            x sample_removed • d • Finsupp.single sample_target 1 ≤
              Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) then
          (1 ^ d) ^ x sample_removed *
            coeff
              (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
                x sample_removed • d • Finsupp.single sample_target 1)
              ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
                (monomial (x x_1 • Finsupp.single x_1 1)) (1 ^ x x_1))
        else 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    p.support.sum fun x =>
      coeff x p *
        if
            x sample_removed • d • Finsupp.single sample_target 1 ≤
              Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) then
          (1 ^ d) ^ x sample_removed *
            coeff
              (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
                x sample_removed • d • Finsupp.single sample_target 1)
              ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
                (monomial (x x_1 • Finsupp.single x_1 1)) (1 ^ x x_1))
        else 0
Tactic:
simp only [Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.single_le_iff, Finsupp.coe_add,
  Pi.add_apply, Finsupp.single_eq_same, one_pow, one_mul, mul_ite, mul_zero]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    p.support.sum fun x =>
      if x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed then
        coeff x p *
          coeff
            (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d))
            ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
              (monomial (Finsupp.single x_1 (x x_1))) 1)
      else 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    p.support.sum fun x =>
      if x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed then
        coeff x p *
          coeff
            (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d))
            ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
              (monomial (Finsupp.single x_1 (x x_1))) 1)
      else 0
Tactic:
simp_rw [Finset.sum_ite]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    ((Finset.filter
            (fun x => x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
            p.support).sum
        fun x =>
        coeff x p *
          coeff
            (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d))
            ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
              (monomial (Finsupp.single x_1 (x x_1))) 1)) +
      (Finset.filter
            (fun x => ¬x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
            p.support).sum
        fun x => 0
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    ((Finset.filter
            (fun x => x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
            p.support).sum
        fun x =>
        coeff x p *
          coeff
            (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d))
            ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
              (monomial (Finsupp.single x_1 (x x_1))) 1)) +
      (Finset.filter
            (fun x => ¬x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
            p.support).sum
        fun x => 0
Tactic:
simp only [not_le, Finset.sum_const_zero, add_zero]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter
          (fun x => x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
          p.support).sum
      fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
            (monomial (Finsupp.single x_1 (x x_1))) 1)
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter
          (fun x => x sample_removed * d ≤ (Finsupp.erase sample_removed m) sample_target + d * m sample_removed)
          p.support).sum
      fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
            (monomial (Finsupp.single x_1 (x x_1))) 1)
Tactic:
simp only [ne_eq, hsa, not_false_eq_true, Finsupp.erase_ne]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter (fun x => x sample_removed * d ≤ m sample_target + d * m sample_removed) p.support).sum fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
            (monomial (Finsupp.single x_1 (x x_1))) 1)
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter (fun x => x sample_removed * d ≤ m sample_target + d * m sample_removed) p.support).sum fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 =>
            (monomial (Finsupp.single x_1 (x x_1))) 1)
Tactic:
simp_rw [←MvPolynomial.X_pow_eq_monomial]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter (fun x => x sample_removed * d ≤ m sample_target + d * m sample_removed) p.support).sum fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1)
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter (fun x => x sample_removed * d ≤ m sample_target + d * m sample_removed) p.support).sum fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1)
Tactic:
simp_rw [MvPolynomial.prod_neq_pow_eq_monomial_erase sample_removed]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
d : ℕ
hd : 0 < d
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
h : (bind₁ fun x => if x = sample_removed then X sample_target ^ d else X x) p = 0
hdegree : degreeOf sample_target p < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ coeff m p =
    (Finset.filter (fun x => x sample_removed * d ≤ m sample_target + d * m sample_removed) p.support).sum fun x =>
      coeff x p *
        coeff
          (Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
            Finsupp.single sample_target (x sample_removed * d))
          ((monomial (Finsupp.erase sample_removed x)) 1)