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
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
⊢ 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
-- 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
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))
⊢ (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a))
          (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty)) :
      M) ≠
    0

Tactic:
simpa using f.support.min'_mem hnonempty

Premises used: Finset.min'_mem, DFinsupp.support
-- 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
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))
pos :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty ≠
    FiniteArchimedeanClass.mk a h0
⊢ 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 [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]

Premises used: FiniteArchimedeanClass.val_mk, HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum, ArchimedeanClass.mk_sum, Subtype.coe_ne_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
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))
pos :
  ∀
    (this :
      f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
        FiniteArchimedeanClass.mk a h0),
    False
⊢ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty ≠
    FiniteArchimedeanClass.mk a h0

Tactic:
by_contra!
-- 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
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
⊢ 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
-- 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
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))
pos :
  ∀ (h : True),
    FiniteArchimedeanClass.mk a h0 ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
⊢ False

Tactic:
contrapose! 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
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
⊢ ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)

Tactic:
have := u.archimedeanClassMk_of_mem_stratum ha 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
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_1 :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
h : True
this : ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)
⊢ FiniteArchimedeanClass.mk a h0 = c

Tactic:
rw [← val_mk h0, ← Subtype.ext_iff] at this

Premises used: FiniteArchimedeanClass.val_mk, Subtype.ext_iff
-- 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
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_1 :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
h : True
this : FiniteArchimedeanClass.mk a h0 = c
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))

Tactic:
simpa [DFinsupp.notMem_support_iff, this] using (f c).prop

Premises used: DFinsupp.notMem_support_iff, Subtype.prop, DFunLike.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
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)) = ∅
neg :
  Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk (∑ 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:
rw [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
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)) = ∅
neg :
  Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
    (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
⊢ Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
    (ArchimedeanClass.mk a)

Tactic:
symm
-- 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)) = ∅
⊢ Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
    (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))

Tactic:
simpa using 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
apply :
  iSupIndep (α := (↑(Set.Iic u.baseDomain) : Type u_2))
    ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum')
⊢ iSupIndep u.stratum'

Tactic:
apply (iSupIndep_map_orderIso_iff (Submodule.mapIic u.baseDomain)).mp

Premises used: Submodule.mapIic, Iff.mp, iSupIndep_map_orderIso_iff, HahnEmbedding.ArchimedeanStrata.baseDomain
-- 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
ht :
  iSupIndep (α := Submodule K M)
    (Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum'))
⊢ iSupIndep (α := (↑(Set.Iic u.baseDomain) : Type u_2))
    ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum')

Tactic:
apply iSupIndep.of_coe_Iic_comp

Premises used: iSupIndep.of_coe_Iic_comp
-- 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
⊢ iSupIndep u.stratum

Tactic:
u.iSupIndep_stratum

Premises used: HahnEmbedding.ArchimedeanStrata.iSupIndep_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
h :
  Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') =
    u.stratum
⊢ iSupIndep (α := Submodule K M)
    (Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum'))

Tactic:
convert! u.iSupIndep_stratum

Premises used: HahnEmbedding.ArchimedeanStrata.iSupIndep_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
h :
  ∀ (c : FiniteArchimedeanClass M),
    Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
        (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
        ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum')
        c =
      u.stratum c
⊢ Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') =
    u.stratum

Tactic:
ext1 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') c =
    u.stratum c

Tactic:
simpa using le_iSup _ _

Premises used: le_iSup