-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
fdomain : Submodule K M
f : ↥fdomain →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := fdomain, toFun := f }
hdomain :
  (↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
            HahnEmbedding.IsPartial h.some f)
            { domain := fdomain, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
            hpartial) :
        M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain =
    ⊤
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := fdomain, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Eq (α := ArchimedeanClass M)
      ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
          (orderTop.{u_2, u_3} (R := R)
            ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := fdomain, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := fdomain, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop.{u_2, u_3} (R := R)
              ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
have obtain : ∀ (f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
  (hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f })
  (harch :
    ∀
      (x :
        ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                  HahnEmbedding.IsPartial h.some f)
                  { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                  hpartial) :
              M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
      Eq (α := ArchimedeanClass M)
        ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop.{u_2, u_3} (R := R)
              ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
                ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                            HahnEmbedding.IsPartial h.some f)
                            { domain := ⊤, toFun := f :
                              M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                            hpartial) :
                        M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                    ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                      Lex R⟦FiniteArchimedeanClass M⟧)
                  x))) :
          ArchimedeanClass M)
        (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)),
  ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop.{u_2, u_3} (R := R)
              ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
Tactic: obtain rfl := hdomain
Cleared hypotheses: fdomain, f, hpartial, hdomain, harch