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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
hf :
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)
⊢ Eq (α := M) ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M) x : M)
    ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M)
        ((DirectSum.coeAddMonoidHom seed.stratum' :
              (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
            f' :
          ↥seed.baseDomain) :
      M)
have a : Eq (α := M) ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M) x : M)
  ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M)
      (f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c))
        fun (i : FiniteArchimedeanClass M) (b : ↥(seed.stratum i)) ↦
        (↑(Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' i)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑b : M) sorry) sorry) :
          ↥seed.baseDomain)) :
    M)
Tactic: rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]
-- 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.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
hf :
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)
⊢ (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((((decompose seed.stratum' : (a : ↥seed.baseDomain) → ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) x :
            ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) :
          (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a))
        c) =
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c
have hx : x =
  (Equiv.symm (decompose seed.stratum') : (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
    f'
Tactic: have hx : x = (decompose seed.stratum').symm f' := by
    change x = f'.coeAddMonoidHom _
    apply Submodule.subtype_injective
    rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]
    simp [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 : M
c : FiniteArchimedeanClass M
h : x ∈ seed.stratum c
⊢ x ∈ seed.baseEmbedding.domain
have apply : (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseEmbedding.domain : Set M)
Tactic: apply Set.mem_of_mem_of_subset h
-- 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
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
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
hx : 0 < x
hmem : (↑x : M) ∈ seed.baseDomain
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
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)),
  0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
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
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)
⊢ 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))
have rw : 0 < (↑x : M)
Tactic: rw [hf]
-- 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)
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
have 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))
Tactic: have hfpos : 0 < (f.sum fun _ x ↦ x.val) := by
    rw [hf]
    simpa using hx
-- 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))
⊢ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).Nonempty
have hne : Ne (α := M)
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M))
  0
Tactic: obtain hne := hfpos.ne.symm
-- 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))
hne :
  Ne (α := M)
    (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M))
    0
⊢ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).Nonempty
have contrapose! : ∀ (hempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) = ∅),
  Eq (α := M)
    (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M))
    0
Tactic: contrapose! hne with hempty
Cleared hypotheses: hne
-- 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))
hempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) = ∅
⊢ Eq (α := M)
    (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (x_1 : ↥(seed.stratum x)) ↦ (↑x_1 : M))
    0
have hyp : ∀ (i : FiniteArchimedeanClass M), (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) i) : M) = 0
Tactic: apply DFinsupp.sum_eq_zero
-- 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))
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
have hsupport : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).Nonempty
Tactic: have hsupport : f.support.Nonempty := by
    obtain hne := hfpos.ne.symm
    contrapose! hne with hempty
    apply DFinsupp.sum_eq_zero
    intro c
    simpa using DFinsupp.notMem_support_iff.mp (Finset.eq_empty_iff_forall_notMem.mp hempty c)
-- 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
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
have refine_1 : ∀ j < f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport,
  Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j)
    (HahnSeries.coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))
      j)
Tactic: refine (HahnSeries.lt_iff _ _).mpr ⟨f.support.min' 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
refine_1 :
  ∀ j < f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport,
    Eq.{u_3 + 1} (α := R)
      (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j)
      (HahnSeries.coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))
        j)
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x
have refine_2 : LT.lt.{u_3} (α := R)
  (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0)
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport))
  (HahnSeries.coeff
    ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
      ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport))
Tactic: refine (HahnSeries.lt_iff _ _).mpr ⟨f.support.min' 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
j : FiniteArchimedeanClass M
hj : j < f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j)
    (HahnSeries.coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))
      j)
have refine_1 : Eq.{u_3 + 1} (α := R)
  (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j : R)
  ((seed.coeff j : (a : ↥(seed.stratum j)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) j) : R)
Tactic: rw [seed.coeff_baseEmbedding hf.symm]
-- 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
j : FiniteArchimedeanClass M
hj : j < f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j : R)
    ((seed.coeff j : (a : ↥(seed.stratum j)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) j) : R)
have refine_1 : Eq.{u_3 + 1} (α := R)
  (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j : R)
  ((seed.coeff j : (a : ↥(seed.stratum j)) → R) 0 : R)
Tactic: rw [DFinsupp.notMem_support_iff.mp ?_]
-- 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
j : FiniteArchimedeanClass M
hj : j < f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).min' hsupport
refine_1 :
  Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j : R)
    ((seed.coeff j : (a : ↥(seed.stratum j)) → R) 0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) 0) j : R)
    ((seed.coeff j : (a : ↥(seed.stratum j)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) j) : R)
have rw : j ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
Tactic: rw [DFinsupp.notMem_support_iff.mp ?_]