internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c * c) * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
simp only [one_div, ne_eq, hc, not_false_eq_true, inv_mul_cancel, map_one, one_mul] at this
Proof state after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j f ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j f ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
convert this
Proof state after:
no goals
Theorem: MvPolynomial.coeff_single_X
Proof state before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ coeff (Finsupp.single j n) (X x) = if n = 1 ∧ j = x then 1 else 0
Tactic:
simp_rw [MvPolynomial.X, MvPolynomial.coeff_monomial, Finsupp.single_eq_single_iff]
Proof state after:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (if x = j ∧ 1 = n ∨ False ∧ n = 0 then 1 else 0) = if n = 1 ∧ j = x then 1 else 0
Theorem: MvPolynomial.coeff_single_X
Proof state before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (if x = j ∧ 1 = n ∨ False ∧ n = 0 then 1 else 0) = if n = 1 ∧ j = x then 1 else 0
Tactic:
congr
Proof state after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (x = j ∧ 1 = n ∨ False ∧ n = 0) = (n = 1 ∧ j = x)
Theorem: MvPolynomial.coeff_single_X
Proof state before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ (x = j ∧ 1 = n ∨ False ∧ n = 0) = (n = 1 ∧ j = x)
Tactic:
simp_rw [eq_iff_iff]
Proof state after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ x = j ∧ 1 = n ∨ False ∧ n = 0 ↔ n = 1 ∧ j = x
Theorem: MvPolynomial.coeff_single_X
Proof state before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n : ℕ
x : σ
⊢ x = j ∧ 1 = n ∨ False ∧ n = 0 ↔ n = 1 ∧ j = x
Tactic:
tauto
Proof state after:
no goals
Theorem: MvPolynomial.coeff_single_X_pow
Proof state before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ coeff (Finsupp.single j n) (X x ^ k) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0
Tactic:
rw [MvPolynomial.X_pow_eq_monomial, MvPolynomial.coeff_monomial]
Proof state after:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (if Finsupp.single x k = Finsupp.single j n then 1 else 0) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0
Theorem: MvPolynomial.coeff_single_X_pow
Proof state before:
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (if Finsupp.single x k = Finsupp.single j n then 1 else 0) = if n = k ∧ j = x ∨ k = 0 ∧ n = 0 then 1 else 0
Tactic:
congr
Proof state after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (Finsupp.single x k = Finsupp.single j n) = (n = k ∧ j = x ∨ k = 0 ∧ n = 0)
Theorem: MvPolynomial.coeff_single_X_pow
Proof state before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ (Finsupp.single x k = Finsupp.single j n) = (n = k ∧ j = x ∨ k = 0 ∧ n = 0)
Tactic:
simp only [Finsupp.single_eq_single_iff, eq_iff_iff]
Proof state after:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ x = j ∧ k = n ∨ k = 0 ∧ n = 0 ↔ n = k ∧ j = x ∨ k = 0 ∧ n = 0
Theorem: MvPolynomial.coeff_single_X_pow
Proof state before:
case e_c
F : Type
inst✝² : Field F
R : Type
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
j : σ
n k : ℕ
x : σ
⊢ x = j ∧ k = n ∨ k = 0 ∧ n = 0 ↔ n = k ∧ j = x ∨ k = 0 ∧ n = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (monomial (Finsupp.erase sample_removed x)) 1
Tactic:
rw [← MvPolynomial.prod_X_pow_eq_monomial]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (Finsupp.erase sample_removed x).support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (Finsupp.erase sample_removed x).support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
simp only [Finsupp.mem_support_iff, ne_eq, not_not, Finsupp.support_erase]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (x.support.erase sample_removed).prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (x.support.erase sample_removed).prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
rw [Finset.prod_erase]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    x.support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1

case h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ X sample_removed ^ (Finsupp.erase sample_removed x) sample_removed = 1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ X sample_removed ^ (Finsupp.erase sample_removed x) sample_removed = 1
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ ((Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    x.support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
rw [Finset.prod_filter]
Proof state after:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ (x.support.prod fun a => if ¬a = sample_removed then X a ^ x a else 1) =
    x.support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ (x.support.prod fun a => if ¬a = sample_removed then X a ^ x a else 1) =
    x.support.prod fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
congr
Proof state after:
case e_f
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ (fun a => if ¬a = sample_removed then X a ^ x a else 1) = fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case e_f
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
⊢ (fun a => if ¬a = sample_removed then X a ^ x a else 1) = fun x_1 => X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
funext x_1
Proof state after:
case e_f.h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
⊢ (if ¬x_1 = sample_removed then X x_1 ^ x x_1 else 1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case e_f.h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
⊢ (if ¬x_1 = sample_removed then X x_1 ^ x x_1 else 1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
simp
Proof state after:
case e_f.h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case e_f.h
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
by_cases h : x_1 = sample_removed
Proof state after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
h : x_1 = sample_removed
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1

case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
h : ¬x_1 = sample_removed
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
h : x_1 = sample_removed
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
simp only [h, ↓reduceIte, Finsupp.erase_same, pow_zero]
Proof state after:
no goals
Theorem: MvPolynomial.prod_neq_pow_eq_monomial_erase
Proof state before:
case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
sample_removed : σ
x : σ →₀ ℕ
x_1 : σ
h : ¬x_1 = sample_removed
⊢ (if x_1 = sample_removed then 1 else X x_1 ^ x x_1) = X x_1 ^ (Finsupp.erase sample_removed x) x_1
Tactic:
simp only [h, ↓reduceIte, ne_eq, not_false_eq_true, Finsupp.erase_ne]
Proof state after:
no goals
Theorem: mod_cast_eq_cast_mod
Proof state before:
F : Type
inst✝ : Field F
a b : ℕ
⊢ ↑a % ↑b = ↑(a % b)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
⊢ c = 0
Tactic:
have h := congr_arg (fun p => p % (d : ℤ)) habcd
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : (fun p => p % d) a = (fun p => p % d) (b + c * d)
⊢ c = 0
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : (fun p => p % d) a = (fun p => p % d) (b + c * d)
⊢ c = 0
Tactic:
simp_rw [Int.add_mul_emod_self] at h
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ c = 0
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ c = 0
Tactic:
rw [emod_eq_of_lt ha', emod_eq_of_lt hb'] at h
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
simp [h] at *
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
hb' : 0 ≤ b
hb : b < d
ha' : 0 ≤ b
ha : b < d
habcd : c = 0 ∨ d = 0
h : True
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
hb' : 0 ≤ b
hb : b < d
ha' : 0 ≤ b
ha : b < d
habcd : c = 0 ∨ d = 0
h : True
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
cases habcd <;> linarith
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
exact hb
Proof state after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Theorem: Int.near_mods
Proof state before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
exact ha
Proof state after:
no goals
Theorem: near_mods
Proof state before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
⊢ c = 0
Tactic:
have h := congr_arg (fun p => p % (d : ℤ)) habcd
Proof state after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : (fun p => p % ↑d) ↑a = (fun p => p % ↑d) (↑b + c * ↑d)
⊢ c = 0
Theorem: near_mods
Proof state before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : (fun p => p % ↑d) ↑a = (fun p => p % ↑d) (↑b + c * ↑d)
⊢ c = 0
Tactic:
simp_rw [Int.add_mul_emod_self, mod_cast_eq_cast_mod, Int.ofNat_inj] at h
Proof state after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a % d = b % d
⊢ c = 0
Theorem: near_mods
Proof state before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a % d = b % d
⊢ c = 0
Tactic:
simp only [ha, Nat.mod_eq_of_lt, hb] at h
Proof state after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a = b
⊢ c = 0
Theorem: near_mods
Proof state before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a = b
⊢ c = 0
Tactic:
rw [h, self_eq_add_right, mul_eq_zero, Nat.cast_eq_zero] at habcd
Proof state after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : c = 0 ∨ d = 0
h : a = b
⊢ c = 0
Theorem: near_mods
Proof state before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : c = 0 ∨ d = 0
h : a = b
⊢ c = 0
Tactic:
cases habcd <;> linarith
Proof state after:
no goals
Theorem: MvPolynomial.bind_ite_filter_aux
Proof 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
Proof 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
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
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
Proof 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
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
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
Proof 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
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
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
Proof 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
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 + 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]
Proof 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