rw [← Finset.sum_coe_sort]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this✝ : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (weightedDegree 1) d ≠ p.totalDegree
this : ∀ x ∈ p.support, ¬x + Finsupp.single i (p.totalDegree - x.sum fun _x m => m) = d
⊢ (∑ i_1 : { x // x ∈ p.support },
      if ↑i_1 + Finsupp.single i (p.totalDegree - (↑i_1).sum fun x m => m) = d then p ↑i_1 else 0) =
    0