apply Finset.Subset.trans support_monomial_subset _
case insert.hs
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ ((monomial (g s)) (f s)).support ⊆ image g (insert s S)
R : Type u_3
ι : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
α : Type u_2
g : α → ι →₀ ℕ
f : α → R
this : DecidableEq α := Classical.decEq α
s : α
S : Finset α
hs : s ∉ S
hsi : (∑ v ∈ S, (monomial (g v)) (f v)).support ⊆ image g S
⊢ {g s} ⊆ image g (insert s S)