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

Proof state:
case 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ ⋯.min (⇑toLex '' Function.support φ) ne ∈ ⇑toLex '' Function.support φ

Tactic:
apply WellFounded.min_mem

Result:
no goals

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:
have hφ : φ ≠ 0 := by
  simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]

Result:
σ : 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 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ (coeff R d) φ ≠ 0

Tactic:
suffices toLex d ∈ toLex '' φ.support by
  simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex, Function.mem_support, ne_eq] at this
  apply this

Result:
case 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ toLex d ∈ ⇑toLex '' Function.support φ

Proof state:
case 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:
simp only [← h, WithTop.coe_eq_coe] at hφ'

Result:
case 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φ' : toLex d = ⋯.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
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
this : toLex d ∈ ⇑toLex '' Function.support φ
⊢ (coeff R d) φ ≠ 0

Tactic:
simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex, Function.mem_support, ne_eq] at this

Result:
σ : 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
this : ¬φ d = 0
⊢ (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
hφ : φ ≠ 0
hφ' : ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff R d) φ ≠ 0

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

Result:
case 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
hφ : φ ≠ 0
⊢ (coeff R d) φ ≠ 0

Tactic:
have hφ' := lexOrder_def_of_ne_zero hφ

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) = φ.lexOrder
hφ : φ ≠ 0
hφ' : ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.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
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
this : ¬φ d = 0
⊢ (coeff R d) φ ≠ 0

Tactic:
apply this

Result:
no goals

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

Tactic:
simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]

Result:
no goals

Proof state:
case 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ toLex d ∈ ⇑toLex '' Function.support φ

Tactic:
rw [hφ']

Result:
case 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φ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ ⋯.min (⇑toLex '' Function.support φ) ne ∈ ⇑toLex '' Function.support φ