awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ∀ {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
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
⊢ 0 < z - y

Tactic:
rw [← sub_pos] at hyz

Premises used: sub_pos
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
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
⊢ (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) y <
    (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) z

Tactic:
apply lt_of_sub_pos

Premises used: lt_of_sub_pos
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
a : 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (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

Tactic:
rw [← LinearPMap.map_sub]

Premises used: LinearPMap.map_sub
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
⊢ (↑(z - y) : M) ∈ (f.extendFun hx).domain

Tactic:
obtain hyzmem := (z - y).prop

Premises used: HSub.hSub, Subtype.prop
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
⊢ (↑(z - y) : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain ⊔ K ∙ x

Tactic:
nth_rw 1 [extendFun, LinearPMap.domain_supSpanSingleton] at hyzmem

Premises used: LinearPMap.domain_supSpanSingleton, HahnEmbedding.Partial.extendFun
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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 :
  ∀ (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)
⊢ 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

Premises used: Iff.mp, Submodule.mem_sup
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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)
⊢ z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯

Tactic:
simp_rw [hab]
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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)
⊢ z - y = Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ (f.extendFun hx).domain) (a + b) ⋯

Tactic:
have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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) ⋯
a₁ :
  ∀
    (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) ⋯)
⊢ 0 < (↑(f.extendFun hx) : ↥(f.extendFun hx).domain → Lex R⟦FiniteArchimedeanClass M⟧) (z - y)

Tactic:
rw [this] at ⊢ hyz
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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 < a + b

Tactic:
hyz
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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 < a + b

Tactic:
have habpos : 0 < a + b := by exact hyz
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
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) ⋯)
⊢ 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) ⋯)

Tactic:
obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb

Premises used: Submodule.mem_span_singleton, Iff.mp
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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 < a + c • x

Tactic:
rw [← hc] at habpos
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
habpos₁ : 0 < a + c • x
⊢ c • x = b

Tactic:
rw [← hc] at habpos
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
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) ⋯)
⊢ 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) ⋯)

Tactic:
simp_rw [← hc, extendFun]

Premises used: HahnEmbedding.Partial.extendFun
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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
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)
⊢ 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) ⋯)

Tactic:
rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha]

Premises used: LinearPMap.supSpanSingleton_apply_mk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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)
⊢ -(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

Premises used: neg_smul, HahnEmbedding.Partial.eval_smul