R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) ⊆
    {n}
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
rw [← ofFinsupp_single, support]
no goals
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) ⊆
    {n}
exact Finsupp.support_single_subset