no goals
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
classical
  cases p
  simp only [support, update, Finsupp.support_update]
  congr
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (update { toFinsupp := toFinsupp✝ } n a) =
    if a = 0 then Finset.erase (support { toFinsupp := toFinsupp✝ }) n
    else insert n (support { toFinsupp := toFinsupp✝ })
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
cases p
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support) =
    if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (update { toFinsupp := toFinsupp✝ } n a) =
    if a = 0 then Finset.erase (support { toFinsupp := toFinsupp✝ }) n
    else insert n (support { toFinsupp := toFinsupp✝ })
simp only [support, update, Finsupp.support_update]
no goals
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support) =
    if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support
congr