conv_rhs =>
  congr; congr; rfl; ext i;
  rw [this i.1 i.2]
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 =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if ∑ i_1 ∈ (↑i).support, ↑i i_1 = p.totalDegree then coeff (↑i) p else 0) +
      ∑ 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 =
    ∑ i : { x // x ∈ p.leadingTerms.support },
        (monomial ↑i) (if p.totalDegree = p.totalDegree then coeff (↑i) p else 0) +
      ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)