R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ φ = X ^ Part.get (order φ) h * mk fun n => ↑(coeff R (n + Part.get (order φ) h)) φ
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ X ^ Part.get (order φ) h ∣ φ
refine' ⟨PowerSeries.mk fun n => coeff R (n + (order φ).get h) φ, _⟩
case h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
⊢ ↑(coeff R n) φ = ↑(coeff R n) (X ^ Part.get (order φ) h * mk fun n => ↑(coeff R (n + Part.get (order φ) h)) φ)
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ φ = X ^ Part.get (order φ) h * mk fun n => ↑(coeff R (n + Part.get (order φ) h)) φ
ext n
case h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
⊢ ↑(coeff R n) φ =
    ∑ x in if Part.get (order φ) h ≤ n then {(Part.get (order φ) h, n - Part.get (order φ) h)} else ∅,
      ↑(coeff R (x.snd + Part.get (order φ) h)) φ
case h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
⊢ ↑(coeff R n) φ = ↑(coeff R n) (X ^ Part.get (order φ) h * mk fun n => ↑(coeff R (n + Part.get (order φ) h)) φ)
simp only [coeff_mul, coeff_X_pow, coeff_mk, boole_mul, Finset.sum_ite,
  Finset.Nat.filter_fst_eq_antidiagonal, Finset.sum_const_zero, add_zero]
case h.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ =
    ∑ x in {(Part.get (order φ) h, n - Part.get (order φ) h)}, ↑(coeff R (x.snd + Part.get (order φ) h)) φ

case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ = ∑ x in ∅, ↑(coeff R (x.snd + Part.get (order φ) h)) φ
case h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
⊢ ↑(coeff R n) φ =
    ∑ x in if Part.get (order φ) h ≤ n then {(Part.get (order φ) h, n - Part.get (order φ) h)} else ∅,
      ↑(coeff R (x.snd + Part.get (order φ) h)) φ
split_ifs with hn
no goals
case h.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ =
    ∑ x in {(Part.get (order φ) h, n - Part.get (order φ) h)}, ↑(coeff R (x.snd + Part.get (order φ) h)) φ
simp [tsub_add_cancel_of_le hn]
case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ = 0
case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ = ∑ x in ∅, ↑(coeff R (x.snd + Part.get (order φ) h)) φ
simp only [Finset.sum_empty]
case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑n < order φ
case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑(coeff R n) φ = 0
refine' coeff_of_lt_order _ _
no goals
case h.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
n : ℕ
hn : ¬Part.get (order φ) h ≤ n
⊢ ↑n < order φ
simpa [PartENat.coe_lt_iff] using fun _ => hn