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
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)
c : FiniteArchimedeanClass M
hc : c ∈ (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) : Set (FiniteArchimedeanClass M))
d : FiniteArchimedeanClass M
hd : d ∈ (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) : Set (FiniteArchimedeanClass M))
h : c < d
⊢ (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : M)
have rw : (↑c : ArchimedeanClass M) < (↑d : ArchimedeanClass M)
Tactic: rw [seed.archimedeanClassMk_of_mem_stratum (f d).prop (by simpa using hd)]
-- 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
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)
⊢ LT.lt (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : 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)))
have 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))
Tactic: have hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk (f x).val) f.support := by
    intro c hc d hd h
    simp only
    rw [seed.archimedeanClassMk_of_mem_stratum (f c).prop (by simpa using hc)]
    rw [seed.archimedeanClassMk_of_mem_stratum (f d).prop (by simpa using hd)]
    exact h
-- 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
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))
⊢ LT.lt (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
        fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : 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)))
have refine_2 : LT.lt (α := ArchimedeanClass M)
  (ArchimedeanClass.mk
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)) :
      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: rw [DFinsupp.sum, ArchimedeanClass.mk_sum hsupport hmono]
-- 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
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))
⊢ LT.lt (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
            (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)) :
        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)))
have refine_2 : (↑(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: rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop
    (by simpa using f.support.min'_mem hsupport)]
-- 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
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))
⊢ (↑(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))
have pos : ∀
  (hsupport' :
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
        (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).Nonempty),
  (↑(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: by_cases! hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
-- 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
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)).Nonempty
⊢ (↑(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))
have pos : (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) : ArchimedeanClass M) <
  ArchimedeanClass.mk
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          ((f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
                (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).min'
            hsupport')) :
      M)
Tactic: rw [ArchimedeanClass.mk_sum hsupport' (hmono.mono (by simp))]
-- 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
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)).Nonempty
⊢ (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) : ArchimedeanClass M) <
    ArchimedeanClass.mk
      (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
            ((f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
                  (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).min'
              hsupport')) :
        M)
have pos : (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) : ArchimedeanClass M) <
  (↑((f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
            (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).min'
        hsupport') :
    ArchimedeanClass M)
Tactic: rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop (by
      simpa using (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2)]
-- 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
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)).Nonempty
⊢ (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport) : ArchimedeanClass M) <
    (↑((f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
              (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).min'
          hsupport') :
      ArchimedeanClass M)
have pos : (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
        (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)).min'
    hsupport' ∈
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).erase
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport)
Tactic: apply Finset.min'_lt_of_mem_erase_min' (α := FiniteArchimedeanClass M)
-- 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
⊢ (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x <
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y
have a : 0 <
  (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) y -
    (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
Tactic: apply lt_of_sub_pos