case inl
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ order (↑(monomial R n) a) = ⊤

case inr
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ order (↑(monomial R n) a) = ↑n
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ order (↑(monomial R n) a) = if a = 0 then ⊤ else ↑n
split_ifs with h
no goals
case inl
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ order (↑(monomial R n) a) = ⊤
rw [h, order_eq_top, LinearMap.map_zero]
case inr
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∀ (i : ℕ), ↑i = ↑n → ↑(coeff R i) (↑(monomial R n) a) ≠ 0) ∧
    ∀ (i : ℕ), ↑i < ↑n → ↑(coeff R i) (↑(monomial R n) a) = 0
case inr
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ order (↑(monomial R n) a) = ↑n
rw [order_eq]
case inr.left
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ ↑(coeff R i) (↑(monomial R n) a) ≠ 0

case inr.right
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ ↑(coeff R i) (↑(monomial R n) a) = 0
case inr
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∀ (i : ℕ), ↑i = ↑n → ↑(coeff R i) (↑(monomial R n) a) ≠ 0) ∧
    ∀ (i : ℕ), ↑i < ↑n → ↑(coeff R i) (↑(monomial R n) a) = 0
constructor <;> intro i hi
case inr.left
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ ↑(coeff R i) (↑(monomial R n) a) ≠ 0
case inr.left
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ ↑(coeff R i) (↑(monomial R n) a) ≠ 0
rw [PartENat.natCast_inj] at hi
no goals
case inr.left
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ ↑(coeff R i) (↑(monomial R n) a) ≠ 0
rwa [hi, coeff_monomial_same]
case inr.right
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ↑(coeff R i) (↑(monomial R n) a) = 0
case inr.right
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ ↑(coeff R i) (↑(monomial R n) a) = 0
rw [PartENat.coe_lt_coe] at hi
case inr.right.hnc
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n
case inr.right
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ↑(coeff R i) (↑(monomial R n) a) = 0
rw [coeff_monomial, if_neg]
no goals
case inr.right.hnc
R : Type u_1
inst✝¹ : Semiring R
φ : PowerSeries R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n
exact ne_of_lt hi