awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 <
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
      (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
have a : 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x)
Tactic: rw [← LinearPMap.map_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ 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))
have hmem : (↑x : M) ∈ seed.baseEmbedding.domain
Tactic: have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
-- 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
⊢ 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))
have 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))
Tactic: obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem
-- 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
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))
have refine_1 : (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M)) ∈
  seed.baseEmbedding.domain
Tactic: refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
-- 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
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
⊢ 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))
have 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))
        sorry) :
    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))
Tactic: refine ⟨⟨f'.sum fun d x ↦ x.val, ?_⟩, ?_⟩
-- 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
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)
⊢ (f'.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (d : FiniteArchimedeanClass M) (x : ↥(seed.stratum d)) ↦ (↑x : M)) ∈
    seed.baseEmbedding.domain
have 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))
Tactic: rw [seed.domain_baseEmbedding, ArchimedeanStrata.baseDomain,
      Submodule.mem_iSup_iff_exists_dfinsupp']
-- 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
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)
⊢ ∃ (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))
have 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))
Tactic: use f'
-- 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
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)
⊢ 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)
have 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))
            sorry)))
      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: ext d
-- 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
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
⊢ 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)
have 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)
Tactic: rw [seed.coeff_baseEmbedding rfl]
-- 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
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
hdc : d < c
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
        ((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) :
            (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          d) :
      R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : R)
have refine_2 : (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) :
      (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
    d =
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d
Tactic: apply congrArg
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
hdc : d < c
⊢ (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) :
        (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
      d =
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d
have hcd : ¬(↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)
Tactic: have hcd : ¬ c.val ≤ d.val := not_le_of_gt hdc