awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Disjoint (u.stratum c) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j)
have 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
Tactic: rw [Submodule.disjoint_def']
-- 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
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
⊢ a = 0
have 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
Tactic: obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb
-- 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
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
⊢ a = 0
have 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)
Tactic: obtain hf' := congr(ArchimedeanClass.mk $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
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)
⊢ a = 0
have 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)
Tactic: contrapose! hf' with h0
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
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
⊢ 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)
have 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)
Tactic: rw [← hab, DFinsupp.sum]
-- 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
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
⊢ 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)
have 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)
Tactic: by_cases! hnonempty : f.support.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
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)
⊢ 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)
have 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)
Tactic: by_cases! hnonempty : f.support.Nonempty
-- 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
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
⊢ 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)
have hmem : ∀ (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)
-- 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
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
⊢ 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))
have rw : (↑x : ArchimedeanClass 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)]
-- 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
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) <
    ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) y) : M)
have rw : (↑x : ArchimedeanClass M) < (↑y : ArchimedeanClass M)
Tactic: rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]
-- 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
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
⊢ 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)
have hmono : StrictMonoOn (β := ArchimedeanClass M)
  (fun (i : FiniteArchimedeanClass M) ↦
    ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
  (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
    Set (FiniteArchimedeanClass M))
Tactic: have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support := by
      intro x hx y hy hxy
      change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val
      rw [u.archimedeanClassMk_of_mem_stratum (hmem x) (by simpa using hx)]
      rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]
      exact hxy
-- 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
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
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (i : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
⊢ 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)
have pos : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty ≠
  FiniteArchimedeanClass.mk a h0
Tactic: rw [ArchimedeanClass.mk_sum hnonempty hmono, u.archimedeanClassMk_of_mem_stratum (hmem _)
      (by simpa using f.support.min'_mem hnonempty), ← val_mk h0, Subtype.coe_ne_coe]
-- 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
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
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (i : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
this :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
⊢ False
have h : FiniteArchimedeanClass.mk a h0 ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
Tactic: obtain h := this ▸ Finset.min'_mem f.support hnonempty
-- 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
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
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (i : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
this :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
h : FiniteArchimedeanClass.mk a h0 ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
⊢ False
have pos : ∀ (h : True),
  FiniteArchimedeanClass.mk a h0 ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
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
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (i : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
this :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
h : True
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
have this₁ : ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)
Tactic: have := u.archimedeanClassMk_of_mem_stratum ha h0