case a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)).toFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)
apply toFinsupp_injective
case a.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝ },
        sum q fun j a => ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝ } i * a)).toFinsupp
case a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)).toFinsupp
rcases p with ⟨⟩
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝¹ },
        sum { toFinsupp := toFinsupp✝ } fun j a =>
          ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝¹ } i * a)).toFinsupp
case a.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝ },
        sum q fun j a => ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝ } i * a)).toFinsupp
rcases q with ⟨⟩
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ * toFinsupp✝ =
    ∑ x in toFinsupp✝¹.support, ∑ x_1 in toFinsupp✝.support, Finsupp.single (x + x_1) (↑toFinsupp✝¹ x * ↑toFinsupp✝ x_1)
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝¹ },
        sum { toFinsupp := toFinsupp✝ } fun j a =>
          ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝¹ } i * a)).toFinsupp
simp [support, sum, coeff, toFinsupp_sum]
no goals
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ * toFinsupp✝ =
    ∑ x in toFinsupp✝¹.support, ∑ x_1 in toFinsupp✝.support, Finsupp.single (x + x_1) (↑toFinsupp✝¹ x * ↑toFinsupp✝ x_1)
rfl