awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h :
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∧
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
⊢ i ∉ v
have rw : ¬Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
Tactic: rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h :
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∧
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
rw : ¬Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ i ∉ v
have rw₁ : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
Tactic: rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h :
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∧
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
rw : ¬Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₁ : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ i ∉ v
have rw₂ : Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
Tactic: rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h :
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∧
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
rw : ¬Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₁ : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₂ : Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ i ∉ v
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
⊢ a ≤ b ∨ b ≤ a
have hvu : v ⊆ u
Tactic: have hvu : v ⊆ u := by
        intro i h
        rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]
        contrapose! h
        rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
hvu : v ⊆ u
⊢ a ≤ b ∨ b ≤ a
have hv : v.IsWF
Tactic: have hv : v.IsWF :=
        ((ofLex a).isPWO_support'.isWF.union (ofLex b).isPWO_support'.isWF).subset hvu
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
⊢ a ≤ b ∨ b ≤ a
have hji : ∀ j < i,
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
Tactic: have hji (j) : j < i → (ofLex a).coeff j = (ofLex b).coeff j :=
        not_imp_not.mp <| fun h' ↦ hv.not_lt_min hab h'
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
hji :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
⊢ a ≤ b ∨ b ≤ a
have hne : Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
Tactic: have hne : (ofLex a).coeff i ≠ (ofLex b).coeff i := hv.min_mem hab
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
hji :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hne : Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ a ≤ b ∨ b ≤ a
have inr : ∀
  (hi :
    LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)),
  a ≤ b ∨ b ≤ a
Tactic: obtain hi | hi := lt_or_gt_of_ne hne
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
hji :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hne : Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
inr :
  ∀
    (hi :
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)),
    a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a
have inr₁ : ∀
  (hi :
    LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)),
  a ≤ b ∨ b ≤ a
Tactic: obtain hi | hi := lt_or_gt_of_ne hne
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔ 0 < x
have rw : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
Tactic: rw [lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔
    ∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
have mp : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) →
  ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
mp :
  LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) →
    ∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔
    ∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
have mpr : (∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i)
        (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)) →
  LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
hpos : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
have hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: have hne : (ofLex x) ≠ 0 := leadingCoeff_ne_zero.mp hpos.ne.symm
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
hpos : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
have htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
Tactic: have htop : (ofLex x).orderTop ≠ ⊤ := orderTop_ne_top.2 hne
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
hpos : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
⊢ ∃ (i : Γ),
    (∀ j < i,
        Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)) ∧
      LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
have mp : ∀ j < WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) htop,
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
Tactic: refine ⟨(ofLex x).orderTop.untop htop, ?_, by simpa [coeff_untop_eq_leadingCoeff] using hpos⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
⊢ orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
have hg : Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) i
Tactic: apply orderTop_eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) i
⊢ orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
have hx : ∀ (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) g' → i ≤ g'
Tactic: apply orderTop_eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) g
⊢ i ≤ g
have hx : ∀ (hg : g < i), g ∉ support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)
Tactic: contrapose! hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have horder : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
Tactic: have horder : (ofLex x).orderTop = WithTop.some i := by
      apply orderTop_eq_of_le
      · simpa using hi.ne.symm
      · intro g hg
        contrapose! hg
        simpa using (hj g hg).symm
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
horder : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
Tactic: have htop : (ofLex x).orderTop ≠ ⊤ := WithTop.ne_top_iff_exists.mpr ⟨i, horder.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
horder : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: have hne : ofLex x ≠ 0 := orderTop_ne_top.1 htop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
horder : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have horder' : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) htop = i
Tactic: have horder' : (ofLex x).orderTop.untop htop = i := (WithTop.untop_eq_iff _).mpr horder
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
horder : orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)
htop : Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤
hne : Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
horder' : WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) htop = i
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
have mpr : LT.lt.{u_2} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)
Tactic: rw [leadingCoeff_of_ne_zero hne, horder']
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔ 0 ≤ x
have mp : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) → 0 ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
mp : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) → 0 ≤ x
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔ 0 ≤ x
have mpr : 0 ≤ x → LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ 0 ≤ x
have mp : ∀ (heq : Eq.{u_2 + 1} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))), 0 ≤ x
Tactic: obtain heq | hlt := h.eq_or_lt
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
mp : ∀ (heq : Eq.{u_2 + 1} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))), 0 ≤ x
⊢ 0 ≤ x
have mp₁ : ∀ (hlt : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))), 0 ≤ x
Tactic: obtain heq | hlt := h.eq_or_lt