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
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ((∃ (m : ℕ), |y| ≤ m • |x|) ∧ ∃ (n : ℕ), |x| ≤ n • |y|) ↔
    (∃ (m : ℕ), |(↑y : M)| ≤ m • |(↑x : M)|) ∧ ∃ (n : ℕ), |(↑x : M)| ≤ n • |(↑y : M)|

Tactic:
aesop
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
inl :
  ∀ (hsubsingleton : Subsingleton M),
    Eq.{u_2 + 1} (α := 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)))
        (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⟧)
              y))) ↔
      Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
inr :
  ∀ (hnontrivial : Nontrivial M),
    Eq.{u_2 + 1} (α := 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)))
        (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⟧)
              y))) ↔
      Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
⊢ Eq.{u_2 + 1} (α := 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)))
      (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⟧)
            y))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
obtain hsubsingleton | hnontrivial := subsingleton_or_nontrivial M

Premises used: subsingleton_or_nontrivial
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hsubsingleton : Subsingleton M
⊢ y = x

Tactic:
have : y = x := Subtype.ext <| hsubsingleton.allEq _ _
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hsubsingleton : Subsingleton M
this : y = x
⊢ Eq.{u_2 + 1} (α := 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)))
      (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⟧)
            y))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
simp [this]
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
⊢ Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)

Tactic:
have hnonempty : Nonempty (FiniteArchimedeanClass M) := inferInstance
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
inr :
  ∀ (c : FiniteArchimedeanClass M),
    Eq.{u_2 + 1} (α := 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)))
        (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⟧)
              y))) ↔
      Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
⊢ Eq.{u_2 + 1} (α := 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)))
      (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⟧)
            y))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
obtain c := hnonempty.some

Premises used: Nonempty.some
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
⊢ Nontrivial R

Tactic:
have : Nontrivial R := (seed.strictMono_coeff c).injective.nontrivial
-- 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 y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
inr :
  Eq.{u_2 + 1} (α := 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)))
      (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⟧)
            y))) ↔
    Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          x))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y))
⊢ Eq.{u_2 + 1} (α := 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)))
      (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⟧)
            y))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
rw [← archimedeanClassMk_eq_iff]

Premises used: HahnEmbedding.Partial.archimedeanClassMk_eq_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
pos :
  ∀ (hx0 : x = 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)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
neg :
  ∀ (hx0 : ¬x = 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)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ 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:
by_cases hx0 : x = 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
⊢ 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 [hx0]
-- 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
⊢ (↑x : M) ≠ 0

Tactic:
simpa using hx0
-- 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
⊢ (↑x : M) ≠ 0

Tactic:
have hx0' : x.val ≠ 0 := by simpa using hx0
-- 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
neg :
  ∀ (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),
    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)
⊢ 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:
obtain ⟨⟨x', hx'mem⟩, hx'0⟩ := exists_ne (0 : seed.stratum (.mk x hx0'))

Premises used: exists_ne, OfNat.ofNat
-- 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
apply : x' ≠ 0
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))

Tactic:
apply seed.archimedeanClassMk_of_mem_stratum hx'mem

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, HahnEmbedding.Seed.toArchimedeanStrata
-- 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
⊢ x' ≠ 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
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk x') (ArchimedeanClass.mk (↑x : M))

Tactic:
have heq : ArchimedeanClass.mk x' = .mk x.val := by
    apply seed.archimedeanClassMk_of_mem_stratum hx'mem
    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' ⋯
⊢ (↑x'' : M) ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x : M) hx0')

Tactic:
have hx''mem : x''.val ∈ seed.stratum (mk x.val hx0') := hx'mem