-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem X_pow_order_dvd (h : order φ < ⊤) : X ^ (order φ).lift h ∣ φ

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ =
    ∑ x ∈ Finset.filter (fun x => x.1 = φ.order.lift h) (antidiagonal n), (coeff R (x.2 + φ.order.lift h)) φ

Tactic:
rw [Finset.filter_fst_eq_antidiagonal n ((order φ).lift h)]

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ =
    ∑ x ∈ if φ.order.lift h ≤ n then {(φ.order.lift h, n - φ.order.lift h)} else ∅, (coeff R (x.2 + φ.order.lift h)) φ

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ X ^ φ.order.lift h ∣ φ

Tactic:
refine ⟨PowerSeries.mk fun n => coeff R (n + (order φ).lift h) φ, ?_⟩

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ φ = X ^ φ.order.lift h * mk fun n => (coeff R (n + φ.order.lift h)) φ

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ = (coeff R n) (X ^ φ.order.lift h * mk fun n => (coeff R (n + φ.order.lift h)) φ)

Tactic:
simp only [coeff_mul, coeff_X_pow, coeff_mk, boole_mul, Finset.sum_ite,
  Finset.sum_const_zero, add_zero]

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ =
    ∑ x ∈ Finset.filter (fun x => x.1 = φ.order.lift h) (antidiagonal n), (coeff R (x.2 + φ.order.lift h)) φ

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ =
    ∑ x ∈ if φ.order.lift h ≤ n then {(φ.order.lift h, n - φ.order.lift h)} else ∅, (coeff R (x.2 + φ.order.lift h)) φ

Tactic:
split_ifs with hn

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : φ.order.lift h ≤ n
⊢ (coeff R n) φ = ∑ x ∈ {(φ.order.lift h, n - φ.order.lift h)}, (coeff R (x.2 + φ.order.lift h)) φ

case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ (coeff R n) φ = ∑ x ∈ ∅, (coeff R (x.2 + φ.order.lift h)) φ

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ (coeff R n) φ = ∑ x ∈ ∅, (coeff R (x.2 + φ.order.lift h)) φ

Tactic:
simp only [Finset.sum_empty]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ (coeff R n) φ = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : φ.order.lift h ≤ n
⊢ (coeff R n) φ = ∑ x ∈ {(φ.order.lift h, n - φ.order.lift h)}, (coeff R (x.2 + φ.order.lift h)) φ

Tactic:
simp [tsub_add_cancel_of_le hn]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ ↑n < φ.order

Tactic:
simpa using hn

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
⊢ φ = X ^ φ.order.lift h * mk fun n => (coeff R (n + φ.order.lift h)) φ

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
⊢ (coeff R n) φ = (coeff R n) (X ^ φ.order.lift h * mk fun n => (coeff R (n + φ.order.lift h)) φ)

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ (coeff R n) φ = 0

Tactic:
refine coeff_of_lt_order _ ?_

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ.order < ⊤
n : ℕ
hn : ¬φ.order.lift h ≤ n
⊢ ↑n < φ.order