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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
ne : x ≠ 0
⊢ Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) ⊤

Tactic:
simpa using 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
ne : x ≠ 0
⊢ (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)

Tactic:
simpa using hx (by simpa using 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : (↑x : M) ≠ 0
⊢ Ne.{u_3 + 1} (α := R)
    (coeff (Γ := FiniteArchimedeanClass M)
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          x))
      (FiniteArchimedeanClass.mk (↑x : M) hx0))
    0

Tactic:
HahnSeries.coeff_orderTop_ne <| f.orderTop_eq_finiteArchimedeanClassMk hx0

Premises used: HahnSeries.coeff_orderTop_ne, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
h :
  HSub.hSub (α := R)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))
        d)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            z))
        d) =
    0
⊢ Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
      d)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      d)

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
h :
  Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (y - z)))
      d)
    0
⊢ HSub.hSub (α := R)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            y))
        d)
      (coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            z))
        d) =
    0

Tactic:
rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub]

Premises used: ofLex_sub, HahnSeries.coeff_sub, LinearPMap.map_sub
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
⊢ Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (y - z)))
      d)
    0

Tactic:
coeff_eq_zero_of_mem f ?_ hd

Premises used: Lex, HahnEmbedding.Partial.coeff_eq_zero_of_mem
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
h : Membership.mem (γ := Submodule K M) (ball K c) (↑(y - z) : M)
⊢ Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (y - z)))
      d)
    0

Tactic:
refine coeff_eq_zero_of_mem f ?_ hd

Premises used: HahnEmbedding.Partial.coeff_eq_zero_of_mem
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
push_cast : (↑y : M) - (↑z : M) = (↑y : M) - x - ((↑z : M) - x)
⊢ (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)

Tactic:
push_cast
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
⊢ (↑y : M) - (↑z : M) = (↑y : M) - x - ((↑z : M) - x)

Tactic:
simp
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
⊢ (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)

Tactic:
have : (y - z).val = (y.val - x) - (z.val - x) := by
    push_cast
    simp
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
this : (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)
h : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x - ((↑z : M) - x))
⊢ Membership.mem (γ := Submodule K M) (ball K c) (↑(y - z) : M)

Tactic:
rw [this]
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
this : (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)
⊢ Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x - ((↑z : M) - x))

Tactic:
Submodule.sub_mem _ hy hz

Premises used: Submodule.sub_mem
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
y z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hz : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)
d : FiniteArchimedeanClass M
hd : d ≤ c
this : (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)
⊢ Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x - ((↑z : M) - x))

Tactic:
exact Submodule.sub_mem _ hy hz

Premises used: Submodule.sub_mem
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
⊢ ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)

Tactic:
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K c := ⟨y, hy⟩
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
hnonempty :
  ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
⊢ f.evalCoeff x c =
    coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
      c

Tactic:
simpa [evalCoeff, dif_pos hnonempty] using coeff_eq_of_mem f x hnonempty.choose_spec hy le_rfl

Premises used: HahnEmbedding.Partial.evalCoeff, Exists.choose_spec, le_rfl, HahnEmbedding.Partial.coeff_eq_of_mem, dif_pos
-- 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
f : Partial seed
x : M
c : FiniteArchimedeanClass M
h :
  ¬∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
      Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
rw :
  Eq.{u_3 + 1} (α := R)
    (if h :
        ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
          Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x) then
      coeff
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
              ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
            (h.choose (p := fun (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ↦
              Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)))))
        c
    else 0)
    0
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) 0 0
⊢ f.evalCoeff x c = 0

Tactic:
rw [evalCoeff, dif_neg h]

Premises used: HahnEmbedding.Partial.evalCoeff, dif_neg
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
rw : ∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ Function.support (f.evalCoeff x)
⊢ (Function.support (f.evalCoeff x)).IsWF

Tactic:
rw [Set.isWF_iff_no_descending_seq]

Premises used: Set.isWF_iff_no_descending_seq
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
by_contra! :
  ∀ (seq : ℕ → FiniteArchimedeanClass M) (hanti : StrictAnti seq)
    (hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)), False
⊢ ∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ Function.support (f.evalCoeff x)

Tactic:
by_contra! ⟨seq, ⟨hanti, hmem⟩⟩
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
⊢ seq 0 ∈ Function.support (f.evalCoeff x)

Tactic:
specialize hmem 0

Premises used: OfNat.ofNat
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : seq 0 ∈ Function.support (f.evalCoeff x)
contrapose :
  ∀
    (hempty :
      ¬∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
          Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)),
    seq 0 ∉ Function.support (f.evalCoeff x)
⊢ ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)

Tactic:
contrapose hmem 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hempty :
  ¬∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
      Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
⊢ seq 0 ∉ Function.support (f.evalCoeff x)

Tactic:
simp [evalCoeff, dif_neg hempty]

Premises used: HahnEmbedding.Partial.evalCoeff, dif_neg
-- 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
⊢ ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)

Tactic:
have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K (seq 0) := by
    specialize hmem 0
    contrapose hmem with hempty
    simp [evalCoeff, dif_neg 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : ∀ (n : ℕ), seq n ∈ Function.support (f.evalCoeff x)
hnonempty :
  ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
obtain :
  ∀ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain)
    (hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)), False
⊢ False

Tactic:
obtain ⟨y, hy⟩ := hnonempty