R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ order φ ≤ ↑n
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
⊢ order φ ≤ ↑n
have _ :  ∃ n, coeff R n φ ≠ 0 := Exists.intro n h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0)) ≤ ↑n

case hnc
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ¬φ = 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ order φ ≤ ↑n
rw [order, dif_neg]
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ∃ m, m ≤ n ∧ ↑(coeff R m) φ ≠ 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0)) ≤ ↑n
simp only [PartENat.coe_le_coe, Nat.find_le_iff]
no goals
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ∃ m, m ≤ n ∧ ↑(coeff R m) φ ≠ 0
exact ⟨n, le_rfl, h⟩
no goals
case hnc
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
x✝ : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ¬φ = 0
exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩