internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H
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 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) ↔
    x = m
Tactic:
constructor
Proof state after:
case H.mp
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 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) →
    x = m

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)
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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 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) →
    x = m
Tactic:
intro ⟨h', h''⟩
Proof state after:
case H.mp
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)
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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)
⊢ x = m
Tactic:
have h''_t := congr_arg (fun p => p sample_target) h''
Proof state after:
case H.mp
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 :
  (fun p => p sample_target) (Finsupp.erase sample_removed x) =
    (fun p => p sample_target)
      (Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (x sample_removed * d))
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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 :
  (fun p => p sample_target) (Finsupp.erase sample_removed x) =
    (fun p => p sample_target)
      (Finsupp.erase sample_removed m + Finsupp.single sample_target (m sample_removed * d) -
        Finsupp.single sample_target (x sample_removed * d))
⊢ x = m
Tactic:
simp only [ne_eq, hsa, not_false_eq_true, Finsupp.erase_ne, Finsupp.coe_tsub, Finsupp.coe_add,
  Pi.sub_apply, Pi.add_apply, Finsupp.single_eq_same] at h''_t
Proof state after:
case H.mp
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 + m sample_removed * d - x sample_removed * d
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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 + m sample_removed * d - x sample_removed * d
⊢ x = m
Tactic:
zify [h'] at h''_t
Proof state after:
case H.mp
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) + ↑(m sample_removed) * ↑d - ↑(x sample_removed) * ↑d
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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) + ↑(m sample_removed) * ↑d - ↑(x sample_removed) * ↑d
⊢ x = m
Tactic:
rw [add_sub_assoc] at h''_t
Proof state after:
case H.mp
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) + (↑(m sample_removed) * ↑d - ↑(x sample_removed) * ↑d)
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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) + (↑(m sample_removed) * ↑d - ↑(x sample_removed) * ↑d)
⊢ x = m
Tactic:
rw [<-sub_mul] at h''_t
Proof state after:
case H.mp
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) + (↑(m sample_removed) - ↑(x sample_removed)) * ↑d
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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) + (↑(m sample_removed) - ↑(x sample_removed)) * ↑d
⊢ x = m
Tactic:
have nm := near_mods (x sample_target) (m sample_target) d _ hx m_sample_target_bound h''_t
Proof state after:
case H.mp
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) + (↑(m sample_removed) - ↑(x sample_removed)) * ↑d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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) + (↑(m sample_removed) - ↑(x sample_removed)) * ↑d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
⊢ x = m
Tactic:
rw [nm] at h''_t
Proof state after:
case H.mp
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) + 0 * ↑d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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) + 0 * ↑d
nm : ↑(m sample_removed) - ↑(x sample_removed) = 0
⊢ x = m
Tactic:
simp at h''_t
Proof state after:
case H.mp
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
⊢ x = m
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp
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
⊢ x = m
Tactic:
ext val
Proof state after:
case H.mp.h
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 val = m val
Theorem: MvPolynomial.bind_ite_filter_aux
Proof state before:
case H.mp.h
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 val = m val
Tactic:
by_cases h''' : val = sample_target
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 val = m val

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
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
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
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:
by_cases h'''' : val = sample_removed
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'''' : val = sample_removed
⊢ x val = m val

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
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
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
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:
have h''_v := congr_arg (fun p => p val) 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
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
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
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
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
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:
clear 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''' : ¬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