-- Mathlib/RingTheory/LaurentSeries.lean
theorem single_order_mul_powerSeriesPart (x : R⸨X⸩) :
    (single x.order 1 : R⸨X⸩) * x.powerSeriesPart = x

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
contrapose! h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : n - order x ∈ Set.range ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ }
⊢ order x ≤ n

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
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]

Result:
no goals

Proof state:
case coeff.h
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
by_cases h : x.order ≤ n

Result:
case pos
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Tactic:
rw [ofPowerSeries_apply, embDomain_notin_range]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n

case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉ Set.range ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ }

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n

Tactic:
contrapose! h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : 0 ≠ x.coeff n
⊢ order x ≤ n

Proof state:
case neg.intro
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ order x ≤ n

Tactic:
rw [← sub_nonneg, ← hm]

Result:
case neg.intro
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ 0 ≤ ↑m

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart = x

Tactic:
ext n

Result:
case coeff.h
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart).coeff n = x.coeff n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : n - order x ∈ Set.range ⇑{ toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ }
⊢ order x ≤ n

Tactic:
simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : ∃ y, ↑y = n - order x
⊢ order x ≤ n

Tactic:
obtain ⟨m, hm⟩ := h

Result:
case neg.intro
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ order x ≤ n

Proof state:
case neg.intro
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
m : ℕ
hm : ↑m = n - order x
⊢ 0 ≤ ↑m

Tactic:
simp only [Nat.cast_nonneg]

Result:
no goals

Proof state:
case coeff.h
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart).coeff n = x.coeff n

Tactic:
rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]

Result:
case coeff.h
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
⊢ ((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
n : ℤ
h : 0 ≠ x.coeff n
⊢ order x ≤ n

Tactic:
exact order_le_of_coeff_ne_zero h.symm

Result:
no goals