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
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  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)))
    (↑(y - 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) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
hmono : StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
⊢ 0 = (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  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)))
    (↑(y - 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) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
hmono : StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
a :
  (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) 0 <
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
⊢ 0 <
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)

Tactic:
rw [show 0 = f 0 by simp]
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  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)))
    (↑(y - 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) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
hmono : StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
a : 0 < Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf
⊢ (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) 0 <
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)

Tactic:
apply hmono
-- 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)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  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)))
    (↑(y - 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) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
hmono : StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
a : (↑0 : M) < (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf) : M)
⊢ 0 < Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf

Tactic:
rw [← Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
inst_12 : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
x y : ↥(sSupFun (c := c) hc).domain
h : x < y
hyx :
  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)))
    (↑(y - 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) f
hf : (↑(y - x) : M) ∈ f.domain
this :
  (↑(sSupFun (c := c) hc) : ↥(sSupFun hc).domain → Lex R⟦FiniteArchimedeanClass M⟧) (y - x) =
    (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf)
f' : Partial seed
left : f' ∈ c
hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f
hmono : StrictMono (↑f : ↥f.domain → Lex R⟦FiniteArchimedeanClass M⟧)
⊢ (↑0 : M) < (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ f.domain) (↑(y - x) : M) hf) : M)

Tactic:
simp [h]
-- 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 : Set (Partial seed)
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
f : Partial seed
hf : f ∈ c
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ sSupFun (c := c) hc

Tactic:
LinearPMap.le_sSup _ <| (Set.mem_image _ _ _).mpr ⟨f, hf, rfl⟩

Premises used: Iff.mpr, Set.Mem, HahnEmbedding.Partial.sSupFun, Set.mem_image, And.intro, Exists.intro, LinearPMap.le_sSup, rfl
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
obtain : ∀ (f : Partial seed) (hf : f ∈ c), seed.baseEmbedding ≤ sSupFun (c := c) hc
⊢ seed.baseEmbedding ≤ sSupFun (c := c) hc

Tactic:
obtain ⟨f, hf⟩ := hnonempty
-- 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 : Set (Partial seed)
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
f : Partial seed
hf : f ∈ c
⊢ seed.baseEmbedding ≤ sSupFun (c := c) hc

Tactic:
le_trans f.prop.baseEmbedding_le (le_sSupFun hc hf)

Premises used: HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.le_sSupFun, Subtype.prop, le_trans
-- 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 : Set (Partial seed)
hc : DirectedOn (fun (x1 x2 : Partial seed) ↦ x1 ≤ x2) c
f : Partial seed
hf : f ∈ c
⊢ seed.baseEmbedding ≤ sSupFun (c := c) hc

Tactic:
exact le_trans f.prop.baseEmbedding_le (le_sSupFun hc hf)

Premises used: HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.le_sSupFun, Subtype.prop, le_trans
-- 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
⊢ (↑x : M) ∈ (sSupFun (c := c_1) hc).domain

Tactic:
obtain hx := x.prop

Premises used: Subtype.prop
-- 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)
⊢ ∀ ⦃x y : Partial seed⦄,
    x ≤ y → (↑x : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) ≤ (↑y : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
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)
obtain :
  ∀ (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),
    Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (sSupFun (c := c_1) hc).toFun.range
      ((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))) :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (sSupFun (c := c_1) hc).toFun.range
    ((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))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
obtain ⟨f, hmem, hf⟩ :=
    (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hx

Premises used: LinearPMap.mem_domain_sSup_iff, DirectedOn.mono_comp, Set.Nonempty.image, Iff.mp
-- 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
obtain :
  ∀ (f' : Partial seed) (hmem' : f' ∈ c_1) (hf' : (↑f' : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) = f),
    Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (sSupFun (c := c_1) hc).toFun.range
      ((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))) :
        Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) (sSupFun (c := c_1) hc).toFun.range
    ((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))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
obtain ⟨f', hmem', hf'⟩ := (Set.mem_image _ _ _).mp hmem

Premises used: Set.mem_image, Iff.mp
-- 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
⊢ Membership.mem (α := Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)) f.toFun.range
    ((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)))) :
      Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))

Tactic:
obtain h := (hf'.symm ▸ f'.prop.truncLT_mem_range) ⟨x, hf⟩ c
-- 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))))
apply : (↑f.domain : Set M) ⊆ (↑(sSupFun (c := c_1) hc).domain : Set M)
⊢ (↑x' : M) ∈ (sSupFun (c := c_1) hc).domain

Tactic:
apply Set.mem_of_mem_of_subset x'.prop

Premises used: Subtype.prop, Set.mem_of_mem_of_subset
-- 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:
hf'.symm ▸ (le_sSupFun hc hmem').1

Premises used: Eq.rec, HahnEmbedding.Partial.le_sSupFun, And.left, Eq.symm