R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ ↑(coeff R (Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))) φ ≠ 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ ↑(coeff R (Part.get (order φ) h)) φ ≠ 0
simp only [order, order_finite_iff_ne_zero.mp h, not_false_iff, dif_neg, PartENat.get_natCast']
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h✝ : (order φ).Dom
h : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ↑(coeff R (Nat.find h)) φ ≠ 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : (order φ).Dom
⊢ ↑(coeff R (Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))) φ ≠ 0
generalize_proofs h
no goals
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h✝ : (order φ).Dom
h : ∃ n, ↑(coeff R n) φ ≠ 0
⊢ ↑(coeff R (Nat.find h)) φ ≠ 0
exact Nat.find_spec h