-- 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
a' : M
ha'mem : a' ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
ha' :
  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⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a' ha'mem) :
      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⟧)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
refine_1 :
  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) a' ⋯) :
      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⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a' ha'mem) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ 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) a' ⋯) :
      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⟧)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) a ha)))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
rw [← ha']