intro _
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0) → degreeOf i (∅.prod id) = 0
case refine'_1
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
hp✝ : ∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (∅.prod id) = 0