awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
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
⊢ a ≤ b ∨ b ≤ a

Tactic:
obtain hi | hi := lt_or_gt_of_ne hne

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
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:
Or.inl (le_of_lt ⟨i, hji, hi⟩)

Premises used: le_of_lt, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
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:
exact Or.inl (le_of_lt ⟨i, hji, hi⟩)
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
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:
Or.inr (le_of_lt ⟨i, fun j hj ↦ (hji j hj).symm, hi⟩)

Premises used: le_of_lt, And.intro, Exists.intro, Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
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:
exact Or.inr (le_of_lt ⟨i, fun j hj ↦ (hji j hj).symm, hi⟩)
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
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)
⊢ LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔ 0 < x

Tactic:
rw [lt_iff]

Premises used: HahnSeries.lt_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
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))
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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))
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
have hne : (ofLex x) ≠ 0 := leadingCoeff_ne_zero.mp hpos.ne.symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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⟦Γ⟧)
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)) ⊤
⊢ LT.lt.{u_2} (α := R)
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) htop))
    (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)
      (WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) htop))

Tactic:
simpa [coeff_untop_eq_leadingCoeff] using hpos

Premises used: HahnSeries.coeff_untop_eq_leadingCoeff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)) ⊤
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)
⊢ ∃ (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:
refine ⟨(ofLex x).orderTop.untop htop, ?_, by simpa [coeff_untop_eq_leadingCoeff] using hpos⟩
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)) ⊤
j : Γ
hj : 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:
simpa using (coeff_eq_zero_of_lt_orderTop ((WithTop.lt_untop_iff htop).mp hj)).symm

Premises used: WithTop.lt_untop_iff, Iff.mp, Eq.symm, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
hx :
  ∀ (g' : Γ), Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) g' → i ≤ g'
⊢ orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) = (↑i : WithTop Γ)

Tactic:
apply orderTop_eq_of_le

Premises used: HahnSeries.orderTop_eq_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)
⊢ Membership.mem (γ := Set Γ) (support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) i

Tactic:
simpa using hi.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
hx : ∀ (hg : g < i), g ∉ support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)
⊢ i ≤ g

Tactic:
contrapose! hg
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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 : g < i
⊢ g ∉ support.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)

Tactic:
simpa using (hj g hg).symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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 Γ)

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
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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 Γ)
⊢ 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⟩
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)) ⊤
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
have hne : ofLex x ≠ 0 := orderTop_ne_top.1 htop
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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⟦Γ⟧)
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
mpr : LT.lt.{u_2} (α := R) 0 (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:
rw [leadingCoeff_of_ne_zero hne, horder']

Premises used: HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) i)

Tactic:
simpa using hi
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
mpr : 0 ≤ x → LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ↔ 0 ≤ x

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
mp₁ : ∀ (hlt : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))), 0 ≤ x
⊢ 0 ≤ x

Tactic:
obtain heq | hlt := h.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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))
heq : Eq.{u_2 + 1} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ 0 ≤ x

Tactic:
le_of_eq (leadingCoeff_eq_zero.mp heq.symm).symm

Premises used: Iff.mp, HahnSeries.leadingCoeff_eq_zero, le_of_eq, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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))
heq : Eq.{u_2 + 1} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ 0 ≤ x

Tactic:
exact le_of_eq (leadingCoeff_eq_zero.mp heq.symm).symm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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))
hlt : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ 0 ≤ x

Tactic:
(leadingCoeff_pos_iff.mp hlt).le

Premises used: LT.lt.le, HahnSeries.leadingCoeff_pos_iff, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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))
hlt : LT.lt.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ 0 ≤ x

Tactic:
exact (leadingCoeff_pos_iff.mp hlt).le

Premises used: LT.lt.le, HahnSeries.leadingCoeff_pos_iff, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
mpr :
  ∀ (h : LE.le (α := Lex R⟦Γ⟧) 0 0),
    LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))
mpr₁ : ∀ (hlt : 0 < x), LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))

Tactic:
obtain rfl | hlt := h.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
h : LE.le (α := Lex R⟦Γ⟧) 0 0
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 0))

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))

Tactic:
(leadingCoeff_pos_iff.mpr hlt).le

Premises used: Iff.mpr, LT.lt.le, HahnSeries.leadingCoeff_pos_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))

Tactic:
exact (leadingCoeff_pos_iff.mpr hlt).le

Premises used: Iff.mpr, LT.lt.le, HahnSeries.leadingCoeff_pos_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0 ↔ x < 0

Tactic:
simp [← not_le]

Premises used: not_le
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) 0 ↔ x ≤ 0

Tactic:
simp [← not_lt]

Premises used: not_lt
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
inst_2 : AddCommMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
inl : ∀ (hab : a ≤ a), a + c ≤ a + c
inr : ∀ (hlt : a < b), a + c ≤ b + c
⊢ a + c ≤ b + c

Tactic:
obtain rfl | hlt := hab.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl