case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q✝ q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ } = q ↔ ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝ } n = coeff q n
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), coeff p n = coeff q n
rcases p with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ } ↔
    ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝¹ } n = coeff { toFinsupp := toFinsupp✝ } n
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q✝ q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ } = q ↔ ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝ } n = coeff q n
rcases q with ⟨⟩
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ = toFinsupp✝ ↔ ∀ (n : ℕ), ↑toFinsupp✝¹ n = ↑toFinsupp✝ n
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ } ↔
    ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝¹ } n = coeff { toFinsupp := toFinsupp✝ } n
simp [coeff]
no goals
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ = toFinsupp✝ ↔ ∀ (n : ℕ), ↑toFinsupp✝¹ n = ↑toFinsupp✝ n
exact FunLike.ext_iff (F := ℕ →₀ R)