-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_monomial {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] :
    weightedOrder w (monomial R d a) = if a = 0 then (⊤ : ℕ∞) else weight w d

Proof state:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff R d_1) ((monomial R d) a) = 0

Tactic:
intro b hb

Result:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff R b) ((monomial R d) a) = 0

Proof state:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d

Tactic:
intro h

Result:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (coeff R d) ((monomial R d) a) ≠ 0 ∧ (weight w) d = (weight w) d

Tactic:
simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]

Result:
no goals

Proof state:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ (coeff R b) ((monomial R d) a) = 0

Tactic:
rw [coeff_monomial, if_neg]

Result:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d

Proof state:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h✝ : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
h : b = d
⊢ False

Tactic:
simp only [h, lt_self_iff_false] at hb

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial R d) a) = ⊤

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

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial R d) a) = ↑((weight w) d)

Tactic:
rw [weightedOrder_eq_nat]

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (coeff R d_1) ((monomial R d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff R d_1) ((monomial R d) a) = 0

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ d_1, (coeff R d_1) ((monomial R d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d) ∧
    ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff R d_1) ((monomial R d) a) = 0

Tactic:
constructor

Result:
case neg.left
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (coeff R d_1) ((monomial R d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d

case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff R d_1) ((monomial R d) a) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ weightedOrder w ((monomial R d) a) = if a = 0 then ⊤ else ↑((weight w) d)

Tactic:
split_ifs with h

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : a = 0
⊢ weightedOrder w ((monomial R d) a) = ⊤

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder w ((monomial R d) a) = ↑((weight w) d)

Proof state:
case neg.left
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (coeff R d_1) ((monomial R d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d

Tactic:
use d

Result:
case h
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ (coeff R d) ((monomial R d) a) ≠ 0 ∧ (weight w) d = (weight w) d