K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
r : F
⊢ ↑(ofPowerSeries ℤ F) (↑(PowerSeries.C F) r) = ↑HahnSeries.C r
K F : Type u
inst✝ : Field F
p q : F[X]
f g : RatFunc F
r : F
⊢ ↑(↑C r) = ↑HahnSeries.C r
rw [coe_num_denom, num_C, denom_C, Polynomial.coe_C, 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
r : F
⊢ ↑(ofPowerSeries ℤ F) (↑(PowerSeries.C F) r) = ↑HahnSeries.C r
simp only [algebraMap_eq_C, ofPowerSeries_C, C_apply]