case mk
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := Finsupp.erase n p } = erase n { toFinsupp := p }
rcases p with ⟨⟩
no goals
case mk
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }
simp only [erase_def]