-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨z, hz⟩ := LinearMap.mem_range.mp (f.prop.truncLT_mem_range y c)