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
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
⊢ 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⟧)
          x))
      d)
    0
have inr : (↑d : WithTop (FiniteArchimedeanClass M)) <
  orderTop.{u_2, u_3} (R := R)
    ((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))
Tactic: apply HahnSeries.coeff_eq_zero_of_lt_orderTop
-- 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
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
⊢ (↑d : WithTop (FiniteArchimedeanClass M)) <
    orderTop.{u_2, u_3} (R := R)
      ((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))
have apply_fun : LT.lt (α := ArchimedeanClass M)
  ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
      (↑d : WithTop (FiniteArchimedeanClass M)) :
    ArchimedeanClass M)
  ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
      (orderTop.{u_2, u_3} (R := R)
        ((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))) :
    ArchimedeanClass M)
Tactic: apply_fun FiniteArchimedeanClass.withTopOrderIso _
-- 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
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
⊢ LT.lt (α := ArchimedeanClass M)
    ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (↑d : WithTop (FiniteArchimedeanClass M)) :
      ArchimedeanClass M)
    ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (orderTop.{u_2, u_3} (R := R)
          ((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))) :
      ArchimedeanClass M)
have rw : (↑d : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)
Tactic: rw [orderTop_eq_archimedeanClassMk, FiniteArchimedeanClass.withTopOrderIso_apply_coe]
-- 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
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
⊢ (↑d : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)
have apply : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)
Tactic: apply lt_of_le_of_lt hd
-- 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
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))
      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)
have 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
Tactic: apply eq_of_sub_eq_zero
-- 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
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
⊢ 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
have 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
Tactic: rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub]
-- 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
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
have h : Membership.mem (γ := Submodule K M) (ball K c) (↑(y - z) : M)
Tactic: refine coeff_eq_zero_of_mem f ?_ hd
-- 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
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)
have push_cast : (↑y : M) - (↑z : M) = (↑y : M) - x - ((↑z : M) - x)
Tactic: push_cast
-- 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
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
⊢ Membership.mem (γ := Submodule K M) (ball K c) (↑(y - z) : M)
have this : (↑(y - z) : M) = (↑y : M) - x - ((↑z : M) - x)
Tactic: have : (y - z).val = (y.val - x) - (z.val - x) := by
    push_cast
    simp
-- 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
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 - z) : M)
have h : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x - ((↑z : M) - x))
Tactic: rw [this]
-- 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
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)
⊢ 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
have hnonempty : ∃ (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⟩
-- 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
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)
⊢ f.evalCoeff x c = 0
have 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
Tactic: rw [evalCoeff, dif_neg 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
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
⊢ f.evalCoeff x c = 0
have rw₁ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [evalCoeff, dif_neg 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
⊢ (Function.support (f.evalCoeff x)).IsWF
have rw : ∀ (f_1 : ℕ → FiniteArchimedeanClass M), StrictAnti f_1 → ¬∀ (n : ℕ), f_1 n ∈ Function.support (f.evalCoeff x)
Tactic: rw [Set.isWF_iff_no_descending_seq]
-- 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
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)
have hmem₁ : seq 0 ∈ Function.support (f.evalCoeff x)
Tactic: specialize hmem 0
Cleared hypotheses: 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
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)
⊢ ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
    Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
have 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)
Tactic: contrapose hmem with hempty
Cleared hypotheses: hmem
-- 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
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)
⊢ False
have hnonempty : ∃ (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]
-- 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
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)
⊢ False
have obtain : ∀ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain)
  (hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)), False
Tactic: obtain ⟨y, hy⟩ := hnonempty
Cleared hypotheses: hnonempty
-- 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
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
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
n : ℕ
⊢ Membership.mem (γ := Set (FiniteArchimedeanClass M))
    (Function.support.{u_2, u_3} (M := 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))))
    (seq n)
have hmem₁ : seq n ∈ Function.support (f.evalCoeff x)
Tactic: specialize hmem n
Cleared hypotheses: hmem