conv_lhs =>
  congr; rfl; ext i
  rw [if_neg (this i.1 i.2)]
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
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 : { x // x ∈ p.support }, 0 = 0