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
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 :
  -(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)
⊢ 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:
neg_lt_iff_pos_add.mp this

Premises used: neg_lt_iff_pos_add, 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_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 :
  -(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)
⊢ 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:
exact neg_lt_iff_pos_add.mp this

Premises used: neg_lt_iff_pos_add, 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) ⋯
c : K
habpos : 0 < a + c • x
hc : c • x = b
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)
⊢ 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:
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
-- 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
rw : -(c • x) < a
⊢ -c • x < a

Tactic:
rw [neg_smul]

Premises used: neg_smul
-- 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
⊢ -(c • x) < a

Tactic:
neg_lt_iff_pos_add.mpr habpos

Premises used: Iff.mpr, neg_lt_iff_pos_add
-- 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
⊢ -(c • x) < a

Tactic:
exact neg_lt_iff_pos_add.mpr habpos

Premises used: Iff.mpr, neg_lt_iff_pos_add
-- 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
⊢ -c • x < a

Tactic:
have hac : -c • x < a := by
    rw [neg_smul]
    exact neg_lt_iff_pos_add.mpr 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
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)
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)
⊢ 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
-- 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_1 : c • x = b
hac : -c • x < a
hc : c = 0
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)
⊢ 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:
rw [hc] at ⊢ hac
-- 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_1 : c • x = b
hac : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x < a
hc : c = 0
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)
⊢ 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:
suffices f.val 0 < f.val ⟨a, ha⟩ by simpa using this
-- 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_1 : c • x = b
hac : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x < a
hc : c = 0
⊢ 0 < Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha

Tactic:
simpa using hac
-- 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_1 : c • x = b
hac : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (-0) x < a
hc : c = 0
⊢ (↑(↑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:
exact f.prop.strictMono (by simpa using hac)

Premises used: HahnEmbedding.IsPartial.strictMono, 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
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)

Tactic:
f.eval_lt (hx' hc) ⟨a, ha⟩ hac

Premises used: Subtype.mk, HahnEmbedding.Partial.eval_lt
-- 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_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)

Tactic:
exact f.eval_lt (hx' hc) ⟨a, ha⟩ hac

Premises used: Subtype.mk, HahnEmbedding.Partial.eval_lt
-- 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
⊢ seed.baseEmbedding ≤ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx

Tactic:
le_trans f.prop.baseEmbedding_le <| LinearPMap.left_le_sup _ _ _

Premises used: HahnEmbedding.IsPartial.baseEmbedding_le, LinearPMap.left_le_sup, Subtype.prop, le_trans