awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ 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 (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
have simp_rw : Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((orderHom f.toOrderAddMonoidHom :
          (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
            ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
        (ArchimedeanClass.mk x) :
      ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((orderHom f.toOrderAddMonoidHom :
          (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
            ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
        (ArchimedeanClass.mk y) :
      ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
  Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
Tactic: simp_rw [← toOrderAddMonoidHom_apply, ← orderHom_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
have trans : Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((orderHom f.toOrderAddMonoidHom :
          (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
            ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
        (ArchimedeanClass.mk x) :
      ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((orderHom f.toOrderAddMonoidHom :
          (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
            ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
        (ArchimedeanClass.mk y) :
      ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
  Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
    (ArchimedeanClass.mk y)
Tactic: trans ArchimedeanClass.mk x = .mk y
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
trans :
  Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y)
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
have trans₁ : Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
    (ArchimedeanClass.mk y) ↔
  Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
Tactic: trans ArchimedeanClass.mk x = .mk y
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
have simp_rw : ((∃ (m : ℕ), |y| ≤ m • |x|) ∧ ∃ (n : ℕ), |x| ≤ n • |y|) ↔
  (∃ (m : ℕ), |(↑y : M)| ≤ m • |(↑x : M)|) ∧ ∃ (n : ℕ), |(↑x : M)| ≤ n • |(↑y : M)|
Tactic: simp_rw [mk_eq_mk]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ 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))
have 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))
Tactic: obtain hsubsingleton | hnontrivial := subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x 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))
⊢ 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))
have 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))
Tactic: obtain hsubsingleton | hnontrivial := subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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))
have this : y = x
Tactic: have : y = x := Subtype.ext <| hsubsingleton.allEq _ _
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
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))
have hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
Tactic: have hnonempty : Nonempty (FiniteArchimedeanClass M) := inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (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))
have 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))
Tactic: obtain c := hnonempty.some
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty.{u_2 + 1} (FiniteArchimedeanClass M)
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))
have this : Nontrivial R
Tactic: have : Nontrivial R := (seed.strictMono_coeff c).injective.nontrivial
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x 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
⊢ 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))
have 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))
Tactic: rw [← archimedeanClassMk_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ 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)
have 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)
Tactic: by_cases hx0 : x = 0