rw [Finset.inter_comm, Finset.sum_inter_add_sum_diff]
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
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p =
    ∑ i ∈ p.leadingTerms.support ∩ p.support, (monomial i) (coeff i p) +
      ∑ 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
this✝ : p.leadingTerms.support ⊆ p.support
this : p.leadingTerms.support ∩ p.support = p.leadingTerms.support
⊢ p = ∑ x ∈ p.support, (monomial x) (coeff x p)