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 : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
rw :
  Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M) hx''mem ≠ 0
⊢ Ne.{u_3 + 1} (α := R)
    ((seed.coeff (FiniteArchimedeanClass.mk (↑x : M) hx0') :
          (a : ↥(seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M)
          hx''mem) :
      R)
    (0 : R)

Tactic:
rw [(LinearMap.map_eq_zero_iff _ (seed.strictMono_coeff _).injective).ne]

Premises used: HahnEmbedding.Seed.strictMono_coeff, StrictMono.injective, Iff.ne, LinearMap.map_eq_zero_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 : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
unfold :
  Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯) : M) hx''mem ≠
    0
⊢ Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M) hx''mem ≠ 0

Tactic:
unfold x''
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
⊢ Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯) : M) hx''mem ≠
    0

Tactic:
simpa using hx'0
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
⊢ Ne.{u_3 + 1} (α := R)
    ((seed.coeff (FiniteArchimedeanClass.mk (↑x : M) hx0') :
          (a : ↥(seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M)
          hx''mem) :
      R)
    (0 : R)

Tactic:
have h0 : (seed.coeff (mk x.val hx0')) ⟨x''.val, hx''mem⟩ ≠ 0 := by
    rw [(LinearMap.map_eq_zero_iff _ (seed.strictMono_coeff _).injective).ne]
    unfold x''
    simpa using hx'0
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
h0 :
  Ne.{u_3 + 1} (α := R)
    ((seed.coeff (FiniteArchimedeanClass.mk (↑x : M) hx0') :
          (a : ↥(seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M)
          hx''mem) :
      R)
    (0 : R)
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x'' : M)) (ArchimedeanClass.mk (↑x : M))

Tactic:
have heq' : ArchimedeanClass.mk x''.val = .mk x.val := heq
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
h0 :
  Ne.{u_3 + 1} (α := R)
    ((seed.coeff (FiniteArchimedeanClass.mk (↑x : M) hx0') :
          (a : ↥(seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M)
          hx''mem) :
      R)
    (0 : R)
heq' : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x'' : M)) (ArchimedeanClass.mk (↑x : M))
⊢ Eq (α := WithTop (FiniteArchimedeanClass M))
    (↑(FiniteArchimedeanClass.mk (↑x : M) hx0') : 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:
rw [← orderTop_eq_iff, apply_of_mem_stratum f hx''mem, ofLex_toLex,
    HahnSeries.orderTop_single h0] at heq'

Premises used: HahnEmbedding.Partial.orderTop_eq_iff, ofLex_toLex, HahnEmbedding.Partial.apply_of_mem_stratum, HahnSeries.orderTop_single
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : ¬x = 0
hx0' : (↑x : M) ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
hx'0 : Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) x' hx'mem ≠ 0
heq : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))
x'' : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain :=
  Subtype.mk (p := fun (x : M) ↦ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) x' ⋯
hx''mem : (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')
h0 :
  Ne.{u_3 + 1} (α := R)
    ((seed.coeff (FiniteArchimedeanClass.mk (↑x : M) hx0') :
          (a : ↥(seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0'))) → R)
        (Subtype.mk (p := fun (x_1 : M) ↦ x_1 ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')) (↑x'' : M)
          hx''mem) :
      R)
    (0 : R)
heq' :
  Eq (α := WithTop (FiniteArchimedeanClass M))
    (↑(FiniteArchimedeanClass.mk (↑x : M) hx0') : 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)))
⊢ Eq (α := 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)
    (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)

Tactic:
simp [← heq']
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : (↑x : M) ≠ 0
apply_fun :
  Eq (α := 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)
    ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (↑(FiniteArchimedeanClass.mk (↑x : M) hx0) : WithTop (FiniteArchimedeanClass M)) :
      ArchimedeanClass M)
⊢ Eq (α := 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)))
    (↑(FiniteArchimedeanClass.mk (↑x : M) hx0) : WithTop (FiniteArchimedeanClass M))

Tactic:
apply_fun FiniteArchimedeanClass.withTopOrderIso M

Premises used: FiniteArchimedeanClass.withTopOrderIso
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx0 : (↑x : M) ≠ 0
⊢ Eq (α := 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)
    ((withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
        (↑(FiniteArchimedeanClass.mk (↑x : M) hx0) : WithTop (FiniteArchimedeanClass M)) :
      ArchimedeanClass M)

Tactic:
simp [orderTop_eq_archimedeanClassMk]

Premises used: HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
inl :
  ∀ (hx : Membership.mem (γ := Submodule K M) (ball K c) (↑0 : 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⟧)
            0))
        d)
      0
inr :
  ∀ (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
⊢ 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

Tactic:
obtain rfl | ne := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, 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
c d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑0 : 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⟧)
          0))
      d)
    0

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
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
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))
⊢ 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

Tactic:
apply HahnSeries.coeff_eq_zero_of_lt_orderTop

Premises used: HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
ne : x ≠ 0
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)
⊢ (↑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_fun FiniteArchimedeanClass.withTopOrderIso _

Premises used: FiniteArchimedeanClass.withTopOrderIso
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
ne : x ≠ 0
rw : (↑d : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)
⊢ 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:
rw [orderTop_eq_archimedeanClassMk, FiniteArchimedeanClass.withTopOrderIso_apply_coe]

Premises used: HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, FiniteArchimedeanClass.withTopOrderIso_apply_coe
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
c : FiniteArchimedeanClass M
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hx : Membership.mem (γ := Submodule K M) (ball K c) (↑x : M)
d : FiniteArchimedeanClass M
hd : (↑d : ArchimedeanClass M) ≤ (↑c : ArchimedeanClass M)
ne : x ≠ 0
apply : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)
⊢ (↑d : ArchimedeanClass M) < ArchimedeanClass.mk (↑x : M)

Tactic:
apply lt_of_le_of_lt hd

Premises used: lt_of_le_of_lt