rw [← h]
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ 0
case mp.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : (p.support.sup fun m => m i) = 0
j : ι →₀ ℕ
hj : j ∈ p.support
⊢ j i ≤ p.support.sup fun m => m i