exact h' h
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
f : (ι →₀ ℕ) → R
this : DecidableEq ι := Classical.decEq ι
s : ι →₀ ℕ
S : Finset (ι →₀ ℕ)
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial v) (f v)).support = filter (fun v => f v ≠ 0) S
h : f s = 0
h' : f s ≠ 0
⊢ False
no goals