Theorem: MvPolynomial.support_sum_monomial_subset (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support ⊆ S
Tactic:
classical
rw [support_sum_monomial_eq]
apply filter_subset
State after:
no goals

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ (∑ v ∈ S, (monomial v) (f v)).support ⊆ S
Tactic:
rw [support_sum_monomial_eq]
State after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ filter (fun v => f v ≠ 0) S ⊆ S

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
S : Finset (ι →₀ ℕ)
f : (ι →₀ ℕ) → R
⊢ filter (fun v => f v ≠ 0) S ⊆ S
Tactic:
apply filter_subset
State after:
no goals