-- 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))
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))
⊢ (↑(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 neg : ∀
  (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: by_cases! hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty