-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem coeff_eq_zero_of_lt_lexOrder {φ : MvPowerSeries σ R} {d : σ →₀ ℕ}
    (h : toLex d < lexOrder φ) : coeff R d φ = 0

Proof state:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff R d) φ = 0

Tactic:
rw [hφ', WithTop.coe_lt_coe] at h

Result:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff R d) φ = 0

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

Tactic:
rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩

Result:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff R d) φ = 0

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

Tactic:
by_cases hφ : φ = 0

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

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

Proof state:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
h' : ¬(coeff R d) φ = 0
⊢ False

Tactic:
exact WellFounded.not_lt_min _ (toLex '' φ.support) ne (Set.mem_image_equiv.mpr h') h

Result:
no goals

Proof state:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff R d) φ = 0

Tactic:
by_contra h'

Result:
case neg.intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
h : toLex d < ⋯.min (⇑toLex '' Function.support φ) ne
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
h' : ¬(coeff R d) φ = 0
⊢ False

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

Tactic:
simp only [hφ, map_zero]

Result:
no goals