-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem embDomain_succ_smul_powers :
    (x • powers x hx).embDomain ⟨Nat.succ, Nat.succ_injective⟩ =
      powers x hx - ofFinsupp (Finsupp.single 0 1)

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ∀ (a : ℕ),
    ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) a =
      (powers x hx - ofFinsupp (Finsupp.single 0 1)) a

Tactic:
rintro (_ | n)

Result:
case h.zero
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) 0 =
    (powers x hx - ofFinsupp (Finsupp.single 0 1)) 0

case h.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
n : ℕ
⊢ ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) (n + 1) =
    (powers x hx - ofFinsupp (Finsupp.single 0 1)) (n + 1)

Proof state:
case h.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
n : ℕ
⊢ ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) (n + 1) =
    (powers x hx - ofFinsupp (Finsupp.single 0 1)) (n + 1)

Tactic:
refine Eq.trans (embDomain_image _ ⟨Nat.succ, Nat.succ_injective⟩) ?_

Result:
case h.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
n : ℕ
⊢ (x • powers x hx) n = (powers x hx - ofFinsupp (Finsupp.single 0 1)) (n + 1)

Proof state:
case h.zero
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) 0 =
    (powers x hx - ofFinsupp (Finsupp.single 0 1)) 0

Tactic:
rw [embDomain_notin_range, sub_apply, coe_powers, pow_zero, coe_ofFinsupp,
  Finsupp.single_eq_same, sub_self]

Result:
case h.zero.h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ 0 ∉ Set.range ⇑{ toFun := Nat.succ, inj' := Nat.succ_injective }

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ (x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } =
    powers x hx - ofFinsupp (Finsupp.single 0 1)

Tactic:
apply SummableFamily.ext

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ∀ (a : ℕ),
    ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) a =
      (powers x hx - ofFinsupp (Finsupp.single 0 1)) a

Proof state:
case h.zero.h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ 0 ∉ Set.range ⇑{ toFun := Nat.succ, inj' := Nat.succ_injective }

Tactic:
rw [Set.mem_range, not_exists]

Result:
case h.zero.h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ∀ (x : ℕ), ¬{ toFun := Nat.succ, inj' := Nat.succ_injective } x = 0

Proof state:
case h.zero.h
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
⊢ ∀ (x : ℕ), ¬{ toFun := Nat.succ, inj' := Nat.succ_injective } x = 0

Tactic:
exact Nat.succ_ne_zero

Result:
no goals

Proof state:
case h.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
n : ℕ
⊢ (x • powers x hx) n = (powers x hx - ofFinsupp (Finsupp.single 0 1)) (n + 1)

Tactic:
rw [smul_apply, powers_toFun, coe_sub, coe_powers, Pi.sub_apply, coe_ofFinsupp, pow_succ',
  Finsupp.single_eq_of_ne (Nat.zero_ne_add_one n), sub_zero, of_symm_smul_of_eq_mul]

Result:
no goals