awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
n : ℕ
hmem : seq n ∈ Function.support (f.evalCoeff x)
⊢ 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₁ : f.evalCoeff x (seq n) ≠ 0
Tactic: rw [Function.mem_support] at ⊢ hmem
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
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ Ne.{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))
      (seq n))
    0
have h : 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) =
  f.evalCoeff x (seq n)
Tactic: convert! hmem using 1
-- 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
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ 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) =
    f.evalCoeff x (seq n)
have h : seq n ≤ seq 0
Tactic: refine (f.evalCoeff_eq ((ball_strictAnti K).antitone ?_ hy)).symm
-- 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)
⊢ False
have hmem' : ∀ (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)
Tactic: have hmem' (n : ℕ) : seq n ∈ (ofLex (f.val y)).coeff.support := by
    specialize hmem n
    rw [Function.mem_support] at ⊢ hmem
    convert! hmem using 1
    refine (f.evalCoeff_eq ((ball_strictAnti K).antitone ?_ hy)).symm
    simpa using hanti.antitone (show 0 ≤ n 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
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)
hmem' :
  ∀ (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)
⊢ False
have hwf : Set.IsWF.{u_2} (α := FiniteArchimedeanClass M)
  (support.{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⟧)
        y)))
Tactic: obtain hwf := (ofLex (f.val y)).isWF_support
-- 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)
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
hmem' :
  ∀ (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)
hwf :
  Set.IsWF.{u_2} (α := FiniteArchimedeanClass M)
    (support.{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⟧)
          y)))
⊢ False
have contrapose! : ∀ (hwf : True),
  ¬Set.IsWF.{u_2} (α := FiniteArchimedeanClass M)
      (support.{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⟧)
            y)))
Tactic: contrapose! hwf
Cleared hypotheses: hwf
-- 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)
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K (seq 0)) ((↑y : M) - x)
hmem' :
  ∀ (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)
hwf : True
⊢ ¬Set.IsWF.{u_2} (α := FiniteArchimedeanClass M)
      (support.{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⟧)
            y)))
have rw : ¬∀ (f_1 : ℕ → FiniteArchimedeanClass M),
    StrictAnti f_1 →
      ¬∀ (n : ℕ),
          Membership.mem (γ := Set (FiniteArchimedeanClass M))
            (support.{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⟧)
                  y)))
            (f_1 n)
Tactic: rw [Set.isWF_iff_no_descending_seq]
-- 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
⊢ Eq (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
        { coeff := f.evalCoeff 0, isPWO_support' := ⋯ } :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (0 : Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
have h : f.evalCoeff 0 = coeff 0
Tactic: convert! toLex_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
⊢ f.evalCoeff 0 = coeff 0
have h : ∀ (c : FiniteArchimedeanClass M), f.evalCoeff 0 c = coeff 0 c
Tactic: ext 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
⊢ f.evalCoeff 0 c = coeff 0 c
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⟧)
        0))
    c)
  (coeff 0 c)
Tactic: rw [f.evalCoeff_eq (y := 0) (by 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
k : K
x : M
⊢ f.eval (k • x) = k • f.eval x
have pos : ∀ (hk : k = 0), f.eval (k • x) = k • f.eval x
Tactic: by_cases hk : k = 0
-- 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
k : K
x : M
pos : ∀ (hk : k = 0), f.eval (k • x) = k • f.eval x
⊢ f.eval (k • x) = k • f.eval x
have neg : ∀ (hk : ¬k = 0), f.eval (k • x) = k • f.eval x
Tactic: by_cases hk : k = 0
-- 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
k : K
x : M
hk : ¬k = 0
⊢ f.eval (k • x) = k • f.eval x
have neg : (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
    { coeff := f.evalCoeff (k • x), isPWO_support' := sorry } =
  HSMul.hSMul (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) k
    ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
        { coeff := f.evalCoeff x, isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R } :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
Tactic: unfold eval
-- 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
k : K
x : M
hk : ¬k = 0
⊢ (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ } =
    HSMul.hSMul (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) k
      ((toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
          { coeff := f.evalCoeff x, isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R } :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
have neg : { coeff := f.evalCoeff (k • x), isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R } =
  k • { coeff := f.evalCoeff x, isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }
Tactic: rw [← toLex_smul, toLex.injective.eq_iff]
-- 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
k : K
x : M
hk : ¬k = 0
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R } =
    k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }
have neg : ∀ (c : FiniteArchimedeanClass M),
  { coeff := f.evalCoeff (k • x), isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := sorry : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }).coeff c
Tactic: ext 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ : HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R }).coeff c
have neg : f.evalCoeff (k • x) c = k • f.evalCoeff x c
Tactic: suffices f.evalCoeff (k • x) c = k • f.evalCoeff x c by simpa using this
-- 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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
have pos : ∀
  (h :
    ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
      Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)),
  f.evalCoeff (k • x) c = k • f.evalCoeff x c
Tactic: by_cases h : ∃ y : f.val.domain, y.val - x ∈ ball K 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
pos :
  ∀
    (h :
      ∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
        Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)),
    f.evalCoeff (k • x) c = k • f.evalCoeff x c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
have neg : ∀
  (h :
    ¬∃ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain),
        Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)),
  f.evalCoeff (k • x) c = k • f.evalCoeff x c
Tactic: by_cases h : ∃ y : f.val.domain, y.val - x ∈ ball K 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
k : K
x : M
hk : ¬k = 0
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 (k • x) c = k • f.evalCoeff x c
have pos : ∀ (y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain)
  (hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)), f.evalCoeff (k • x) c = k • f.evalCoeff x c
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
k : K
x : M
hk : ¬k = 0
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 (k • x) c = k • f.evalCoeff x c
have heq : (↑(k • y) : M) - k • x = k • ((↑y : M) - x)
Tactic: have heq : (k • y).val - k • x = k • (y.val - x) := by simp [smul_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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑y : M) - x)
heq : (↑(k • y) : M) - k • x = k • ((↑y : M) - x)
⊢ Membership.mem (γ := Submodule K M) (ball K c) ((↑(k • y) : M) - k • x)
have rw : Membership.mem (γ := Submodule K M) (ball K c) (k • ((↑y : M) - x))
Tactic: rw [heq]