Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of (FormalSnarksProject/ToMathlib/ForTransformations.lean)

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

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]
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

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

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]
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

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]
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

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
State after:
no goals

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₁
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)

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]
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)))

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']
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

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]
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

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]
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

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]
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)

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]
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)

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]
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)

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]
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)

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))
          ((monomial (Finsupp.erase sample_removed x)) 1)
Tactic:
simp only [coeff_monomial, mul_ite, mul_one, mul_zero]
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 =>
      if
          Finsupp.erase sample_removed x =
            Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d) then
        coeff x p
      else 0

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 =>
      if
          Finsupp.erase sample_removed x =
            Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
              Finsupp.single sample_target (x sample_removed * d) then
        coeff x p
      else 0
Tactic:
simp_rw [Finset.sum_ite]
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 =>
              Finsupp.erase sample_removed x =
                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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
        fun x => coeff x p) +
      (Finset.filter
            (fun x =>
              ¬Finsupp.erase sample_removed x =
                  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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
        fun x => 0

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 =>
              Finsupp.erase sample_removed x =
                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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
        fun x => coeff x p) +
      (Finset.filter
            (fun x =>
              ¬Finsupp.erase sample_removed x =
                  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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
        fun x => 0
Tactic:
simp only [Finset.sum_const_zero, add_zero]
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 =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p

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 =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p
Tactic:
rw [eq_comm]
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
⊢ ((Finset.filter
          (fun x =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p) =
    coeff m p

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
⊢ ((Finset.filter
          (fun x =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p) =
    coeff m p
Tactic:
rw [MvPolynomial.degreeOf_lt_iff hd] at hdegree
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter
          (fun x =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p) =
    coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter
          (fun x =>
            Finsupp.erase sample_removed x =
              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 * d ≤ m sample_target + d * m sample_removed) p.support)).sum
      fun x => coeff x p) =
    coeff m p
Tactic:
rw [Finset.filter_filter]
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter
          (fun a =>
            a sample_removed * d ≤ m sample_target + d * m sample_removed ∧
              Finsupp.erase sample_removed a =
                Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
                  Finsupp.single sample_target (a sample_removed * d))
          p.support).sum
      fun x => coeff x p) =
    coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter
          (fun a =>
            a sample_removed * d ≤ m sample_target + d * m sample_removed ∧
              Finsupp.erase sample_removed a =
                Finsupp.erase sample_removed m + Finsupp.single sample_target (d * m sample_removed) -
                  Finsupp.single sample_target (a sample_removed * d))
          p.support).sum
      fun x => coeff x p) =
    coeff m p
Tactic:
rw [MvPolynomial.bind_ite_filter_aux (σ := σ) p sample_removed sample_target hsa d hd hdegree m m_sample_target_bound]
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter (fun a => a = m) p.support).sum fun x => coeff x p) = coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((Finset.filter (fun a => a = m) p.support).sum fun x => coeff x p) = coeff m p
Tactic:
simp only [Finset.filter_eq', mem_support_iff, ne_eq]
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p
Tactic:
by_cases h' : m ∈ p.support
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p
Tactic:
convert Finset.sum_singleton (p.coeff) m
State after:
case h.e'_2.h
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ (if m ∈ p.support then {m} else ∅) = {m}

State before:
case h.e'_2.h
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ (if m ∈ p.support then {m} else ∅) = {m}
Tactic:
simp only [ite_eq_left_iff]
State after:
case h.e'_2.h
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ m ∉ p.support → ∅ = {m}

State before:
case h.e'_2.h
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∈ p.support
⊢ m ∉ p.support → ∅ = {m}
Tactic:
tauto
State after:
no goals

State before:
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p
Tactic:
have h''' : (if m ∈ support p then ({m} : Finset (σ →₀ ℕ)) else ∅) = (∅ : Finset (σ →₀ ℕ)) := by
  simp only [h', ↓reduceIte]
State after:
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
h''' : (if m ∈ p.support then {m} else ∅) = ∅
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p

State before:
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
h''' : (if m ∈ p.support then {m} else ∅) = ∅
⊢ ((if m ∈ p.support then {m} else ∅).sum fun x => coeff x p) = coeff m p
Tactic:
rw [h''']
State after:
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
h''' : (if m ∈ p.support then {m} else ∅) = ∅
⊢ (∅.sum fun x => coeff x p) = coeff m p

State before:
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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
h''' : (if m ∈ p.support then {m} else ∅) = ∅
⊢ (∅.sum fun x => coeff x p) = coeff m p
Tactic:
simp only [Finset.sum_empty, mem_support_iff, coeff_zero_of_not_mem_support p m h', ne_eq,
  not_true_eq_false, not_false_eq_true, coeff_zero_of_not_mem_support]
State after:
no goals

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 : ∀ m ∈ p.support, m sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
h' : m ∉ p.support
⊢ (if m ∈ p.support then {m} else ∅) = ∅
Tactic:
simp only [h', ↓reduceIte]
State after:
no goals

State before:
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
Tactic:
apply MvPolynomial.coeff_zero_of_not_mem_support
State after:
case neg.h
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
⊢ m ∉ p.support

State before:
case neg.h
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
⊢ m ∉ p.support
Tactic:
contrapose! m_sample_target_bound
State after:
case neg.h
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 ∈ p.support
⊢ m sample_target < d

State before:
case neg.h
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 ∈ p.support
⊢ m sample_target < d
Tactic:
exact lt_of_le_of_lt (monomial_le_degreeOf sample_target m_sample_target_bound) hdegree
State after:
no goals