R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : ¬↑n ≤ order φ
⊢ False
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
⊢ ↑n ≤ order φ
by_contra H
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : order φ < ↑n
⊢ False
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : ¬↑n ≤ order φ
⊢ False
rw [not_le] at H
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : order φ < ↑n
this : (order φ).Dom
⊢ False
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : order φ < ↑n
⊢ False
have : (order φ).Dom := PartENat.dom_of_le_natCast H.le
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
this : (order φ).Dom
H : Part.get (order φ) this < n
⊢ False
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
H : order φ < ↑n
this : (order φ).Dom
⊢ False
rw [← PartENat.natCast_get this, PartENat.coe_lt_coe] at H
no goals
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
h : ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
this : (order φ).Dom
H : Part.get (order φ) this < n
⊢ False
exact coeff_order this (h _ H)