rfl
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ C r * (homogeneousComponent (p.support.sup fun s => s.sum fun x e => e)) p =
    C r * (homogeneousComponent p.totalDegree) p
no goals