have : ∀ (x : ι →₀ ℕ) (_ : x ∈ p.support),
    ¬x + Finsupp.single i (p.totalDegree - x.sum fun (_x : ι) (m : ℕ) => m) = d := by
  intro x hx hh
  apply hd
  rw [← hh, weightedDegree_one]
  change ((x + Finsupp.single i (p.totalDegree - x.sum fun _ m => m)).sum fun _ m => m) = _
  rw [aux hx]
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
⊢ (∑ 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
⊢ (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) = 0