English
If toLex d equals the leading lex order of φ, then the coefficient of φ at d is nonzero.
Русский
Если toLex d равно ведущему лексическому члену φ, то коэффициент φ при d не равен нулю.
LaTeX
$$$\text{toLex } d = \phi.lexOrder \Rightarrow \operatorname{coeff}(d,\phi) \neq 0$$$
Lean4
theorem coeff_ne_zero_of_lexOrder {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : toLex d = lexOrder φ) : coeff d φ ≠ 0 :=
by
have hφ : φ ≠ 0 := by simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]
have hφ' := lexOrder_def_of_ne_zero hφ
rcases hφ' with ⟨ne, hφ'⟩
simp only [← h, WithTop.coe_eq_coe] at hφ'
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
rw [hφ']
apply WellFounded.min_mem
