classical
rw [Finsupp.sum_add_index]
rw [Finsupp.sum_single_index]
rw [add_tsub_cancel_iff_le]
apply Finset.le_sup hp
rfl
intros
rfl
intros
rfl
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
x : ι →₀ ℕ
hp : x ∈ p.support
⊢ ((x + Finsupp.single i (p.totalDegree - x.sum fun x m => m)).sum fun x m => m) = p.totalDegree
no goals