awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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)
have hi₁ : i < FiniteArchimedeanClass.mk ((↑z : M) - (↑y : M)) hzyne
Tactic: rw [hzyclass] at hi
Cleared hypotheses: hi
-- 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
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
⊢ 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)
have hzy : Membership.mem (γ := Submodule K M) (ball K i) ((↑z : M) - (↑y : M))
Tactic: have hzy : z.val - y.val ∈ ball K i := fun _ ↦ hi
-- 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
c : K
hc : c ≠ 0
⊢ -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have contrapose : ∀ (hx : -c • x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
  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
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
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have rwa : ∀ (hx : -(c • 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
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
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
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have rwa₁ : ∀ (hx : c • 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
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
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
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have rwa₂ : ∀ (hx : 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
Cleared hypotheses: 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
⊢ StrictMono (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
have hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
Tactic: have hx' {c : K} (hc : c ≠ 0) : -c • x ∉ f.val.domain := by
    contrapose hx
    rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : y < z
⊢ (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) y <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) z
have hyz₁ : 0 < z - y
Tactic: rw [← sub_pos] at hyz
Cleared hypotheses: hyz
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
⊢ (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) y <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) z
have a : 0 <
  (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) z -
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) y
Tactic: apply lt_of_sub_pos
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
⊢ 0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) z -
      (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) y
have a : 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
Tactic: rw [← LinearPMap.map_sub]
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
have hyzmem : (↑(z - y) : M) ∈ (f.extendFun hx).domain
Tactic: obtain hyzmem := (z - y).prop
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : (↑(z - y) : M) ∈ (f.extendFun hx).domain
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
have hyzmem₁ : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
Tactic: nth_rw 1 [extendFun, LinearPMap.domain_supSpanSingleton] at hyzmem
Cleared hypotheses: hyzmem
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
have a : ∀ (a : M) (ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (b : M)
  (hb : Membership.mem (γ := Submodule K M) (K ∙ x) b) (hab : a + b = (↑(z - y) : M)),
  0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
Tactic: obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hyzmem
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
b : M
hb : Membership.mem (γ := Submodule K M) (K ∙ x) b
hab : a + b = (↑(z - y) : M)
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
have this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) sorry
Tactic: have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
b : M
hb : Membership.mem (γ := Submodule K M) (K ∙ x) b
hab : a + b = (↑(z - y) : M)
this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)
have a₁ : ∀
  (hyz :
    LT.lt (α := ↥(f.extendFun hx).domain) 0 (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) sorry))
  (this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) sorry),
  0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) sorry)
Tactic: rw [this] at ⊢ hyz
Cleared hypotheses: hyz, this
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
b : M
hb : Membership.mem (γ := Submodule K M) (K ∙ x) b
hab : a + b = (↑(z - y) : M)
hyz :
  LT.lt (α := ↥(f.extendFun hx).domain) 0 (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯
⊢ 0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
have habpos : 0 < a + b
Tactic: have habpos : 0 < a + b := by exact hyz
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
b : M
hb : Membership.mem (γ := Submodule K M) (K ∙ x) b
hab : a + b = (↑(z - y) : M)
hyz :
  LT.lt (α := ↥(f.extendFun hx).domain) 0 (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯
habpos : 0 < a + b
⊢ 0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
have a₁ : ∀ (c : K) (hc : c • x = b),
  0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) sorry)
Tactic: obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb
-- 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
hx' : ∀ {c : K} (hc : c ≠ 0), -c • x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y z : ↥(f.extendFun hx).domain
hyzmem : (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
b : M
hb : Membership.mem (γ := Submodule K M) (K ∙ x) b
hab : a + b = (↑(z - y) : M)
hyz :
  LT.lt (α := ↥(f.extendFun hx).domain) 0 (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
this : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯
habpos : 0 < a + b
c : K
hc : c • x = b
⊢ 0 <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯)
have habpos₁ : 0 < a + c • x
Tactic: rw [← hc] at habpos
Cleared hypotheses: habpos, hc