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))
hab : LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))
⊢ LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M)))
    (ArchimedeanClass.mk (x - (↑z : M) + ((↑z : M) - (↑y : M))))

Tactic:
apply ArchimedeanClass.mk_left_le_mk_add

Premises used: ArchimedeanClass.mk_left_le_mk_add
-- 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))
pos :
  ∀ (hyz : (↑z : M) - (↑y : M) = 0),
    LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))
neg :
  ∀ (hyz : ¬(↑z : M) - (↑y : M) = 0),
    LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))
⊢ LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))

Tactic:
by_cases hyz : z.val - y.val = 0

Premises used: 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
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
⊢ LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))

Tactic:
simp [hyz]
-- 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
c : FiniteArchimedeanClass M
hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M))
⊢ (↑c : ArchimedeanClass M) < ArchimedeanClass.mk ((↑z : M) - x)

Tactic:
rw [ArchimedeanClass.mk_sub_comm] at hc

Premises used: ArchimedeanClass.mk_sub_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
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
c : FiniteArchimedeanClass M
hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk ((↑z : M) - x)
simp_rw :
  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⟧)
          z))
      c
⊢ 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)

Tactic:
simp_rw [eval, ofLex_toLex]

Premises used: ofLex_toLex, HahnEmbedding.Partial.eval
-- 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
c : FiniteArchimedeanClass M
hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk ((↑z : M) - x)
hy : Membership.mem (γ := Submodule K M) (ball K c) ((↑z : 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⟧)
          z))
      c

Tactic:
apply evalCoeff_eq

Premises used: HahnEmbedding.Partial.evalCoeff_eq
-- 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
c : FiniteArchimedeanClass M
hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk ((↑z : M) - x)
⊢ Membership.mem (γ := Submodule K M) (ball K c) ((↑z : M) - x)

Tactic:
simpa [c.prop] using fun _ ↦ hc

Premises used: Subtype.prop
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
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
⊢ ∀ (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)

Tactic:
have h1 (c : FiniteArchimedeanClass M) (hc : c.val < .mk (x - z.val)) :
      (ofLex (f.eval x)).coeff c = (ofLex (f.val z)).coeff c := by
    rw [ArchimedeanClass.mk_sub_comm] at hc
    simp_rw [eval, ofLex_toLex]
    apply evalCoeff_eq
    simpa [c.prop] using fun _ ↦ hc
-- 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)
c : FiniteArchimedeanClass M
hc : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑z : M))
rw :
  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⟧)
          z))
      c)
    (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) 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⟧)
          (z - y)))
      c)
    0

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

Premises used: ofLex_sub, sub_eq_zero, 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 : ↥(↑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)
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 : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      c)
    (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) c)

Tactic:
(h1 c hc).symm

Premises used: 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
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)
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 : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          z))
      c)
    (coeff ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧) (f.eval x)) c)

Tactic:
exact (h1 c hc).symm

Premises used: 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
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)
⊢ ∀ (c : FiniteArchimedeanClass M),
    (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑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⟧)
              (z - y)))
          c)
        0

Tactic:
have h2 : ∀ c : FiniteArchimedeanClass M, c.val < .mk (x - z.val) →
      (ofLex (f.val (z - y))).coeff c = 0 := by
    intro c hc
    rw [LinearPMap.map_sub, ofLex_sub, HahnSeries.coeff_sub, sub_eq_zero, ← h]
    exact (h1 c hc).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
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 :
  ∀ (c : FiniteArchimedeanClass M),
    (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (x - (↑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⟧)
              (z - y)))
          c)
        0
neg :
  ∀
    (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
⊢ LE.le (α := ArchimedeanClass M) (ArchimedeanClass.mk (x - (↑z : M))) (ArchimedeanClass.mk ((↑z : M) - (↑y : M)))

Tactic:
contrapose! h2
-- 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:
⟨FiniteArchimedeanClass.mk (z.val - y.val) hyz, h2, coeff_ne_zero _ _⟩

Premises used: HSub.hSub, FiniteArchimedeanClass.mk, And.intro, Exists.intro, HahnEmbedding.Partial.coeff_ne_zero, Subtype.val