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
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) ⋯
c : K
habpos : 0 < a + c • x
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 a₁ : 0 <
  (↑((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx) :
      ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain →
        Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x_1 : M) ↦
      x_1 ∈ ((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) (a + c • x) sorry)
Tactic: simp_rw [← hc, extendFun]
-- 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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 <
    (↑((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx) :
        ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain →
          Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x_1 : M) ↦
        x_1 ∈ ((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) (a + c • x) ⋯)
have a₁ : 0 <
  (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha) +
    HSMul.hSMul (α := K) ((RingHom.id K : (a : K) → K) c : K) (f.eval x)
Tactic: rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha]
-- 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_1 : z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
this :
  f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
⊢ 0 <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha) +
      HSMul.hSMul (α := K) ((RingHom.id K : (a : K) → K) c : K) (f.eval x)
have this₁ : -(c • f.eval x) <
  (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
      ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: rw [eval_smul, neg_smul] 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
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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha) +
      HSMul.hSMul (α := K) ((RingHom.id K : (a : K) → K) c : K) (f.eval x)
have a₁ : f.eval (-c • x) <
  (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
      ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: suffices f.eval (-c • x) < f.val ⟨a, ha⟩ by
    rw [eval_smul, neg_smul] at this
    exact neg_lt_iff_pos_add.mp 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
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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ -c • x < a
have rw : -(c • x) < a
Tactic: rw [neg_smul]
-- 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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
have hac : -c • x < a
Tactic: have hac : -c • x < a := by
    rw [neg_smul]
    exact neg_lt_iff_pos_add.mpr habpos
-- 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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
hac : -c • x < a
⊢ f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
have pos : ∀ (hc : c = 0),
  f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: by_cases hc : c = 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
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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
hac : -c • x < a
pos :
  ∀ (hc : c = 0),
    f.eval (-c • x) <
      (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
⊢ f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
have neg : ∀ (hc : ¬c = 0),
  f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: by_cases hc : c = 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
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) ⋯
c : K
habpos : 0 < a + c • x
hc_1 : c • x = b
hac : -c • x < a
hc : c = 0
⊢ f.eval (-c • x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
have pos : ∀ (hac : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x < a) (hc : c = 0),
  f.eval (HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: rw [hc] at ⊢ hac
Cleared hypotheses: hac, hc
-- 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) ⋯
c : K
habpos : 0 < a + c • x
hc_1 : c • x = b
hac : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x < a
hc : c = 0
⊢ f.eval (HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x) <
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
have pos : (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
      ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
    0 <
  (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
      ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)
Tactic: suffices f.val 0 < f.val ⟨a, ha⟩ by simpa 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
c : FiniteArchimedeanClass M
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (f.extendFun hx).toFun.range
    ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
have rw : ∃ (y : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain),
  Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    ((((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).toFun :
          (a : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) →
            Lex R⟦FiniteArchimedeanClass M⟧)
        y :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
Tactic: rw [extendFun, LinearMap.mem_range]
-- 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 : FiniteArchimedeanClass M
⊢ ∃ (y : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain),
    Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
      ((((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).toFun :
            (a : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) →
              Lex R⟦FiniteArchimedeanClass M⟧)
          y :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
      ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
          ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))) :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
have pos : ∀
  (h :
    ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
      Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)),
  ∃ (y : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain),
    Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
      ((((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).toFun :
            (a : ↥((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) →
              Lex R⟦FiniteArchimedeanClass M⟧)
          y :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
      ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
          ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x))) :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
Tactic: by_cases h : ∃ y : f.val.domain, y.val - x ∈ ball K c