awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
hφ' :
  ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
⊢ Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)

Tactic:
rcases hφ' with ⟨ne, hφ'⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
hφ' :
  ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))

Tactic:
rcases hφ' with ⟨ne, hφ'⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
⊢ (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne

Tactic:
simp only [← h, WithTop.coe_eq_coe] at hφ'

Premises used: WithTop.coe_eq_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
this :
  Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))
⊢ ¬φ d = 0

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

Premises used: ofLex_toLex, ne_eq, toLex_symm_eq, Function.mem_support, Set.mem_image_equiv
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
this : ¬φ d = 0
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
apply this
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
suffices :
  Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

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
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
rw :
  Membership.mem (γ := Set (Lex (σ →₀ ℕ))) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    (WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne)
⊢ Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))

Tactic:
rw [hφ']
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
⊢ Membership.mem (γ := Set (Lex (σ →₀ ℕ))) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    (WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne)

Tactic:
apply WellFounded.min_mem

Premises used: WellFounded.min_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
pos : ∀ (hφ : φ = 0), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
neg : ∀ (hφ : ¬φ = 0), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
by_cases hφ : φ = 0
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : φ = 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
simp only [hφ, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
⊢ Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)

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

Premises used: MvPowerSeries.lexOrder_def_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))

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

Premises used: MvPowerSeries.lexOrder_def_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
⊢ (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne

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

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
h₁ :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
⊢ φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))

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

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
h :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
neg : ∀ (h' : ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)), False
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
by_contra h'
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
h :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
h' : ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ False

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

Premises used: Iff.mpr, Function.support, WellFounded.not_lt_min, Set.image, DFunLike.coe, Set.mem_image_equiv, toLex
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
h :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
h' : ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ False

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

Premises used: Iff.mpr, Function.support, WellFounded.not_lt_min, Set.image, DFunLike.coe, Set.mem_image_equiv, toLex
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
rw : ¬(↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ False

Tactic:
h (coeff_eq_zero_of_lt_lexOrder h')

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ False

Tactic:
exact h (coeff_eq_zero_of_lt_lexOrder h')

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
mp :
  w ≤ φ.lexOrder →
    ∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
mpr :
  (∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
    w ≤ φ.lexOrder
⊢ w ≤ φ.lexOrder ↔
    ∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
mp : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
apply coeff_eq_zero_of_lt_lexOrder

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_lexOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder

Tactic:
lt_of_lt_of_le hd h

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : w ≤ φ.lexOrder
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder

Tactic:
exact lt_of_lt_of_le hd h

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
mpr : ¬φ.lexOrder < w
⊢ w ≤ φ.lexOrder

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
rw : ¬φ.lexOrder = ⊤
⊢ φ ≠ 0

Tactic:
rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]

Premises used: ne_eq, MvPowerSeries.lexOrder_eq_top_iff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
⊢ ¬φ.lexOrder = ⊤

Tactic:
ne_top_of_lt h'

Premises used: ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
⊢ ¬φ.lexOrder = ⊤

Tactic:
exact ne_top_of_lt h'

Premises used: ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
⊢ φ ≠ 0

Tactic:
have hφ : φ ≠ 0 := by
      rw [ne_eq, ← lexOrder_eq_top_iff_eq_zero]
      exact ne_top_of_lt h'
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
mpr : ∀ (d : σ →₀ ℕ) (hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))), False
⊢ False

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

Premises used: MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
⊢ False

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

Premises used: MvPowerSeries.coeff_ne_zero_of_lexOrder, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
mpr : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w
⊢ False

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

Premises used: MvPowerSeries.coeff_ne_zero_of_lexOrder, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
mpr mpr₁ mpr₂ mpr₃ : φ.lexOrder < w
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w

Tactic:
rwa [← hd]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
rw :
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < min φ.lexOrder ψ.lexOrder →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (φ + ψ) : R) (0 : R)
⊢ min φ.lexOrder ψ.lexOrder ≤ (φ + ψ).lexOrder

Tactic:
rw [le_lexOrder_iff]

Premises used: MvPowerSeries.le_lexOrder_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < min φ.lexOrder ψ.lexOrder
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∧
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder

Tactic:
simp only [lt_min_iff] at hd

Premises used: lt_min_iff