case ofNat
R : Type u
R' : Type ?u.236572
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

case negSucc
R : Type u
R' : Type ?u.236572
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
R : Type u
R' : Type ?u.236572
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
cases i
no goals
case ofNat
R : Type u
R' : Type ?u.236572
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
rw [Int.ofNat_eq_coe, coeff_coe_powerSeries, if_neg (Int.coe_nat_nonneg _).not_lt,
  Int.natAbs_ofNat]
case negSucc
R : Type u
R' : Type ?u.236572
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)
case negSucc
R : Type u
R' : Type ?u.236572
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
rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]
no goals
case negSucc
R : Type u
R' : Type ?u.236572
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)
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]