K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
⊢ ↑(ofPowerSeries ℤ F) PowerSeries.X = ↑(single 1) 1
K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
⊢ ↑X = ↑(single 1) 1
rw [coe_num_denom, num_X, denom_X, Polynomial.coe_X, Polynomial.coe_one,
   PowerSeries.coe_one, div_one]
no goals
K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
⊢ ↑(ofPowerSeries ℤ F) PowerSeries.X = ↑(single 1) 1
simp only [ofPowerSeries_X]