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 : (↑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 :
  ∀ (hi : i < FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0),
    LE.le.{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⟧)
            y))
        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⟧)
            z))
        i)
⊢ FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0 ≤ i

Tactic:
contrapose! hi
-- 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 : i < FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0
⊢ i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne

Tactic:
rw [hzyclass] at hi
-- 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 : i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne
⊢ Membership.mem (γ := Submodule K M) (ball K i) ((↑z : M) - (↑y : M))

Tactic:
have hzy : z.val - y.val ∈ ball K i := fun _ ↦ hi
-- 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 : i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne
hzy : Membership.mem (γ := Submodule K M) (ball K i) ((↑z : M) - (↑y : M))
⊢ Membership.mem (γ := Submodule K M) (ball K i) ((↑y : M) - (↑y : M))

Tactic:
simp
-- 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 : i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne
hzy : Membership.mem (γ := Submodule K M) (ball K i) ((↑z : M) - (↑y : M))
⊢ i ≤ i

Tactic:
simp
-- 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 : i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne
hzy : Membership.mem (γ := Submodule K M) (ball K i) ((↑z : M) - (↑y : M))
⊢ LE.le.{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⟧)
          y))
      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⟧)
          z))
      i)

Tactic:
exact (f.coeff_eq_of_mem y.val (by simp) hzy (by simp)).le

Premises used: HahnEmbedding.Partial.coeff_eq_of_mem, Eq.le, 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 : (↑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)
⊢ i = FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0

Tactic:
have hieq : i = mk (y.val - x) hxy0 := by
    apply le_antisymm
    · by_contra! hlt
      obtain hj := sub_eq_zero_of_eq (hj (mk _ hxy0) hlt)
      contrapose! hj
      rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub, hzyclass]
      apply f.coeff_ne_zero
    · contrapose! hi
      rw [hzyclass] at hi
      have hzy : z.val - y.val ∈ ball K i := fun _ ↦ hi
      exact (f.coeff_eq_of_mem y.val (by simp) hzy (by simp)).le
-- 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)
hieq : i = FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0
⊢ LT.lt.{u_3} (α := 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))
      (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯))
    (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⟧)
          y))
      (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0))

Tactic:
hieq ▸ hi

Premises used: Eq.rec
-- 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)
hieq : i = FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0
⊢ LT.lt.{u_3} (α := 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))
      (FiniteArchimedeanClass.mk ((↑y : M) - x) ⋯))
    (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⟧)
          y))
      (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0))

Tactic:
exact hieq ▸ hi
-- 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
c : K
hc : c ≠ 0
contrapose :
  ∀ (hx : -c • x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
contrapose hx
-- 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
c : K
hc : c ≠ 0
hx : -c • x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
rwa :
  ∀ (hx : -(c • x) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
rwa₁ :
  ∀ (hx : c • x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hx : x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at hx

Premises used: neg_mem_iff, neg_smul, Submodule.smul_mem_iff