awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this_1 : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
this : (↑y : M) - (↑z : M) = (↑y : M) - x + (x - (↑z : M))
refine : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x)) (ArchimedeanClass.mk (x - (↑z : M)))
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x))
    (ArchimedeanClass.mk ((↑y : M) - x + (x - (↑z : M))))

Tactic:
refine (ArchimedeanClass.mk_add_eq_mk_left ?_).symm

Premises used: ArchimedeanClass.mk_add_eq_mk_left, Eq.symm
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this_1 : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
this : (↑y : M) - (↑z : M) = (↑y : M) - x + (x - (↑z : M))
rw : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x)) (ArchimedeanClass.mk ((↑z : M) - x))
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x)) (ArchimedeanClass.mk (x - (↑z : M)))

Tactic:
rw [ArchimedeanClass.mk_sub_comm x z.val]

Premises used: ArchimedeanClass.mk_sub_comm, Subtype.val
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this_1 : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
this : (↑y : M) - (↑z : M) = (↑y : M) - x + (x - (↑z : M))
⊢ Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑z : M) - x)) ⊤

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this_1 : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
this : (↑y : M) - (↑z : M) = (↑y : M) - x + (x - (↑z : M))
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x)) (ArchimedeanClass.mk ((↑z : M) - x))

Tactic:
simpa using hz (by simpa [sub_eq_zero])
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
⊢ Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)

Tactic:
have hzyclass : mk (y.val - x) hxy0 = mk (z.val - y.val) hzyne := by
    suffices ArchimedeanClass.mk (y.val - x) = .mk (z.val - y.val) by
      simpa [Subtype.ext_iff] using this
    have : y.val - z.val = y.val - x + (x - z.val) := by abel
    rw [ArchimedeanClass.mk_sub_comm z.val y.val, this]
    refine (ArchimedeanClass.mk_add_eq_mk_left ?_).symm
    rw [ArchimedeanClass.mk_sub_comm x z.val]
    simpa using hz (by simpa [sub_eq_zero])
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
⊢ ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                z))
            j)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                y))
            j)) ∧
      LT.lt.{u_3} (α := R)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              z))
          i)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              y))
          i)

Tactic:
rw [← f.prop.strictMono.lt_iff_lt, HahnSeries.lt_iff] at hzy

Premises used: StrictMono.lt_iff_lt, HahnEmbedding.IsPartial.strictMono, Subtype.prop, HahnSeries.lt_iff
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
hzy₁ :
  ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                z))
            j)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                y))
            j)) ∧
      LT.lt.{u_3} (α := R)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              z))
          i)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              y))
          i)
⊢ (↑z : M) - (↑y : M) ≠ 0

Tactic:
rw [← f.prop.strictMono.lt_iff_lt, HahnSeries.lt_iff] at hzy

Premises used: StrictMono.lt_iff_lt, HahnEmbedding.IsPartial.strictMono, Subtype.prop, HahnSeries.lt_iff
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzy : z < y
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
hzy₁ :
  ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                z))
            j)
          (coeff
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
                y))
            j)) ∧
      LT.lt.{u_3} (α := R)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              z))
          i)
        (coeff
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              y))
          i)
hzyne₁ : (↑z : M) - (↑y : M) ≠ 0
⊢ Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne₁)

Tactic:
rw [← f.prop.strictMono.lt_iff_lt, HahnSeries.lt_iff] at hzy

Premises used: StrictMono.lt_iff_lt, HahnEmbedding.IsPartial.strictMono, Subtype.prop, HahnSeries.lt_iff
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
i : FiniteArchimedeanClass M
hj :
  ∀ j < i,
    Eq.{u_3 + 1} (α := R)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            z))
        j)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))
        j)
hi :
  LT.lt.{u_3} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      i)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
      i)
a : i ≤ FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0
a₁ : FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0 ≤ i
⊢ i = FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
i : FiniteArchimedeanClass M
hj :
  ∀ j < i,
    Eq.{u_3 + 1} (α := R)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            z))
        j)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))
        j)
hi :
  LT.lt.{u_3} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      i)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
      i)
a : ∀ (hlt : FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0 < i), False
⊢ i ≤ FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0

Tactic:
by_contra! hlt
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : x < (↑y : M)
hxy0 : (↑y : M) - x ≠ 0
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯)) ((↑z : M) - x)
this : (↑z : M) ≠ x
hzyne : (↑z : M) - (↑y : M) ≠ 0
hzyclass :
  Eq (α := FiniteArchimedeanClass M) (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0)
    (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne)
i : FiniteArchimedeanClass M
hj_1 :
  ∀ j < i,
    Eq.{u_3 + 1} (α := R)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            z))
        j)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))
        j)
hi :
  LT.lt.{u_3} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      i)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
      i)
hlt : FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0 < i
hj : True
⊢ Ne.{u_3 + 1} (α := R)
    (coeff (Γ := FiniteArchimedeanClass M)
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (z - y)))
      (FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne))
    0

Tactic:
apply f.coeff_ne_zero

Premises used: HahnEmbedding.Partial.coeff_ne_zero