awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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)
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) ⋯) ⋯) :
            ↥seed.baseDomain)) :
      M)
⊢ 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)

Tactic:
rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]

Premises used: DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index
-- 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.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)
        (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) ⋯) ⋯) :
            ↥seed.baseDomain)) :
      M)

Tactic:
simp [h]
-- 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.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)
⊢ 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]
-- 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.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)
hx :
  x =
    (Equiv.symm (decompose seed.stratum') :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'
⊢ (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

Tactic:
simp [hf, hx]
-- 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
⊢ seed.baseEmbedding.domain = seed.baseDomain

Tactic:
rfl

Premises used: iSup, HahnEmbedding.ArchimedeanStrata.baseDomain, rfl
-- 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
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
⊢ Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x))
        c :
      R)
    ((seed.coeff c : (a : ↥(seed.stratum c)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c) : R)

Tactic:
simpa [baseEmbedding] using seed.hahnCoeff_apply h c

Premises used: HahnEmbedding.Seed.hahnCoeff_apply, HahnEmbedding.Seed.baseEmbedding
-- 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 : M
c : FiniteArchimedeanClass M
h : x ∈ seed.stratum c
apply : (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseEmbedding.domain : Set M)
⊢ x ∈ seed.baseEmbedding.domain

Tactic:
apply Set.mem_of_mem_of_subset h

Premises used: Set.mem_of_mem_of_subset
-- 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 : M
c : FiniteArchimedeanClass M
h : x ∈ seed.stratum c
⊢ (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseDomain : Set M)

Tactic:
simpa using le_iSup_iff.mpr fun _ h ↦ h c

Premises used: Iff.mpr, le_iSup_iff
-- 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
⊢ (↑x : M) ∈ seed.baseEmbedding.domain

Tactic:
have hmem : x.val ∈ seed.baseEmbedding.domain := x.prop
-- 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
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
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x

Tactic:
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ _).mp hmem

Premises used: Iff.mp, Submodule.mem_iSup_iff_exists_dfinsupp'
-- 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)
rw : 0 < (↑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))

Tactic:
rw [hf]
-- 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)
⊢ 0 < (↑x : M)

Tactic:
simpa using hx
-- 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)
⊢ 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
-- 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))
⊢ 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

Premises used: Ne.symm, LT.lt.ne
-- 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))
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
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
⊢ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)).Nonempty

Tactic:
contrapose! hne with hempty
-- 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))
hempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) = ∅
hyp : ∀ (i : FiniteArchimedeanClass M), (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) i) : M) = 0
⊢ 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:
apply DFinsupp.sum_eq_zero

Premises used: DFinsupp.sum_eq_zero
-- 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))
hempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) = ∅
c : FiniteArchimedeanClass M
⊢ (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c) : M) = 0

Tactic:
simpa using DFinsupp.notMem_support_iff.mp (Finset.eq_empty_iff_forall_notMem.mp hempty c)

Premises used: DFinsupp.notMem_support_iff, Finset.eq_empty_iff_forall_notMem, Iff.mp
-- 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))
⊢ 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)
-- 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
⊢ 0 < (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x

Tactic:
(HahnSeries.lt_iff _ _).mpr ⟨f.support.min' hsupport, ?_, ?_⟩

Premises used: Finset.min', Iff.mpr, DFinsupp.support, And.intro, Exists.intro, HahnSeries.lt_iff