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
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]
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 =>
      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
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 =>
      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]
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 =>
              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
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 =>
              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]
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 =>
            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
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 =>
            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]
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
⊢ ((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
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
⊢ ((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
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 : ∀ 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
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 : ∀ 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]
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 : ∀ 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
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 : ∀ 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]
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 : ∀ 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
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 : ∀ 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]
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 : ∀ 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
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 : ∀ 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
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 : ∀ 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
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 : ∀ 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
Proof 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}
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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]
Proof 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}
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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]
Proof 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
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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''']
Proof 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
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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]
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 : ∀ 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]
Proof state after:
no goals
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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
Proof 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
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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
Proof 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
Theorem: MvPolynomial.bind₁_ite_pow_eq_zero_of
Proof 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
Proof state after:
no goals
Theorem: AlgHom.list_map_sum
Proof state before:
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
ι : Type u_1
f : ι → A
s : List ι
⊢ φ (List.map (fun x => f x) s).sum = (List.map (fun x => φ (f x)) s).sum
Tactic:
induction s with
| nil =>
  simp
| cons x xs ih =>
  simp only [List.map_cons, List.sum_cons, map_add, ih]
Proof state after:
no goals
Theorem: AlgHom.list_map_sum
Proof state before:
case nil
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
ι : Type u_1
f : ι → A
⊢ φ (List.map (fun x => f x) []).sum = (List.map (fun x => φ (f x)) []).sum
Tactic:
simp
Proof state after:
no goals