intro a s has hs
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
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
⊢ (∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0) → degreeOf i ((cons a s has).prod id) = 0