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

case a
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n✝ : ℕ
⊢ order φ = ↑n✝ ↔ (∀ (i : ℕ), ↑i = ↑n✝ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n✝ → ↑(coeff R i) φ = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n : PartENat
⊢ order φ = n ↔ (∀ (i : ℕ), ↑i = n → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → ↑(coeff R i) φ = 0
induction n using PartENat.casesOn
case a
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ φ = 0 ↔ (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
case a
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ order φ = ⊤ ↔ (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
rw [order_eq_top]
case a.mp
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ φ = 0 → (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0

case a.mpr
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ ((∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0) → φ = 0
case a
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ φ = 0 ↔ (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
constructor
case a.mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) 0 ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) 0 = 0
case a.mp
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ φ = 0 → (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
rintro rfl
case a.mp.left
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ = ⊤
⊢ ↑(coeff R i✝) 0 ≠ 0

case a.mp.right
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ < ⊤
⊢ ↑(coeff R i✝) 0 = 0
case a.mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) 0 ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) 0 = 0
constructor <;> intros
case a.mp.left.h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ = ⊤
⊢ False
case a.mp.left
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ = ⊤
⊢ ↑(coeff R i✝) 0 ≠ 0
exfalso
no goals
case a.mp.left.h
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ = ⊤
⊢ False
exact PartENat.natCast_ne_top ‹_› ‹_›
no goals
case a.mp.right
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
i✝ : ℕ
a✝ : ↑i✝ < ⊤
⊢ ↑(coeff R i✝) 0 = 0
exact (coeff _ _).map_zero
case a.mpr.intro
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
_h₁ : ∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0
h₂ : ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
⊢ φ = 0
case a.mpr
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
⊢ ((∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0) → φ = 0
rintro ⟨_h₁, h₂⟩
case a.mpr.intro.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
_h₁ : ∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0
h₂ : ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
i : ℕ
⊢ ↑(coeff R i) φ = ↑(coeff R i) 0
case a.mpr.intro
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
_h₁ : ∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0
h₂ : ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
⊢ φ = 0
ext i
no goals
case a.mpr.intro.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
_h₁ : ∀ (i : ℕ), ↑i = ⊤ → ↑(coeff R i) φ ≠ 0
h₂ : ∀ (i : ℕ), ↑i < ⊤ → ↑(coeff R i) φ = 0
i : ℕ
⊢ ↑(coeff R i) φ = ↑(coeff R i) 0
exact h₂ i (PartENat.natCast_lt_top i)
no goals
case a
R : Type u_1
inst✝ : Semiring R
φ✝ φ : PowerSeries R
n✝ : ℕ
⊢ order φ = ↑n✝ ↔ (∀ (i : ℕ), ↑i = ↑n✝ → ↑(coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n✝ → ↑(coeff R i) φ = 0
simpa [PartENat.natCast_inj] using order_eq_nat