-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem le_lexOrder_iff {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ ℕ))} :
    w ≤ lexOrder φ ↔ (∀ (d : σ →₀ ℕ) (_ : toLex d < w), coeff R d φ = 0)

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
⊢ False

Tactic:
obtain ⟨d, hd⟩ := exists_finsupp_eq_lexOrder_of_ne_zero hφ

Result:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ False

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder → ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0

Tactic:
intro h d hd

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : ↑(toLex d) < w
⊢ (coeff R d) φ = 0

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
⊢ ¬φ.lexOrder < w

Tactic:
intro h'

Result:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
⊢ φ ≠ 0

Tactic:
rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
⊢ ¬φ.lexOrder = ⊤

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
⊢ ¬φ.lexOrder = ⊤

Tactic:
exact ne_top_of_lt h'

Result:
no goals

Proof state:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ False

Tactic:
refine coeff_ne_zero_of_lexOrder hd.symm (h d ?_)

Result:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ ↑(toLex d) < w

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder ↔ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0

Tactic:
constructor

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder → ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ (∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0) → w ≤ φ.lexOrder

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ (∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0) → w ≤ φ.lexOrder

Tactic:
intro h

Result:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
⊢ w ≤ φ.lexOrder

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
⊢ False

Tactic:
have hφ : φ ≠ 0 := by
  rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
  exact ne_top_of_lt h'

Result:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
⊢ False

Proof state:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ ↑(toLex d) < w

Tactic:
rwa [← hd]

Result:
no goals

Proof state:
case mp.h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : ↑(toLex d) < w
⊢ ↑(toLex d) < φ.lexOrder

Tactic:
exact lt_of_lt_of_le hd h

Result:
no goals

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
⊢ w ≤ φ.lexOrder

Tactic:
rw [← not_lt]

Result:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0
⊢ ¬φ.lexOrder < w

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : ↑(toLex d) < w
⊢ (coeff R d) φ = 0

Tactic:
apply coeff_eq_zero_of_lt_lexOrder

Result:
case mp.h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : ↑(toLex d) < w
⊢ ↑(toLex d) < φ.lexOrder