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
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ↑(single (order x)) 1 * ↑(ofPowerSeries ℤ R) (powerSeriesPart x) = x
ext n
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
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
rw [← sub_add_cancel n x.order, single_mul_coeff_add, sub_add_cancel, one_mul]
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

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
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
by_cases h : x.order ≤ n
no goals
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
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]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ¬order x ≤ n
⊢ 0 = HahnSeries.coeff x n

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) }
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
rw [ofPowerSeries_apply, embDomain_notin_range]
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : 0 ≠ HahnSeries.coeff x n
⊢ order x ≤ n
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ¬order x ≤ n
⊢ 0 = HahnSeries.coeff x n
contrapose! h
no goals
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : 0 ≠ HahnSeries.coeff x n
⊢ order x ≤ n
exact order_le_of_coeff_ne_zero h.symm
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
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) }
contrapose! h
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n
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
simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ order x ≤ n
case neg
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n
obtain ⟨m, hm⟩ := h
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ 0 ≤ ↑m
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ order x ≤ n
rw [← sub_nonneg, ← hm]
no goals
case neg.intro
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ 0 ≤ ↑m
simp only [Nat.cast_nonneg]