-- 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
c_1 : Set (Partial seed)
hnonempty : c_1.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c_1
x : ↥(sSupFun (c := c_1) hc).domain
c : FiniteArchimedeanClass M
hx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1)))
    (↑x : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1) f
hf : (↑x : M) ∈ f.domain
f' : Partial seed
hmem' : f' ∈ c_1
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
h :
  Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) f.toFun.range
    ((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 : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑x : M) hf)))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (sSupFun (c := c_1) hc).toFun.range
    ((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⟧)
            ((↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
have simp_rw : ∀
  (h :
    ∃ (y : ↥f.domain),
      (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) y =
        (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 : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑x : M) hf))))),
  ∃ (y : ↥(sSupFun (c := c_1) hc).domain),
    (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y =
      (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⟧)
            ((↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
Tactic: simp_rw [LinearMap.mem_range, LinearPMap.toFun_eq_coe] at ⊢ h
Cleared hypotheses: h