awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ f.eval x <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
have rw : ∃ (i : FiniteArchimedeanClass M),
  (∀ j < i,
      Eq.{u_3 + 1} (α := R)
        (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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.eval x)) 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 [HahnSeries.lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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)
⊢ ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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.eval x)) 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)
have hxy0 : (↑y : M) - x ≠ 0
Tactic: have hxy0 : y.val - x ≠ 0 := sub_ne_zero_of_ne h.ne.symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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.eval x)) 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)
have refine_1 : ∀ j < FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0,
  Eq.{u_3 + 1} (α := R)
    (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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)
Tactic: refine ⟨mk (y.val - x) hxy0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
refine_1 :
  ∀ j < FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0,
    Eq.{u_3 + 1} (α := R)
      (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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)
⊢ ∃ (i : FiniteArchimedeanClass M),
    (∀ j < i,
        Eq.{u_3 + 1} (α := R)
          (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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.eval x)) 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)
have refine_2 : LT.lt.{u_3} (α := R)
  (coeff (Γ := FiniteArchimedeanClass M)
    ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))
    (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0))
  (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: refine ⟨mk (y.val - x) hxy0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
j : FiniteArchimedeanClass M
hj : j < FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0
⊢ Eq.{u_3 + 1} (α := R)
    (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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)
have refine_1 : Membership.mem (γ := Submodule K M) (ball K j) ((↑y : M) - x)
Tactic: apply evalCoeff_eq
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ LT.lt.{u_3} (α := R)
    (coeff (Γ := FiniteArchimedeanClass M)
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))
      (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0))
    (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))
have refine_2 : f.evalCoeff x (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0) <
  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: suffices f.evalCoeff x (mk (y.val - x) hxy0) < (ofLex (f.val y)).coeff (mk _ hxy0) by
    simpa [eval] using this
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ f.evalCoeff x (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0) <
    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)
have refine_2 : ∀ (z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain)
  (hz : Membership.mem (γ := Submodule K M) (ball K (FiniteArchimedeanClass.mk ((↑y : M) - x) sorry)) ((↑z : M) - x)),
  f.evalCoeff x (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0) <
    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: obtain ⟨z, hz⟩ := f.exists_sub_mem_ball hx y
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ f.evalCoeff x (FiniteArchimedeanClass.mk ((↑y : M) - x) hxy0) <
    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)
have refine_2 : 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) sorry))
  (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: rw [f.evalCoeff_eq hz]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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)
⊢ 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))
have this : (↑z : M) ≠ x
Tactic: have : z ≠ x := by rintro rfl; exact hx z.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ z < y
have change : (↑z : M) < (↑y : M)
Tactic: change z.val < y.val
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ (↑z : M) < (↑y : M)
have refine : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑y : M) - x)) (ArchimedeanClass.mk ((↑z : M) - x))
Tactic: refine (sub_lt_sub_iff_right x).mp <|
      ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg ?_ (sub_nonneg_of_le h.le)
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ 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))
have hzy : z < y
Tactic: have hzy : z < y := by
    change z.val < y.val
    refine (sub_lt_sub_iff_right x).mp <|
      ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg ?_ (sub_nonneg_of_le h.le)
    simpa using hz (by simpa [sub_eq_zero])
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ (↑z : M) - (↑y : M) ≠ 0
have a : (↑z : M) ≠ (↑y : M)
Tactic: apply sub_ne_zero_of_ne
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ 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))
have hzyne : (↑z : M) - (↑y : M) ≠ 0
Tactic: have hzyne : z.val - y.val ≠ 0 := by
    apply sub_ne_zero_of_ne
    simpa using hzy.ne