simp_rw [single_eq_monomial, coeff_monomial] at hd
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : ∑ x ∈ p.support, coeff d (Finsupp.single (x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)) (p x)) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
this : DecidableEq ι := Classical.decEq ι
d : ι →₀ ℕ
hd : (∑ x ∈ p.support, if x + Finsupp.single i (p.totalDegree - x.sum fun x m => m) = d then p x else 0) ≠ 0
⊢ (weightedDegree 1) d = p.totalDegree