Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ hsum (powers x hx) - hsum (powers x hx - ofFinsupp (Finsupp.single 0 1)) = 1
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ (1 - x) * hsum (powers x hx) = 1
rw [← hsum_smul, sub_smul 1 x (powers x hx), one_smul, hsum_sub, ←
  hsum_embDomain (x • powers x hx) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers]
no goals
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ hsum (powers x hx) - hsum (powers x hx - ofFinsupp (Finsupp.single 0 1)) = 1
simp