refine' Finset.cons_induction_on P _ _
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ (∀ p ∈ P, ∀ j ∈ p.support, j i = 0) → degreeOf i (P.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
⊢ (∀ p ∈ ∅, ∀ j ∈ p.support, j i = 0) → degreeOf i (∅.prod id) = 0

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)} (h : a ∉ s),
    ((∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0) →
      (∀ p ∈ cons a s h, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s h).prod id) = 0