no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q n : ℕ
hn : 0 < n
g g' : R[X]
H : ↑(expand R n) g = ↑(expand R n) g'
k : ℕ
⊢ coeff g k = coeff g' k
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]