-- 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)).Nonempty
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)
⊢ (↑(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 [seed.archimedeanClassMk_of_mem_stratum (f _).prop (by
      simpa using (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2)]

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, HahnEmbedding.Seed.toArchimedeanStrata, Subtype.prop, DFunLike.coe