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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : (∃ (m : ℕ), |(↑b : M)| ≤ m • |(↑a : M)|) ∧ ∃ (n : ℕ), |(↑a : M)| ≤ n • |(↑b : M)|
⊢ (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|

Tactic:
exact this
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
h : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑a : M)) (ArchimedeanClass.mk (↑b : M))
⊢ Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)

Tactic:
suffices ArchimedeanClass.mk a.val = ArchimedeanClass.mk b.val by
    rw [ArchimedeanClass.mk_eq_mk] at this ⊢
    exact this
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ (↑a : M) ≠ 0

Tactic:
simpa using ha
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
h : (↑c : ArchimedeanClass M) = ArchimedeanClass.mk (↑b : M)
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑a : M)) (ArchimedeanClass.mk (↑b : M))

Tactic:
rw [u.archimedeanClassMk_of_mem_stratum a.prop (by simpa using ha)]

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ (↑b : M) ≠ 0

Tactic:
simpa using hb
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
h h₁ : (↑c : ArchimedeanClass M) = (↑c : ArchimedeanClass M)
⊢ (↑c : ArchimedeanClass M) = ArchimedeanClass.mk (↑b : M)

Tactic:
rw [u.archimedeanClassMk_of_mem_stratum b.prop (by simpa using hb)]

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
rw :
  ∀ x ∈ u.stratum c,
    ∀ (y : M),
      Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) y →
        x = y → x = 0
⊢ Disjoint (u.stratum c) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j)

Tactic:
rw [Submodule.disjoint_def']

Premises used: Submodule.disjoint_def'
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
obtain :
  ∀ (f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i))
    (hf :
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
          fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
        b),
    a = 0
⊢ a = 0

Tactic:
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb

Premises used: Iff.mp, Submodule.mem_iSup_iff_exists_dfinsupp'
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
⊢ Eq (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
        fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)))
    (ArchimedeanClass.mk b)

Tactic:
obtain hf' := congr(ArchimedeanClass.mk $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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
hf' :
  Eq (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
        fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)))
    (ArchimedeanClass.mk b)
contrapose! :
  ∀ (h0 : a ≠ 0),
    Ne (α := ArchimedeanClass M)
      (ArchimedeanClass.mk
        (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
          fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)))
      (ArchimedeanClass.mk b)
⊢ a = 0

Tactic:
contrapose! hf' with h0
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
rw :
  Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (∑ i ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)),
        (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
    (ArchimedeanClass.mk a)
⊢ Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
        fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)))
    (ArchimedeanClass.mk b)

Tactic:
rw [← hab, DFinsupp.sum]

Premises used: DFinsupp.sum
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
pos :
  ∀ (hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty),
    Ne (α := ArchimedeanClass M)
      (ArchimedeanClass.mk
        (∑ i ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)),
          (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
      (ArchimedeanClass.mk a)
neg :
  ∀ (hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)) = ∅),
    Ne (α := ArchimedeanClass M)
      (ArchimedeanClass.mk
        (∑ i ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)),
          (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
      (ArchimedeanClass.mk a)
⊢ Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (∑ i ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)),
        (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
    (ArchimedeanClass.mk a)

Tactic:
by_cases! hnonempty : f.support.Nonempty

Premises used: DFinsupp.support, Finset.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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
x : FiniteArchimedeanClass M
⊢ (↑(⨆ (_ : x ≠ c), u.stratum x) : Set M) ⊆ (↑(u.stratum x) : Set 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
⊢ ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x

Tactic:
have hmem (x : FiniteArchimedeanClass M) : (f x).val ∈ u.stratum x :=
      Set.mem_of_mem_of_subset (f x).prop (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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
⊢ (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ≠ 0

Tactic:
simpa 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
rw :
  (↑x : ArchimedeanClass M) <
    ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) y) : M)
⊢ LT.lt (α := ArchimedeanClass M)
    (ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M))
    (ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) y) : M))

Tactic:
rw [u.archimedeanClassMk_of_mem_stratum (hmem x) (by simpa using hx)]

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
⊢ (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) y) : M) ≠ 0

Tactic:
simpa using hy
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
rw : (↑x : ArchimedeanClass M) < (↑y : ArchimedeanClass M)
⊢ (↑x : ArchimedeanClass M) <
    ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) y) : M)

Tactic:
rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]

Premises used: HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
⊢ (↑x : ArchimedeanClass M) < (↑y : ArchimedeanClass M)

Tactic:
hxy
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx :
  x ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
y : FiniteArchimedeanClass M
hy :
  y ∈
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
hxy : x < y
⊢ (↑x : ArchimedeanClass M) < (↑y : ArchimedeanClass M)

Tactic:
exact hxy