no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ ∑ i in support p, ↑(monomial i) (coeff p i) = ∑ i in support p, ↑C (coeff p i) * X ^ i
simp only [C_mul_X_pow_eq_monomial]