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
x : M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
z : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) = x - (↑z : M) + ((↑z : M) - (↑y : M))
hyz : ¬(↑z : M) - (↑y : M) = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M) (hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M))),
    Eq.{u_3 + 1} (α := R)
      (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval 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⟧)
            z))
        c)
h2 : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk ((↑z : M) - (↑y : M))) (ArchimedeanClass.mk (x - (↑z : M)))
⊢ ∃ (c : FiniteArchimedeanClass M),
    (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M)) ∧
      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⟧)
              (z - y)))
          c)
        0

Tactic:
exact ⟨FiniteArchimedeanClass.mk (z.val - y.val) hyz, h2, coeff_ne_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
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
contrapose : ∀ (hx : (↑y : M) - x = 0), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ (↑y : M) - x ≠ 0

Tactic:
contrapose 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
f : Partial seed
x : M
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : (↑y : M) - x = 0
⊢ x = (↑y : M)

Tactic:
(sub_eq_zero.mp hx).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- 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
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : (↑y : M) - x = 0
obtain : ∀ (hx : (↑y : M) - (↑y : M) = 0), (↑y : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
obtain rfl : x = y.val := (sub_eq_zero.mp hx).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm, Subtype.val, 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
f : Partial seed
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : (↑y : M) - (↑y : M) = 0
⊢ (↑y : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ (↑y : M) - x ≠ 0

Tactic:
have := val_sub_ne_zero f hx y
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : (↑y : M) - x ≠ 0
⊢ x - (↑y : M) ≠ 0

Tactic:
rw [sub_ne_zero, ne_comm, ← sub_ne_zero] at this

Premises used: sub_ne_zero, ne_comm
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
h : Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) ⊤
simp : xy ≤ xy
⊢ Membership.mem (γ := UpperSet (FiniteArchimedeanClass M)) (UpperSet.Ici xy)
    (Subtype.mk (p := fun (A : ArchimedeanClass M) ↦ A ≠ ⊤) (ArchimedeanClass.mk (x - (↑y : M))) h)

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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
h : Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) ⊤
⊢ xy ≤ xy

Tactic:
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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
⊢ Membership.mem (γ := Submodule K M) (closedBall K xy) (x - (↑y : M))

Tactic:
have hxy : x - y.val ∈ closedBall K xy := fun _ ↦ by simp; 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
hxy : ∃ (y_1 : M), Membership.mem (γ := Submodule K M) (ball K xy) y_1 ∧ ∃ z ∈ seed.stratum xy, y_1 + z = x - (↑y : M)
obtain :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule K M) (ball K xy) u) (v : M) (hv : v ∈ seed.stratum xy)
    (huv : u + v = x - (↑y : M)),
    f.eval x ≠
      (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        y
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := hxy
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : Membership.mem (γ := Submodule K M) (ball K xy) u
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
⊢ x - (↑y : M) - v = u

Tactic:
simp [← huv]
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : Membership.mem (γ := Submodule K M) (ball K xy) u
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
⊢ x - (↑y : M) - v = u

Tactic:
have huv' : x - y.val - v = u := by simp [← huv]
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : Membership.mem (γ := Submodule K M) (ball K xy) u
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
rw :
  ∀ (hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h) (v : M) (hv : v ∈ seed.stratum xy)
    (huv : u + v = x - (↑y : M)) (huv' : x - (↑y : M) - v = u),
    f.eval x ≠
      (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
          ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
        y
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y

Tactic:
rw [mem_ball_iff K] at hu

Premises used: FiniteArchimedeanClass.mem_ball_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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
⊢ (↑y : M) ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
⊢ (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
have hyv : y.val + v ∈ f.val.domain := Submodule.add_mem _ (by simp) (f.mem_domain hv)
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
by_contra! :
  ∀
    (h :
      f.eval x =
        (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y),
    False
⊢ f.eval x ≠
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y

Tactic:
by_contra! 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
⊢ LE.le (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))
    (ArchimedeanClass.mk (x - (↑y : M)))

Tactic:
obtain h := f.archimedeanClassMk_le_of_eval_eq h ⟨y.val + v, hyv⟩

Premises used: Subtype.mk, HAdd.hAdd, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, Subtype.val
-- 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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h :
  LE.le (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))
    (ArchimedeanClass.mk (x - (↑y : M)))
contrapose! :
  ∀ (h : True),
    LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M)))
      (ArchimedeanClass.mk
        (x -
          (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
                hyv) :
            M)))
⊢ False

Tactic:
contrapose! 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
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h : True
simp_rw : LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M)))
    (ArchimedeanClass.mk
      (x -
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) ((↑y : M) + v)
              hyv) :
          M)))

Tactic:
simp_rw [← sub_sub, huv']

Premises used: sub_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
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
this : x - (↑y : M) ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - (↑y : M)) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - (↑y : M)
huv' : x - (↑y : M) - v = u
hyv : (↑y : M) + v ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
h_1 :
  f.eval x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      y
h : True
inl :
  ∀ (hu : ∀ (h : Ne.{u_2 + 1} (α := M) 0 0), xy < FiniteArchimedeanClass.mk 0 h) (huv : 0 + v = x - (↑y : M))
    (huv' : x - (↑y : M) - v = 0),
    LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk 0)
inr : ∀ (ne : u ≠ 0), LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)
⊢ LT.lt (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑y : M))) (ArchimedeanClass.mk u)

Tactic:
obtain rfl | ne := eq_or_ne u 0

Premises used: eq_or_ne, OfNat.ofNat, rfl