case h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (a : ℕ),
    toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) a =
      toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) a
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective } =
    powers x hx - ofFinsupp (Finsupp.single 0 1)
apply SummableFamily.ext
case h.zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) Nat.zero =
    toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) Nat.zero

case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) (Nat.succ n) =
    toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) (Nat.succ n)
case h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (a : ℕ),
    toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) a =
      toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) a
rintro (_ | n)
case h.zero.h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ¬Nat.zero ∈ Set.range ↑{ toFun := Nat.succ, inj' := Nat.succ_injective }
case h.zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) Nat.zero =
    toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) Nat.zero
rw [embDomain_notin_range, sub_apply, coe_powers, pow_zero, coe_ofFinsupp,
  Finsupp.single_eq_same, sub_self]
case h.zero.h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (x : ℕ), ¬↑{ toFun := Nat.succ, inj' := Nat.succ_injective } x = Nat.zero
case h.zero.h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ¬Nat.zero ∈ Set.range ↑{ toFun := Nat.succ, inj' := Nat.succ_injective }
rw [Set.mem_range, not_exists]
no goals
case h.zero.h
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (x : ℕ), ¬↑{ toFun := Nat.succ, inj' := Nat.succ_injective } x = Nat.zero
exact Nat.succ_ne_zero
case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ toFun (x • powers x hx) n = toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) (Nat.succ n)
case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ toFun (embDomain (x • powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective }) (Nat.succ n) =
    toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) (Nat.succ n)
refine' Eq.trans (embDomain_image _ ⟨Nat.succ, Nat.succ_injective⟩) _
case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ x * x ^ n = x * x ^ n - ↑(Finsupp.single 0 1) (Nat.succ n)
case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ toFun (x • powers x hx) n = toFun (powers x hx - ofFinsupp (Finsupp.single 0 1)) (Nat.succ n)
simp only [pow_succ, coe_powers, coe_sub, smul_apply, coe_ofFinsupp, Pi.sub_apply]
no goals
case h.succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ x * x ^ n = x * x ^ n - ↑(Finsupp.single 0 1) (Nat.succ n)
rw [Finsupp.single_eq_of_ne n.succ_ne_zero.symm, sub_zero]