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 : FiniteArchimedeanClass M
y' : M
hy'_1 : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑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 = y'
k : K
hk : k • x = b
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    ((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) 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))

Tactic:
apply truncLT_eval_mem_range_extendFun

Premises used: HahnEmbedding.Partial.truncLT_eval_mem_range_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
a : f ≤ f.extend hx
a₁ : f ≠ f.extend hx
⊢ f < f.extend hx

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- 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
a : (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)
⊢ f ≤ f.extend hx

Tactic:
change f.val ≤ (f.extend hx).val

Premises used: HahnEmbedding.Partial.extend, Subtype.val
-- 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
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
simpa [extend, extendFun] using LinearPMap.left_le_sup _ _ _

Premises used: LinearPMap.left_le_sup, HahnEmbedding.Partial.extendFun, HahnEmbedding.Partial.extend
-- 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
a : ∀ (this : f = f.extend hx), False
⊢ f ≠ f.extend hx

Tactic:
by_contra!
-- 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
this : f = f.extend hx
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
congr
-- 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
this : f = f.extend hx
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
have : f.val.domain = (f.extend hx).val.domain := by congr
-- 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
this_1 : f = f.extend hx
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ x ∉ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
rw [this] 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
this_1 : f = f.extend hx
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx₁ : x ∉ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ f = f.extend hx

Tactic:
rw [this] 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
this_1 : f = f.extend hx
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx₁ : x ∉ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this₁ : f = f.extend hx
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
rw [this] 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_1 : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : x ∉ (↑(f.extend hx_1) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this_1 : f = f.extend hx_1
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx_1) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
a : ∀ (h : True), x ∈ (↑(f.extend hx_1) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ False

Tactic:
contrapose! hx with h
-- 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
this_1 : f = f.extend hx
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : True
⊢ Membership.mem (γ := Submodule K M)
    (LinearPMap.domain (S := K) (σ := RingHom.id K) (LinearPMap.mkSpanSingleton x (f.eval x) ⋯)) x

Tactic:
simp
-- 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
this_1 : f = f.extend hx
this :
  (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h : True
⊢ x ∈ (↑(f.extend hx) : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
simpa using Submodule.mem_sup_right (by simp)

Premises used: Submodule.mem_sup_right
-- 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
c : Set (Partial seed)
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
⊢ ∀ ⦃x y : Partial seed⦄,
    x ≤ y → (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ (↑y : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
simp
-- 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
a :
  0 <
    (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
      (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x
⊢ (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x <
    (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y

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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
a : 0 < (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)
⊢ 0 <
    (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
      (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x

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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
⊢ (↑(y - x) : M) ∈ (sSupFun (c := c) hc).domain

Tactic:
obtain hyx := (y - x).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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
⊢ ∀ ⦃x y : Partial seed⦄,
    x ≤ y → (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ (↑y : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
simp
-- 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
a :
  ∀ (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (hmem :
      Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c) f)
    (hf : (↑(y - x) : M) ∈ f.domain),
    0 < (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)
⊢ 0 < (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)

Tactic:
obtain ⟨f, hmem, hf⟩ :=
    (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hyx

Premises used: LinearPMap.mem_domain_sSup_iff, DirectedOn.mono_comp, Set.Nonempty.image, 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c) f
hf : (↑(y - x) : M) ∈ f.domain
⊢ (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)

Tactic:
have : (sSupFun hc) (y - x) = f ⟨(y - x).val, hf⟩ :=
    LinearPMap.sSup_apply _ hmem ⟨(y - x).val, hf⟩
-- 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
a :
  0 <
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
⊢ 0 < (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)

Tactic:
rw [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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
a :
  ∀ f' ∈ c,
    ∀ (hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f),
      0 <
        (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
⊢ 0 <
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)

Tactic:
obtain ⟨f', _, hf'⟩ := (Set.mem_image _ _ _).mp hmem

Premises used: Set.mem_image, 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c)))
    (↑(y - x) : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
⊢ StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
have hmono : StrictMono f := hf'.symm ▸ f'.prop.strictMono