case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (-{ toFinsupp := toFinsupp✝ }) = support { toFinsupp := toFinsupp✝ }
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
p : R[X]
⊢ support (-p) = support p
rcases p with ⟨⟩
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match { toFinsupp := -toFinsupp✝ } with
    | { toFinsupp := p } => p.support) =
    match { toFinsupp := toFinsupp✝ } with
    | { toFinsupp := p } => p.support
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (-{ toFinsupp := toFinsupp✝ }) = support { toFinsupp := toFinsupp✝ }
rw [← ofFinsupp_neg, support, support]
no goals
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match { toFinsupp := -toFinsupp✝ } with
    | { toFinsupp := p } => p.support) =
    match { toFinsupp := toFinsupp✝ } with
    | { toFinsupp := p } => p.support
apply Finsupp.support_neg