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

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

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

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

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

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

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

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

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

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

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

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