∀ {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 : HahnEmbedding.Seed K M R}
  {c : Set (HahnEmbedding.Partial seed)} (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c),
  HahnEmbedding.Partial.sSupFun hc = LinearPMap.sSup ((fun x => ↑x) '' c) ⋯