R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(ofPowerSeries ℤ R) (powerSeriesPart x) =
    ↑(single (-order x)) 1 * (↑(single (order x)) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart x))
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(ofPowerSeries ℤ R) (powerSeriesPart x) = ↑(single (-order x)) 1 * x
refine' Eq.trans _ (congr rfl x.single_order_mul_powerSeriesPart)
no goals
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(ofPowerSeries ℤ R) (powerSeriesPart x) =
    ↑(single (-order x)) 1 * (↑(single (order x)) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart x))
rw [← mul_assoc, single_mul_single, neg_add_self, mul_one, ← C_apply, C_one, one_mul]