awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c_1 : Set (Partial seed)
hnonempty : c_1.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c_1
x : ↥(sSupFun (c := c_1) hc).domain
c : FiniteArchimedeanClass M
hx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1)))
    (↑x : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1) f
hf : (↑x : M) ∈ f.domain
f' : Partial seed
hmem'_1 : f' ∈ c_1
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
x' : ↥f.domain
hx' :
  (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) x' =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑x : M) hf))))
hmem' : (↑x' : M) ∈ (sSupFun (c := c_1) hc).domain
⊢ (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (sSupFun (c := c_1) hc).domain) (↑x' : M) hmem') =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
have hleft : (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ (sSupFun (c := c_1) hc).domain) (↑x' : M) hmem') =
  (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) x'
Tactic: have hleft : sSupFun hc ⟨x'.val, hmem'⟩ = f x' := LinearPMap.sSup_apply _ hmem _
-- 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
c_1 : Set (Partial seed)
hnonempty : c_1.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c_1
x : ↥(sSupFun (c := c_1) hc).domain
c : FiniteArchimedeanClass M
hx :
  Membership.mem (γ := Submodule K M)
    (sSup
      (Set.image (α := M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) LinearPMap.domain
        ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1)))
    (↑x : M)
f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hmem :
  Membership.mem (γ := Set (M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
    ((fun (x : Partial seed) ↦ (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)) '' c_1) f
hf : (↑x : M) ∈ f.domain
f' : Partial seed
hmem'_1 : f' ∈ c_1
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
x' : ↥f.domain
hx' :
  (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) x' =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑x : M) hf))))
hmem' : (↑x' : M) ∈ (sSupFun (c := c_1) hc).domain
hleft :
  (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (sSupFun (c := c_1) hc).domain) (↑x' : M) hmem') =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) x'
⊢ (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ (sSupFun (c := c_1) hc).domain) (↑x' : M) hmem') =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
have hright : (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) x =
  (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑x : M) hf)
Tactic: have hright : sSupFun hc x = f ⟨x, hf⟩ := LinearPMap.sSup_apply _ hmem ⟨x, hf⟩
-- 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
inst_12 : IsOrderedAddMonoid R
⊢ ∃ (f : Partial seed), IsMax f
have h : ∀ (c : Set (Partial seed)), IsChain (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c → c.Nonempty → BddAbove c
Tactic: apply zorn_le_nonempty
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
⊢ ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
have obtain : ∀ (f : Partial seed) (hf : IsMax f), ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
Tactic: obtain ⟨f, hf⟩ := exists_isMax seed
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : IsMax f
⊢ ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
have refine : ∀ (x : M), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
Tactic: refine ⟨f, Submodule.eq_top_iff'.mpr ?_⟩
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : IsMax f
⊢ ∀ (x : M), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have hf₁ : ∀ (b : Partial seed), ¬f < b
Tactic: rw [isMax_iff_forall_not_lt] at hf
Cleared hypotheses: hf
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : ∀ (b : Partial seed), ¬f < b
⊢ ∀ (x : M), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have contrapose! : ∀ (hx : ∃ (x : M), x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain), ∃ (b : Partial seed), f < b
Tactic: contrapose! hf with hx
Cleared hypotheses: hf
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hx : ∃ (x : M), x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ∃ (b : Partial seed), f < b
have obtain : ∀ (x : M) (hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain), ∃ (b : Partial seed), f < b
Tactic: obtain ⟨x, hx⟩ := hx
Cleared hypotheses: hx
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
⊢ ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((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 : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
have obtain : ∀ (e : HahnEmbedding.Partial h.some) (hdomain : (↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤),
  ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((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 : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
Tactic: obtain ⟨e, hdomain⟩ := HahnEmbedding.Partial.exists_domain_eq_top h.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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
e : HahnEmbedding.Partial h.some
hdomain : (↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
⊢ ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((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 : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
have harch : ∀ (x : ↥(↑e : 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⟧)
            ((↑(↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                ↥(↑e : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
              x))) :
      ArchimedeanClass M)
    (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
Tactic: obtain harch := e.orderTop_eq_archimedeanClassMk
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            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⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ ∃ (f : M →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)),
    StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
        (⇑f : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((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 : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧) a))))
have refine_1 : StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
  (⇑(f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id sorry) : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧)
Tactic: refine ⟨f ∘ₗ LinearMap.id.codRestrict ⊤ (by simp), ?_, ?_⟩
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
h : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
hpartial : HahnEmbedding.IsPartial h.some { domain := ⊤, toFun := f }
harch :
  ∀
    (x :
      ↥(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                HahnEmbedding.IsPartial h.some f)
                { domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                hpartial) :
            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⟧)
              ((↑(↑(Subtype.mk (p := fun (f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) ↦
                          HahnEmbedding.IsPartial h.some f)
                          { domain := ⊤, toFun := f :
                            M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }
                          hpartial) :
                      M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
                  ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain →
                    Lex R⟦FiniteArchimedeanClass M⟧)
                x))) :
        ArchimedeanClass M)
      (ArchimedeanClass.mk (↑x : M) : ArchimedeanClass M)
⊢ StrictMono (α := M) (β := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (⇑(f ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) : (a : M) → Lex R⟦FiniteArchimedeanClass M⟧)
have refine_1 : StrictMono (α := M) (β :=
  ↥{ domain := ⊤, toFun := f : M →ₗ.[K] Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R) }.domain)
  (⇑(LinearMap.codRestrict ⊤ LinearMap.id sorry) : (a : M) → ↥⊤)
Tactic: apply hpartial.strictMono.comp
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ α
inst_2 : MulAction ℚ≥0 α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ _q • _a₁ ≤ _q • _a₂
have rw : HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ ≤ HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂
Tactic: rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : MulAction ℚ≥0 α
inst_2 : MulAction ℚ α
inst_3 : IsScalarTower ℚ≥0 ℚ α
inst_4 : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ _q • _a₁ < _q • _a₂
have rw : HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₁ < HSMul.hSMul (α := ℚ) (↑_q : ℚ) _a₂
Tactic: rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : DistribMulAction ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
⊢ |q • a| = q • |a|
have inl : ∀ (ha : a ≤ 0), |q • a| = q • |a|
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : DistribMulAction ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
inl : ∀ (ha : a ≤ 0), |q • a| = q • |a|
⊢ |q • a| = q • |a|
have inr : ∀ (ha : 0 ≤ a), |q • a| = q • |a|
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b
have rw : (↑q : α) * a < (↑q : α) * b
Tactic: rw [NNRat.smul_def, NNRat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Rat (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b
have rw : (↑q : α) * a < (↑q : α) * b
Tactic: rw [Rat.smul_def, Rat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Basic (goal)
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f (a * c) ≤ f (b * c)
have rw : f a * f c ≤ f b * f c
Tactic: rw [mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Basic (goal)
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f a * f c ≤ f b * f c
have grw : f b * f c ≤ f b * f c
Tactic: grw [le.2 ab]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Basic (goal)
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f a * f b ≤ f a * f c
have rwa : f (a * b) ≤ f a * f c
Tactic: rwa [← mul, ← mul, le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Basic (goal)
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
rwa : f (a * b) ≤ f a * f c
⊢ f a * f b ≤ f a * f c
have rwa₁ : f (a * b) ≤ f (a * c)
Tactic: rwa [← mul, ← mul, le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl : ∀ (h : a < b), a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
Tactic: obtain h | h := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
inl : ∀ (h : a < b), a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inr : ∀ (h : b ≤ a), a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
Tactic: obtain h | h := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have this : a < b + c
Tactic: have : a < b + c := h.trans_le (le_self_add ..)
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a < b + c
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl : a < b + c → a < b ∨ ∃ d < c, a = b + d
Tactic: tauto