[GOAL]
R : Type u
inst✝ : Semiring R
x : PowerSeries R
n : ℕ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) x) ↑n = ↑(PowerSeries.coeff R n) x
[PROOFSTEP]
rw [ofPowerSeries_apply_coeff]
[GOAL]
R : Type u
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ ↑(PowerSeries.coeff R n✝) (powerSeriesPart 0) = ↑(PowerSeries.coeff R n✝) 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ powerSeriesPart x = 0 ↔ x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ powerSeriesPart x = 0 → x = 0
[PROOFSTEP]
contrapose!
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x ≠ 0 → powerSeriesPart x ≠ 0
[PROOFSTEP]
simp only [ne_eq]
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ¬x = 0 → ¬powerSeriesPart x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬powerSeriesPart x = 0
[PROOFSTEP]
rw [PowerSeries.ext_iff, not_forall]
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ∃ x_1, ¬↑(PowerSeries.coeff R x_1) (powerSeriesPart x) = ↑(PowerSeries.coeff R x_1) 0
[PROOFSTEP]
refine' ⟨0, _⟩
[GOAL]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬↑(PowerSeries.coeff R 0) (powerSeriesPart x) = ↑(PowerSeries.coeff R 0) 0
[PROOFSTEP]
simp [coeff_order_ne_zero h]
[GOAL]
case mpr
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x = 0 → powerSeriesPart x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(single (order x)) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart x) = x
[PROOFSTEP]
ext n
[GOAL]
case coeff.h
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
⊢ HahnSeries.coeff (↑(single (order x)) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart x)) n = HahnSeries.coeff x n
[PROOFSTEP]
rw [← sub_add_cancel n x.order, single_mul_coeff_add, sub_add_cancel, one_mul]
[GOAL]
case coeff.h
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) (powerSeriesPart x)) (n - order x) = HahnSeries.coeff x n
[PROOFSTEP]
by_cases h : x.order ≤ n
[GOAL]
case pos
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : order x ≤ n
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) (powerSeriesPart x)) (n - order x) = HahnSeries.coeff x n
[PROOFSTEP]
rw [Int.eq_natAbs_of_zero_le (sub_nonneg_of_le h), coeff_coe_powerSeries, powerSeriesPart_coeff, ←
  Int.eq_natAbs_of_zero_le (sub_nonneg_of_le h), add_sub_cancel'_right]
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ¬order x ≤ n
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) (powerSeriesPart x)) (n - order x) = HahnSeries.coeff x n
[PROOFSTEP]
rw [ofPowerSeries_apply, embDomain_notin_range]
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ¬order x ≤ n
⊢ 0 = HahnSeries.coeff x n
[PROOFSTEP]
contrapose! h
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : 0 ≠ HahnSeries.coeff x n
⊢ order x ≤ n
[PROOFSTEP]
exact order_le_of_coeff_ne_zero h.symm
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ¬order x ≤ n
⊢ ¬n - order x ∈
      Set.range
        ↑{ toEmbedding := { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) },
            map_rel_iff' :=
              (_ :
                ∀ {a b : ℕ},
                  ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } a ≤
                      ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } b ↔
                    a ≤ b) }
[PROOFSTEP]
contrapose! h
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h :
  n - order x ∈
    Set.range
      ↑{ toEmbedding := { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) },
          map_rel_iff' :=
            (_ :
              ∀ {a b : ℕ},
                ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } a ≤
                    ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } b ↔
                  a ≤ b) }
⊢ order x ≤ n
[PROOFSTEP]
simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h
[GOAL]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n
[PROOFSTEP]
obtain ⟨m, hm⟩ := h
[GOAL]
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ order x ≤ n
[PROOFSTEP]
rw [← sub_nonneg, ← hm]
[GOAL]
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ 0 ≤ ↑m
[PROOFSTEP]
simp only [Nat.cast_nonneg]
[GOAL]
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(ofPowerSeries ℤ R) (powerSeriesPart x) = ↑(single (-order x)) 1 * x
[PROOFSTEP]
refine' Eq.trans _ (congr rfl x.single_order_mul_powerSeriesPart)
[GOAL]
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))
[PROOFSTEP]
rw [← mul_assoc, single_mul_single, neg_add_self, mul_one, ← C_apply, C_one, one_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ (y : { x // x ∈ Submonoid.powers PowerSeries.X }), IsUnit (↑(algebraMap (PowerSeries R) (LaurentSeries R)) ↑y)
[PROOFSTEP]
rintro ⟨_, n, rfl⟩
[GOAL]
case mk.intro
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ IsUnit
    (↑(algebraMap (PowerSeries R) (LaurentSeries R))
      ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) })
[PROOFSTEP]
refine' ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, _, _⟩, _⟩
[GOAL]
case mk.intro.refine'_1
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ ↑(single ↑n) 1 * ↑(single (-↑n)) 1 = 1
[PROOFSTEP]
simp only [single_mul_single, mul_one, add_right_neg]
[GOAL]
case mk.intro.refine'_1
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ ↑(single 0) 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case mk.intro.refine'_2
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ ↑(single (-↑n)) 1 * ↑(single ↑n) 1 = 1
[PROOFSTEP]
simp only [single_mul_single, mul_one, add_left_neg]
[GOAL]
case mk.intro.refine'_2
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ ↑(single 0) 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case mk.intro.refine'_3
R : Type u
inst✝ : CommRing R
n : ℕ
⊢ ↑{ val := ↑(single ↑n) 1, inv := ↑(single (-↑n)) 1, val_inv := (_ : ↑(single ↑n) 1 * ↑(single (-↑n)) 1 = 1),
        inv_val := (_ : ↑(single (-↑n)) 1 * ↑(single ↑n) 1 = 1) } =
    ↑(algebraMap (PowerSeries R) (LaurentSeries R))
      ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) }
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ (z : LaurentSeries R),
    ∃ x,
      z * ↑(algebraMap (PowerSeries R) (LaurentSeries R)) ↑x.snd = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x.fst
[PROOFSTEP]
intro z
[GOAL]
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
⊢ ∃ x,
    z * ↑(algebraMap (PowerSeries R) (LaurentSeries R)) ↑x.snd = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x.fst
[PROOFSTEP]
by_cases h : 0 ≤ z.order
[GOAL]
case pos
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : 0 ≤ order z
⊢ ∃ x,
    z * ↑(algebraMap (PowerSeries R) (LaurentSeries R)) ↑x.snd = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x.fst
[PROOFSTEP]
refine' ⟨⟨PowerSeries.X ^ Int.natAbs z.order * powerSeriesPart z, 1⟩, _⟩
[GOAL]
case pos
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : 0 ≤ order z
⊢ z *
      ↑(algebraMap (PowerSeries R) (LaurentSeries R))
        ↑(PowerSeries.X ^ Int.natAbs (order z) * powerSeriesPart z, 1).snd =
    ↑(algebraMap (PowerSeries R) (LaurentSeries R)) (PowerSeries.X ^ Int.natAbs (order z) * powerSeriesPart z, 1).fst
[PROOFSTEP]
simp only [RingHom.map_one, mul_one, RingHom.map_mul, coe_algebraMap, ofPowerSeries_X_pow, Submonoid.coe_one]
[GOAL]
case pos
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : 0 ≤ order z
⊢ z = ↑(single ↑(Int.natAbs (order z))) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart z)
[PROOFSTEP]
rw [Int.natAbs_of_nonneg h, single_order_mul_powerSeriesPart]
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ ∃ x,
    z * ↑(algebraMap (PowerSeries R) (LaurentSeries R)) ↑x.snd = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x.fst
[PROOFSTEP]
refine' ⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, rfl⟩⟩, _⟩
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ z *
      ↑(algebraMap (PowerSeries R) (LaurentSeries R))
        ↑(powerSeriesPart z,
              { val := PowerSeries.X ^ Int.natAbs (order z),
                property :=
                  (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = PowerSeries.X ^ Int.natAbs (order z)) }).snd =
    ↑(algebraMap (PowerSeries R) (LaurentSeries R))
      (powerSeriesPart z,
          { val := PowerSeries.X ^ Int.natAbs (order z),
            property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = PowerSeries.X ^ Int.natAbs (order z)) }).fst
[PROOFSTEP]
simp only [coe_algebraMap, ofPowerSeries_powerSeriesPart]
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ z * ↑(ofPowerSeries ℤ R) (PowerSeries.X ^ Int.natAbs (order z)) = ↑(single (-order z)) 1 * z
[PROOFSTEP]
rw [mul_comm _ z]
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ z * ↑(ofPowerSeries ℤ R) (PowerSeries.X ^ Int.natAbs (order z)) = z * ↑(single (-order z)) 1
[PROOFSTEP]
refine' congr rfl _
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ ↑(ofPowerSeries ℤ R) (PowerSeries.X ^ Int.natAbs (order z)) = ↑(single (-order z)) 1
[PROOFSTEP]
rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]
[GOAL]
case neg
R : Type u
inst✝ : CommRing R
z : LaurentSeries R
h : ¬0 ≤ order z
⊢ order z ≤ 0
[PROOFSTEP]
exact le_of_not_ge h
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ {x y : PowerSeries R},
    ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) y ↔
      ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
⊢ ↑(algebraMap (PowerSeries R) (LaurentSeries R)) x = ↑(algebraMap (PowerSeries R) (LaurentSeries R)) y ↔
    ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rw [coe_algebraMap, ofPowerSeries_injective.eq_iff]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
⊢ x = y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
⊢ x = y → ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
inst✝ : CommRing R
x : PowerSeries R
⊢ ∃ c, ↑c * x = ↑c * x
[PROOFSTEP]
exact ⟨1, rfl⟩
[GOAL]
case mpr
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
⊢ (∃ c, ↑c * x = ↑c * y) → x = y
[PROOFSTEP]
rintro ⟨⟨_, n, rfl⟩, hc⟩
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
⊢ x = y
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub, PowerSeries.ext_iff] at hc
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc✝¹ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
hc✝ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      (x - y) =
    0
hc :
  ∀ (n_1 : ℕ),
    ↑(PowerSeries.coeff R n_1)
        (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
              property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
          (x - y)) =
      ↑(PowerSeries.coeff R n_1) 0
⊢ x = y
[PROOFSTEP]
rw [← sub_eq_zero, PowerSeries.ext_iff]
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc✝¹ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
hc✝ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      (x - y) =
    0
hc :
  ∀ (n_1 : ℕ),
    ↑(PowerSeries.coeff R n_1)
        (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
              property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
          (x - y)) =
      ↑(PowerSeries.coeff R n_1) 0
⊢ ∀ (n : ℕ), ↑(PowerSeries.coeff R n) (x - y) = ↑(PowerSeries.coeff R n) 0
[PROOFSTEP]
intro m
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc✝¹ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
hc✝ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      (x - y) =
    0
hc :
  ∀ (n_1 : ℕ),
    ↑(PowerSeries.coeff R n_1)
        (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
              property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
          (x - y)) =
      ↑(PowerSeries.coeff R n_1) 0
m : ℕ
⊢ ↑(PowerSeries.coeff R m) (x - y) = ↑(PowerSeries.coeff R m) 0
[PROOFSTEP]
have h := hc (m + n)
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc✝¹ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
hc✝ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      (x - y) =
    0
hc :
  ∀ (n_1 : ℕ),
    ↑(PowerSeries.coeff R n_1)
        (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
              property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
          (x - y)) =
      ↑(PowerSeries.coeff R n_1) 0
m : ℕ
h :
  ↑(PowerSeries.coeff R (m + n))
      (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
            property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
        (x - y)) =
    ↑(PowerSeries.coeff R (m + n)) 0
⊢ ↑(PowerSeries.coeff R m) (x - y) = ↑(PowerSeries.coeff R m) 0
[PROOFSTEP]
simp only at h
[GOAL]
case mpr.intro.mk.intro
R : Type u
inst✝ : CommRing R
x y : PowerSeries R
n : ℕ
hc✝¹ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      y
hc✝ :
  ↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
      (x - y) =
    0
hc :
  ∀ (n_1 : ℕ),
    ↑(PowerSeries.coeff R n_1)
        (↑{ val := (fun x x_1 => x ^ x_1) PowerSeries.X n,
              property := (_ : ∃ y, (fun x x_1 => x ^ x_1) PowerSeries.X y = (fun x x_1 => x ^ x_1) PowerSeries.X n) } *
          (x - y)) =
      ↑(PowerSeries.coeff R n_1) 0
m : ℕ
h : ↑(PowerSeries.coeff R (m + n)) (PowerSeries.X ^ n * (x - y)) = ↑(PowerSeries.coeff R (m + n)) 0
⊢ ↑(PowerSeries.coeff R m) (x - y) = ↑(PowerSeries.coeff R m) 0
[PROOFSTEP]
rwa [LinearMap.map_zero, PowerSeries.X_pow_eq, PowerSeries.monomial, add_comm m, PowerSeries.coeff, Finsupp.single_add,
  MvPowerSeries.coeff_add_monomial_mul, one_mul] at h
[GOAL]
R : Type u
R' : Type u_1
inst✝¹ : Semiring R
inst✝ : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
i : ℤ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) f) i = if i < 0 then 0 else ↑(coeff R (Int.natAbs i)) f
[PROOFSTEP]
cases i
[GOAL]
case ofNat
R : Type u
R' : Type u_1
inst✝¹ : Semiring R
inst✝ : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
a✝ : ℕ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) f) (Int.ofNat a✝) =
    if Int.ofNat a✝ < 0 then 0 else ↑(coeff R (Int.natAbs (Int.ofNat a✝))) f
[PROOFSTEP]
rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.coe_nat_nonneg _).not_lt, Int.natAbs_ofNat]
[GOAL]
case negSucc
R : Type u
R' : Type u_1
inst✝¹ : Semiring R
inst✝ : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
a✝ : ℕ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ R) f) (Int.negSucc a✝) =
    if Int.negSucc a✝ < 0 then 0 else ↑(coeff R (Int.natAbs (Int.negSucc a✝))) f
[PROOFSTEP]
rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]
[GOAL]
case negSucc
R : Type u
R' : Type u_1
inst✝¹ : Semiring R
inst✝ : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
a✝ : ℕ
⊢ ¬Int.negSucc a✝ ∈
      ↑{ toEmbedding := { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) },
            map_rel_iff' :=
              (_ :
                ∀ {a b : ℕ},
                  ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } a ≤
                      ↑{ toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } b ↔
                    a ≤ b) } ''
        HahnSeries.support (↑(RingEquiv.symm toPowerSeries) f)
[PROOFSTEP]
simp only [not_exists, RelEmbedding.coe_mk, Set.mem_image, not_and, Function.Embedding.coeFn_mk, Ne.def,
  toPowerSeries_symm_apply_coeff, mem_support, imp_true_iff, not_false_iff]
[GOAL]
R : Type u
R' : Type u_1
inst✝³ : Semiring R
inst✝² : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : PowerSeries S
⊢ ↑(ofPowerSeries ℤ S) (r • x) = r • ↑(ofPowerSeries ℤ S) x
[PROOFSTEP]
ext
[GOAL]
case coeff.h
R : Type u
R' : Type u_1
inst✝³ : Semiring R
inst✝² : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : PowerSeries S
x✝ : ℤ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ S) (r • x)) x✝ = HahnSeries.coeff (r • ↑(ofPowerSeries ℤ S) x) x✝
[PROOFSTEP]
simp [coeff_coe, coeff_smul, smul_ite]