no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
n : ℕ
⊢ coeff (↑(ofPowerSeries Γ R) x) ↑n = ↑(PowerSeries.coeff R n) x
simp [ofPowerSeries_apply]