have : ∀ (x : ι →₀ ℕ) (_ : x ∈ p.leadingTerms.support), x.support.sum x = p.totalDegree :=
  by
  intro x hx
  rw [support_leadingTerms] at hx
  simp at hx
  exact hx.2
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
⊢ p =
    ∑ v ∈ p.leadingTerms.support, (monomial v) (coeff v p.leadingTerms) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)