awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
n : ℕ
hn :
  LE.le.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
      (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
    ∀
      (_ :
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
      (n : ℕ),
      HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)| <
        |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)|
⊢ LE.le.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (n • x)))

Tactic:
simpa using orderTop_smul_not_lt n (ofLex x)

Premises used: ofLex, HahnSeries.orderTop_smul_not_lt, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
n : ℕ
hn :
  LE.le.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
      (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
    ∀
      (_ :
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
      (n : ℕ),
      HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)| <
        |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)|
⊢ LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (n • x)))

Tactic:
have hgt' : (ofLex y).orderTop < (ofLex (n • x)).orderTop := by
    apply lt_of_lt_of_le hgt
    simpa using orderTop_smul_not_lt n (ofLex x)
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
n : ℕ
hn :
  LE.le.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
      (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
    ∀
      (_ :
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
      (n : ℕ),
      HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)| <
        |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)|
hgt' :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (n • x)))
⊢ |n • x| < |y|

Tactic:
abs_lt_abs_of_orderTop_ofLex hgt'

Premises used: HahnSeries.abs_lt_abs_of_orderTop_ofLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
n : ℕ
hn :
  LE.le.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
      (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
    ∀
      (_ :
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
      (n : ℕ),
      HSMul.hSMul (β := R) n |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)| <
        |leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)|
hgt' :
  LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (n • x)))
⊢ |n • x| < |y|

Tactic:
exact abs_lt_abs_of_orderTop_ofLex hgt'

Premises used: HahnSeries.abs_lt_abs_of_orderTop_ofLex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
rw :
  (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
      (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))) ↔
    Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
      Eq.{u_2 + 1} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
⊢ Eq (α := ArchimedeanClass (Lex R⟦Γ⟧)) (ArchimedeanClass.mk x) (ArchimedeanClass.mk y) ↔
    Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
      Eq.{u_2 + 1} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))

Tactic:
rw [le_antisymm_iff, archimedeanClassMk_le_archimedeanClassMk_iff,
    archimedeanClassMk_le_archimedeanClassMk_iff]

Premises used: le_antisymm_iff, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
      (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
        Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
            (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
          LE.le.{u_2} (α := ArchimedeanClass R)
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
            (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))) →
    Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
      Eq.{u_2 + 1} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))

Tactic:
simpa +contextual [or_imp, ne_of_gt, le_of_lt] using fun _ ↦ le_antisymm

Premises used: le_of_lt, ne_of_gt, or_imp, le_antisymm
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
horder :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hcoeff :
  Eq.{u_2 + 1} (α := ArchimedeanClass R)
    (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
    (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
⊢ (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
    (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))))

Tactic:
⟨.inr ⟨horder, hcoeff.le⟩, .inr ⟨horder.symm, hcoeff.ge⟩⟩

Premises used: Eq.ge, Eq.le, And.intro, Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
horder :
  Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
hcoeff :
  Eq.{u_2 + 1} (α := ArchimedeanClass R)
    (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
    (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
⊢ (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))) ∧
    (LT.lt.{u_1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
        (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∨
      Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y))
          (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ∧
        LE.le.{u_2} (α := ArchimedeanClass R)
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) y)))
          (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x))))

Tactic:
exact ⟨.inr ⟨horder, hcoeff.le⟩, .inr ⟨horder.symm, hcoeff.ge⟩⟩
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
x : Lex R⟦Γ⟧
hx : x ≠ 0
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
hx

Premises used: Lex
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
x : Lex R⟦Γ⟧
hx : x ≠ 0
⊢ Ne (α := R⟦Γ⟧) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
exact hx
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
x : Lex R⟦Γ⟧
hx : x ≠ 0
⊢ Ne.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) ⊤

Tactic:
simp [orderTop_of_ne_zero (show ofLex x ≠ 0 by exact hx)]

Premises used: HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h :
  LE.le (α := FiniteArchimedeanClass (Lex R⟦Γ⟧))
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha) : Lex R⟦Γ⟧) ⋯)
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb) : Lex R⟦Γ⟧) ⋯)
⊢ LE.le (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha) : Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb) : Lex R⟦Γ⟧))

Tactic:
rw [FiniteArchimedeanClass.mk_le_mk] at ⊢ h

Premises used: FiniteArchimedeanClass.mk_le_mk
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h :
  LE.le (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha) : Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb) : Lex R⟦Γ⟧))
rw :
  WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ <
      WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∨
    orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) =
        (↑(WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯) : WithTop Γ) ∧
      LE.le.{u_2} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)))
⊢ WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ <
      WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∨
    WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ =
        WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∧
      LE.le.{u_2} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)))

Tactic:
rw [WithTop.untop_eq_iff]

Premises used: WithTop.untop_eq_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x x_1 : { a : Lex R⟦Γ⟧ // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h :
  LE.le (α := ArchimedeanClass (Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) a ha) : Lex R⟦Γ⟧))
    (ArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : Lex R⟦Γ⟧) ↦ a ≠ 0) b hb) : Lex R⟦Γ⟧))
⊢ WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ⋯ <
      WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯ ∨
    orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) =
        (↑(WithTop.untop (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ⋯) : WithTop Γ) ∧
      LE.le.{u_2} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)))
        (ArchimedeanClass.mk (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)))

Tactic:
simpa using archimedeanClassMk_le_archimedeanClassMk_iff.mp h

Premises used: HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
a : { a : R // a ≠ 0 }
⊢ Ne (α := Lex R⟦Γ⟧)
    ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
        ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
            (a : R) → R⟦Γ⟧)
          (↑a : R)) :
      Lex R⟦Γ⟧)
    (0 : Lex R⟦Γ⟧)

Tactic:
simpa using a.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
x : Lex (Prod.{u_1, u_2} Γ (FiniteArchimedeanClass R))
x_1 x_2 : { a : R // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h :
  LE.le (α := FiniteArchimedeanClass R)
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) a ha) : R) ⋯)
    (FiniteArchimedeanClass.mk (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) b hb) : R) ⋯)
⊢ LT.lt.{u_1} (α := WithTop Γ)
      (orderTop.{u_1, u_2} (R := R)
        ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
          ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
            ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                (a : R) → R⟦Γ⟧)
              (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) a ha) : R)))))
      (orderTop.{u_1, u_2} (R := R)
        ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
          ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
            ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                (a : R) → R⟦Γ⟧)
              (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) b hb) : R))))) ∨
    Eq.{u_1 + 1} (α := WithTop Γ)
        (orderTop.{u_1, u_2} (R := R)
          ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
            ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
              ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                  (a : R) → R⟦Γ⟧)
                (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) a ha) : R)))))
        (orderTop.{u_1, u_2} (R := R)
          ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
            ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
              ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                  (a : R) → R⟦Γ⟧)
                (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) b hb) : R))))) ∧
      LE.le.{u_2} (α := ArchimedeanClass R)
        (ArchimedeanClass.mk
          (leadingCoeff.{u_1, u_2} (Γ := Γ)
            ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
              ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                    (a : R) → R⟦Γ⟧)
                  (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) a ha) : R))))))
        (ArchimedeanClass.mk
          (leadingCoeff.{u_1, u_2} (Γ := Γ)
            ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧)
              ((toLex : (a : R⟦Γ⟧) → Lex R⟦Γ⟧)
                ((single ((ofLex : (a : Lex (Γ × FiniteArchimedeanClass R)) → Γ × FiniteArchimedeanClass R) x).1 :
                    (a : R) → R⟦Γ⟧)
                  (↑(Subtype.mk (p := fun (a : R) ↦ a ≠ 0) b hb) : R))))))

Tactic:
simpa [ha, hb] using h