-- 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
refine_2 :
  ∀ (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)
      (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)
    ((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)
    (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)
have refine_2₁ : ∀ (hdc : c ≤ d),
  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)
    (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: obtain hdc | hdc := lt_or_ge d c