-- 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)
pos :
  ∀ (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))),
    ∃ (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))
⊢ ∃ (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:
obtain ⟨z, hz⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range y c)

Premises used: HahnEmbedding.IsPartial.truncLT_mem_range, LinearMap.mem_range, Subtype.prop, Iff.mp