case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q✝ r q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } + q) n = coeff { toFinsupp := toFinsupp✝ } n + coeff q n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p + q) n = coeff p n + coeff q n
rcases p with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n + coeff { toFinsupp := toFinsupp✝ } n
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q✝ r q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } + q) n = coeff { toFinsupp := toFinsupp✝ } n + coeff q n
rcases q with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(toFinsupp✝¹ + toFinsupp✝) n = ↑toFinsupp✝¹ n + ↑toFinsupp✝ n
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n + coeff { toFinsupp := toFinsupp✝ } n
simp_rw [← ofFinsupp_add, coeff]
no goals
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(toFinsupp✝¹ + toFinsupp✝) n = ↑toFinsupp✝¹ n + ↑toFinsupp✝ n
exact Finsupp.add_apply _ _ _