awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
hfpos :
  LT.lt (α := M) 0
    (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M))
hsupport : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).Nonempty
hferase :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M)) -
      (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
            (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)) :
        M) =
    ∑
      x ∈
        f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
          (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport),
      (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) x) : M)
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (x : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) x) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) : Set (FiniteArchimedeanClass M))
hsupport' :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
      (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) =
    ∅
⊢ (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) : ArchimedeanClass M) <
    ArchimedeanClass.mk
      (∑
        x ∈
          f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
            (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport),
        (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) x) : M))

Tactic:
simpa [hsupport'] using (f.support.min' hsupport).2.lt_top

Premises used: Finset.min', DFinsupp.support, Ne.lt_top, Subtype.property
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
a :
  0 <
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
      (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
⊢ (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x <
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y

Tactic:
apply lt_of_sub_pos

Premises used: lt_of_sub_pos
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
a : 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)
⊢ 0 <
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
      (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x

Tactic:
rw [← LinearPMap.map_sub]

Premises used: LinearPMap.map_sub
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < y - x

Tactic:
simpa using h
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)

Tactic:
exact baseEmbedding_pos _ <| by simpa using h

Premises used: HahnEmbedding.Seed.baseEmbedding_pos
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
⊢ (↑x : M) ∈ seed.baseEmbedding.domain

Tactic:
have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
obtain :
  ∀ (f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i))
    (hf :
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
          fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
        (↑x : M)),
    Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) seed.baseEmbedding.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⟧)
              ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) seed.baseEmbedding.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⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem

Premises used: Iff.mp, Submodule.mem_iSup_iff_exists_dfinsupp'
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) seed.baseEmbedding.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⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩

Premises used: Set.Mem, setOf, DFinsupp.sum, Subtype.mk, Exists.intro, Set.range, Subtype.val
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
refine_1 :
  (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M)) ∈
    seed.baseEmbedding.domain
refine_2 :
  Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    ((seed.baseEmbedding.toFun : (a : ↥seed.baseEmbedding.domain) → Lex R⟦FiniteArchimedeanClass M⟧)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain)
          (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
            fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
          ⋯) :
      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⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) seed.baseEmbedding.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⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
refine_1 :
  ∃ (f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)),
    Eq (α := M)
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M))
      (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
⊢ (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M)) ∈
    seed.baseEmbedding.domain

Tactic:
rw [seed.domain_baseEmbedding, ArchimedeanStrata.baseDomain,
      Submodule.mem_iSup_iff_exists_dfinsupp']

Premises used: Submodule.mem_iSup_iff_exists_dfinsupp', HahnEmbedding.ArchimedeanStrata.baseDomain, HahnEmbedding.Seed.domain_baseEmbedding
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
w : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
h :
  Eq (α := M)
    (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M))
    (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
⊢ ∃ (f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)),
    Eq (α := M)
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M))
      (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))

Tactic:
use f'
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
refine_2 :
  ∀ (d : FiniteArchimedeanClass M),
    Eq.{u_3 + 1} (α := R)
      (HahnSeries.coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain)
              (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
                fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
              ⋯)))
        d)
      (HahnSeries.coeff
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
        d)
⊢ Eq (α := HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
    ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain)
            (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
              fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
            ⋯)) :
      HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
    ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)) :
      HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)

Tactic:
ext d
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
d : FiniteArchimedeanClass M
refine_2 :
  Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : R)
    (HahnSeries.coeff
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
        d :
      R)
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain)
            (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
              fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M))
            ⋯)))
      d)
    (HahnSeries.coeff
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
      d)

Tactic:
rw [seed.coeff_baseEmbedding rfl]

Premises used: HahnEmbedding.Seed.coeff_baseEmbedding