apply Nat.eq_zero_of_le_zero
case refine'_2
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) = 0
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a * ∏ x ∈ s, id x) ≤ 0