internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : ¬val = sample_removed
h''_v :
  (fun p => p val) (Finsupp.erase sample_removed x) =
    (fun p => p val)
      (Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (x sample_removed * d))
⊢ x val = m val
Tactic:
simp only [Finsupp.erase, Finsupp.coe_mk, h'''', ↓reduceIte, Finsupp.coe_tsub, Finsupp.coe_add,
  Pi.sub_apply, Pi.add_apply, Finsupp.single_apply] at h''_v
Proof state after:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : ¬val = sample_removed
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : ¬val = sample_removed
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Tactic:
rw [eq_comm] at h'''
Proof state after:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬val = sample_removed
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬val = sample_removed
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Tactic:
rw [eq_comm] at h''''
Proof state after:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬sample_removed = val
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬sample_removed = val
h''_v :
  x val =
    (m val + if sample_target = val then m sample_removed * d else 0) -
      if sample_target = val then x sample_removed * d else 0
⊢ x val = m val
Tactic:
simp only [h''', ↓reduceIte, add_zero, tsub_zero] at h''_v
Proof state after:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬sample_removed = val
h''_v : x val = m val
⊢ x val = m val
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬sample_target = val
h'''' : ¬sample_removed = val
h''_v : x val = m val
⊢ x val = m val
Tactic:
rw [h''_v]
Proof state after:
no goals
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : val = sample_target
⊢ x val = m val
Tactic:
rw [h'''] at *
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : sample_target = sample_target
⊢ x sample_target = m sample_target
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : sample_target = sample_target
⊢ x sample_target = m sample_target
Tactic:
clear h'''
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
⊢ x sample_target = m sample_target
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
⊢ x sample_target = m sample_target
Tactic:
assumption
Proof state after:
no goals
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : val = sample_removed
⊢ x val = m val
Tactic:
rw [h''''] at *
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : sample_removed = sample_removed
⊢ x sample_removed = m sample_removed
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
h'''' : sample_removed = sample_removed
⊢ x sample_removed = m sample_removed
Tactic:
clear h''''
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
⊢ x sample_removed = m sample_removed
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
⊢ x sample_removed = m sample_removed
Tactic:
rw [sub_eq_zero] at nm
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) = ↑(x sample_removed)
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
⊢ x sample_removed = m sample_removed
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
nm : ↑(m sample_removed) = ↑(x sample_removed)
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
⊢ x sample_removed = m sample_removed
Tactic:
simp at nm
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
nm : m sample_removed = x sample_removed
⊢ x sample_removed = m sample_removed
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
h' : x sample_removed * d ≤ m sample_target + m sample_removed * d
h'' :
  Finsupp.erase sample_removed x =
    Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
      Finsupp.single sample_target (x sample_removed * d)
h''_t : x sample_target = m sample_target
val : σ
h''' : ¬val = sample_target
nm : m sample_removed = x sample_removed
⊢ x sample_removed = m sample_removed
Tactic:
rw [nm]
Proof state after:
no goals
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mpr
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
⊢ x = m →
    x sample_removed * d ≤ m sample_target + m sample_removed * d ∧
      Finsupp.erase sample_removed x =
        Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
          Finsupp.single sample_target (x sample_removed * d)
Tactic:
intro hxm
Proof state after:
case H.mpr
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
hxm : x = m
⊢ x sample_removed * d ≤ m sample_target + m sample_removed * d ∧
    Finsupp.erase sample_removed x =
      Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (x sample_removed * d)
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mpr
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
hxm : x = m
⊢ x sample_removed * d ≤ m sample_target + m sample_removed * d ∧
    Finsupp.erase sample_removed x =
      Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (x sample_removed * d)
Tactic:
rw [hxm] at *
Proof state after:
case H.mpr
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
hxm : m = m
⊢ m sample_removed * d ≤ m sample_target + m sample_removed * d ∧
    Finsupp.erase sample_removed m =
      Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (m sample_removed * d)
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mpr
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
p : MvPolynomial σ F
sample_removed sample_target : σ
hsa : sample_target ≠ sample_removed
d : ℕ
hd : 0 < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
hxm : m = m
⊢ m sample_removed * d ≤ m sample_target + m sample_removed * d ∧
    Finsupp.erase sample_removed m =
      Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (m sample_removed * d)
Tactic:
simp only [le_add_iff_nonneg_left, zero_le, Finsupp.mem_support_iff, ne_eq, not_not, ge_iff_le,
  add_le_iff_nonpos_left, nonpos_iff_eq_zero, add_tsub_cancel_right, and_self]
Proof state after:
no goals
Theorem: MvPolynomial.remove_ite_for_casing
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
Tactic:
by_cases h : x sample_removed = 0
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1

case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : ¬x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
Theorem: MvPolynomial.remove_ite_for_casing
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
Tactic:
simp only [h, Finsupp.mem_support_iff, ne_eq, not_not, pow_zero, one_mul, ite_self]
Proof state after:
no goals
Theorem: MvPolynomial.remove_ite_for_casing
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : ¬x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
Tactic:
simp only [h, Finsupp.mem_support_iff, ne_eq, not_not, ite_false]
Proof state after:
no goals