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

State before:
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
Tactic:
by_cases h : x sample_removed = 0
State after:
case pos
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1

case neg
F✝ : Type
inst✝² : Field F✝
σ F : Type
inst✝¹ : Field F
inst✝ : DecidableEq σ
d : ℕ
sample_removed sample_target : σ
x : σ →₀ ℕ
h : ¬x sample_removed = 0
⊢ (if x sample_removed = 0 then (Finset.filter (fun y => ¬y = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1
    else
      (X sample_target ^ d) ^ x sample_removed *
        (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1) =
    (X sample_target ^ d) ^ x sample_removed *
      (Finset.filter (fun x => ¬x = sample_removed) x.support).prod fun x_1 => X x_1 ^ x x_1

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

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