-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] :
    order (monomial R n a) = if a = 0 then (⊤ : ℕ∞) else n

Proof state:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ (coeff R i) ((monomial R n) a) = 0

Tactic:
rw [coeff_monomial, if_neg]

Result:
case neg.right.hnc
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n

Proof state:
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ ((monomial R n) a).order = if a = 0 then ⊤ else ↑n

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ ((monomial R n) a).order = ⊤

case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial R n) a).order = ↑n

Proof state:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff R i) ((monomial R n) a) = 0

Tactic:
simp only [Nat.cast_lt] at hi

Result:
case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ (coeff R i) ((monomial R n) a) = 0

Proof state:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff R i) ((monomial R n) a) ≠ 0

Tactic:
simp only [Nat.cast_inj] at hi

Result:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ (coeff R i) ((monomial R n) a) ≠ 0

Proof state:
case pos
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ ((monomial R n) a).order = ⊤

Tactic:
rw [h, order_eq_top, LinearMap.map_zero]

Result:
no goals

Proof state:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i = n
⊢ (coeff R i) ((monomial R n) a) ≠ 0

Tactic:
rwa [hi, coeff_monomial_same]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ((monomial R n) a).order = ↑n

Tactic:
rw [order_eq]

Result:
case neg
R : Type u_1
inst✝¹ : Semiring 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

Proof state:
case neg.right.hnc
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : i < n
⊢ ¬i = n

Tactic:
exact ne_of_lt hi

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Semiring 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

Tactic:
constructor <;> intro i hi

Result:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i = ↑n
⊢ (coeff R i) ((monomial R n) a) ≠ 0

case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
i : ℕ
hi : ↑i < ↑n
⊢ (coeff R i) ((monomial R n) a) = 0