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
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' : 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))))
⊢ (↑f.domain : Set M) ⊆ (↑(sSupFun (c := c_1) hc).domain : Set M)

Tactic:
exact hf'.symm ▸ (le_sSupFun hc hmem').1
-- 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
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' : 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))))
⊢ (↑x' : M) ∈ (sSupFun (c := c_1) hc).domain

Tactic:
have hmem' : x'.val ∈ (sSupFun hc).domain := by
    apply Set.mem_of_mem_of_subset x'.prop
    exact hf'.symm ▸ (le_sSupFun hc hmem').1
-- 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
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
⊢ ∃ (y : ↥(sSupFun (c := c_1) hc).domain),
    (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y =
      (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)))

Tactic:
⟨⟨x'.val, hmem'⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
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
refine :
  (↑(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)))
⊢ ∃ (y : ↥(sSupFun (c := c_1) hc).domain),
    (↑(sSupFun (c := c_1) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) y =
      (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)))

Tactic:
refine ⟨⟨x'.val, hmem'⟩, ?_⟩
-- 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
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') =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) x'

Tactic:
have hleft : sSupFun hc ⟨x'.val, hmem'⟩ = f x' := LinearPMap.sSup_apply _ hmem _
-- 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
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⟧) 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⟩
-- 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
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'
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)
⊢ (↑(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)))

Tactic:
simpa [hleft, hright] using hx'
-- 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
inst_12 : IsOrderedAddMonoid R
h : ∀ (c : Set (Partial seed)), IsChain (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c → c.Nonempty → BddAbove c
⊢ ∃ (f : Partial seed), IsMax f

Tactic:
apply zorn_le_nonempty

Premises used: zorn_le_nonempty
-- 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hc : IsChain (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ BddAbove c

Tactic:
⟨sSup hnonempty hc.directedOn, mem_upperBounds.mpr fun _ hf ↦ le_sSupFun hc.directedOn hf⟩

Premises used: Iff.mpr, HahnEmbedding.Partial.sSup, IsChain.directedOn, HahnEmbedding.Partial.le_sSupFun, BddAbove, Set.Nonempty, Exists.intro, mem_upperBounds
-- 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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hc : IsChain (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ BddAbove c

Tactic:
exact ⟨sSup hnonempty hc.directedOn, mem_upperBounds.mpr fun _ hf ↦ le_sSupFun hc.directedOn hf⟩
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
obtain :
  ∀ (f : Partial seed) (hf : IsMax f), ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤
⊢ ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤

Tactic:
obtain ⟨f, hf⟩ := exists_isMax seed

Premises used: HahnEmbedding.Partial.exists_isMax
-- 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
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 = ⊤

Tactic:
⟨f, Submodule.eq_top_iff'.mpr ?_⟩

Premises used: Iff.mpr, Submodule.eq_top_iff', Exists.intro
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : IsMax f
refine : ∀ (x : M), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ∃ (f : Partial seed), (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain = ⊤

Tactic:
refine ⟨f, Submodule.eq_top_iff'.mpr ?_⟩
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : IsMax f
⊢ ∀ (b : Partial seed), ¬f < b

Tactic:
rw [isMax_iff_forall_not_lt] at hf

Premises used: isMax_iff_forall_not_lt
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hf : ∀ (b : Partial seed), ¬f < b
contrapose! :
  ∀ (hx : ∃ (x : M), x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain), ∃ (b : Partial seed), f < b
⊢ ∀ (x : M), x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
contrapose! hf with hx
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
hx : ∃ (x : M), x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
obtain : ∀ (x : M) (hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain), ∃ (b : Partial seed), f < b
⊢ ∃ (b : Partial seed), f < b

Tactic:
obtain ⟨x, hx⟩ := hx
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ∃ (b : Partial seed), f < b

Tactic:
⟨f.extend hx, f.lt_extend hx⟩

Premises used: HahnEmbedding.Partial.lt_extend, Exists.intro, HahnEmbedding.Partial.extend
-- 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
inst_12 : IsOrderedAddMonoid R
inst_13 : Archimedean R
f : Partial seed
x : M
hx : x ∉ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ ∃ (b : Partial seed), f < b

Tactic:
exact ⟨f.extend hx, f.lt_extend hx⟩