Theorem: Polynomial.discBackwardDiff_aux (LeanCamCombi/DiscreteDeriv.lean)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 0 => 1) - fun₀ | -1 => 1).sum fun x => id) = 0
Tactic:
classical simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
State after:
no goals

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 0 => 1) - fun₀ | -1 => 1).sum fun x => id) = 0
Tactic:
simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
State after:
no goals