case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (erase n { toFinsupp := toFinsupp✝ }) i = if i = n then 0 else coeff { toFinsupp := toFinsupp✝ } i
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n i : ℕ
⊢ coeff (erase n p) i = if i = n then 0 else coeff p i
rcases p with ⟨⟩
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.erase n toFinsupp✝) i = if i = n then 0 else ↑toFinsupp✝ i
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (erase n { toFinsupp := toFinsupp✝ }) i = if i = n then 0 else coeff { toFinsupp := toFinsupp✝ } i
simp only [erase_def, coeff]
no goals
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.erase n toFinsupp✝) i = if i = n then 0 else ↑toFinsupp✝ i
exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)