case inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
⊢ order 0 = ↑n ↔ ↑(coeff R n) 0 ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(coeff R i) 0 = 0

case inr
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
hφ : φ ≠ 0
⊢ order φ = ↑n ↔ ↑(coeff R n) φ ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
⊢ order φ = ↑n ↔ ↑(coeff R n) φ ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
rcases eq_or_ne φ 0 with (rfl | hφ)
no goals
case inr
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : ℕ
hφ : φ ≠ 0
⊢ order φ = ↑n ↔ ↑(coeff R n) φ ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(coeff R i) φ = 0
simp [order, dif_neg hφ, Nat.find_eq_iff]
no goals
case inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
⊢ order 0 = ↑n ↔ ↑(coeff R n) 0 ≠ 0 ∧ ∀ (i : ℕ), i < n → ↑(coeff R i) 0 = 0
simpa using (PartENat.natCast_ne_top _).symm