Theorem: MvPolynomial.bind_ite_filter_aux (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
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
hdegree : ∀ a ∈ p.support, a 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 =
    Finset.filter (fun a => a = m) p.support
Tactic:
apply Finset.filter_congr
State after:
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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ∀ x ∈ p.support,
    x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
        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) ↔
      x = m

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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
⊢ ∀ x ∈ p.support,
    x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
        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) ↔
      x = m
Tactic:
intro x hx
State after:
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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x ∈ p.support
⊢ x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
      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) ↔
    x = m

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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x ∈ p.support
⊢ x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
      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) ↔
    x = m
Tactic:
replace hx := hdegree x hx
State after:
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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
⊢ x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
      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) ↔
    x = m

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
hdegree : ∀ a ∈ p.support, a sample_target < d
m : σ →₀ ℕ
m_sample_target_bound : m sample_target < d
x : σ →₀ ℕ
hx : x sample_target < d
⊢ x sample_removed * d ≤ m sample_target + d * m sample_removed ∧
      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) ↔
    x = m
Tactic:
clear hdegree
State after:
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 + d * m sample_removed ∧
      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) ↔
    x = m

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 + d * m sample_removed ∧
      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) ↔
    x = m
Tactic:
simp_rw [mul_comm d]
State after:
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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