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
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) = x - (↑z : M) + ((↑z : M) - (↑y : M))
hyz : ¬(↑z : M) - (↑y : M) = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M) (hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M))),
    Eq.{u_3 + 1} (α := R)
      (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) c)
      (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))
        c)
h2 :
  ∀ (c : FiniteArchimedeanClass M),
    (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M)) →
      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 - y)))
          c)
        0
⊢ LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))
have neg : ∀
  (h2 :
    LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑z : M) - (↑y : M))) (ArchimedeanClass.mk (x - (↑z : M)))),
  ∃ (c : FiniteArchimedeanClass M),
    (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M)) ∧
      Ne.{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 - y)))
          c)
        0
Tactic: contrapose! h2
Cleared hypotheses: h2
-- 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
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ (↑y : M) - x ≠ 0
have contrapose : ∀ (hx : (↑y : M) - x = 0), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
Tactic: contrapose hx
Cleared hypotheses: hx
-- 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
x : M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : (↑y : M) - x = 0
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have obtain : ∀ (hx : (↑y : M) - (↑y : M) = 0), (↑y : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
Tactic: obtain rfl : x = y.val := (sub_eq_zero.mp hx).symm
Cleared hypotheses: x, hx
-- 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
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
have this : (↑y : M) - x ≠ 0
Tactic: have := val_sub_ne_zero f hx y
-- 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
this : (↑y : M) - x ≠ 0
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
have this₁ : x - (↑y : M) ≠ 0
Tactic: rw [sub_ne_zero, ne_comm, ← sub_ne_zero] at this
Cleared hypotheses: 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
h : Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) ⊤
⊢ Membership.mem (γ := UpperSet (FiniteArchimedeanClass M)) (UpperSet.Ici xy)
    (Subtype.mk (p := fun (A : ArchimedeanClass M) ↦ A ≠ ⊤) (ArchimedeanClass.mk (x - (↑y : M))) h)
have simp : xy ≤ xy
Tactic: simp
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
have hxy : Membership.mem (γ := Submodule K M) (closedBall K xy) (x - (↑y : M))
Tactic: have hxy : x - y.val ∈ closedBall K xy := fun _ ↦ by simp; rfl
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
hxy : ∃ (y_1 : M), Membership.mem (γ := Submodule K M) (ball K xy) y_1 ∧ ∃ z ∈ seed.stratum xy, y_1 + z = 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 obtain : ∀ (u : M) (hu : Membership.mem (γ := Submodule K M) (ball K xy) u) (v : M) (hv : v ∈ seed.stratum xy)
  (huv : u + v = 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
Tactic: obtain ⟨u, hu, v, hv, huv⟩ := hxy
Cleared hypotheses: hxy
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : Membership.mem (γ := Submodule K M) (ball K xy) u
v : M
hv : v ∈ seed.stratum xy
huv : u + v = 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 huv' : x - (↑y : M) - v = u
Tactic: have huv' : x - y.val - v = u := by simp [← huv]
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : Membership.mem (γ := Submodule K M) (ball K xy) u
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
⊢ 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 : ∀ (hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h) (v : M) (hv : v ∈ seed.stratum xy)
  (huv : u + v = x - (↑y : M)) (huv' : x - (↑y : M) - v = u),
  f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
Tactic: rw [mem_ball_iff K] at hu
Cleared hypotheses: hu, v, hv, huv, huv'
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
have hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
Tactic: have hyv : y.val + v ∈ f.val.domain := Submodule.add_mem _ (by simp) (f.mem_domain hv)
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
⊢ False
have h₁ : LE.le (α := ArchimedeanClass M)
  (ArchimedeanClass.mk
    (x -
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
            hyv) :
        M)))
  (ArchimedeanClass.mk (x - (↑y : M)))
Tactic: obtain h := f.archimedeanClassMk_le_of_eval_eq h ⟨y.val + v, hyv⟩
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h :
  LE.le (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))
    (ArchimedeanClass.mk (x - (↑y : M)))
⊢ False
have contrapose! : ∀ (h : True),
  LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M)))
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h : True
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M)))
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))
have simp_rw : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
Tactic: simp_rw [← sub_sub, huv']
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h : True
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
have inl : ∀ (hu : ∀ (h : Ne.{u_2 + 1} (α := M) 0 0), xy < FiniteArchimedeanClass.mk 0 h) (huv : 0 + v = x - (↑y : M))
  (huv' : x - (↑y : M) - v = 0),
  LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk 0)
Tactic: obtain rfl | ne := eq_or_ne u 0
Cleared hypotheses: u, hu, huv, huv'
-- 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
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h : True
inl :
  ∀ (hu : ∀ (h : Ne.{u_2 + 1} (α := M) 0 0), xy < FiniteArchimedeanClass.mk 0 h) (huv : 0 + v = x - (↑y : M))
    (huv' : x - (↑y : M) - v = 0),
    LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk 0)
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
have inr : ∀ (ne : u ≠ 0), LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
Tactic: obtain rfl | ne := eq_or_ne u 0
-- 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
c : FiniteArchimedeanClass M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : ArchimedeanClass.mk ((↑y : M) - x) = (↑c : ArchimedeanClass M)
h : ∀ (z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain), (↑z : M) - x ∉ ball K c
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R } =
    (truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦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))
have coeff : ∀ (d : FiniteArchimedeanClass M),
  { coeff := f.evalCoeff x, isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }.coeff d =
    coeff
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦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)))
      d
Tactic: ext d