-- 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 : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hz :
  Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).toFun :
          (a : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) → Lex R⟦FiniteArchimedeanClass M⟧)
        z :
      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 : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              y))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
pos :
  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⟧)
        (Subtype.mk (p := fun (x_1 : M) ↦
          x_1 ∈ ((↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).supSpanSingleton x (f.eval x) hx).domain) (↑z : M) ⋯) :
      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))
⊢ ∃ (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:
refine ⟨⟨z.val, by simpa using Submodule.mem_sup_left z.prop⟩, ?_⟩