State that archimedean semigroup leads to archimedean monoid

OrderedSemigroups/Archimedean.lean

@@ -78,7 +78,7 @@ theorem anomalous_not_one' {a b : α} (anomalous : anomalous_pair a b) : ¬is_on
       simpa [←ppow_two a]
     have : is_negative b := le_neg_neg this b_lt_ap1.le
     exact False.elim (neg_not_one this one_b)
-  · have : is_positive b := pos_gt_one one_a a_lt_b
+  · have : is_positive b := gt_one_pos one_a a_lt_b
     exact False.elim (pos_not_one this one_b)
   · exact (lt_self_iff_false b).mp (gt_trans b_gt_ap1 (gt_trans (pos_a a) a_gt_b))
   · exact one_not_neg one_b (le_neg_neg neg_a (a_gt_b.le))

OrderedSemigroups/SemigroupToMonoid.lean

@@ -1,5 +1,5 @@
 import Mathlib.Algebra.Order.Group.Basic
-import OrderedSemigroups.Sign
+import OrderedSemigroups.Archimedean
 
 universe u
 variable {α : Type u}
@@ -57,7 +57,8 @@ end CommSemigroup'
 section LinearOrderedCancelSemigroup
 variable [LinearOrderedCancelCommSemigroup α]
 
-instance (not_one : ∀x : α, ¬is_one x): OrderedCommMonoid (with_one α) where
+set_option maxHeartbeats 300000
+instance to_monoid (not_one : ∀x : α, ¬is_one x) : LinearOrderedCancelCommMonoid (with_one α) where
   le := by
     intro x y
     rcases x with x | _
@@ -69,13 +70,13 @@ instance (not_one : ∀x : α, ¬is_one x): OrderedCommMonoid (with_one α) wher
   le_refl := by
     intro x
     rcases x with x | _
-    <;> simp
+    <;> simp only [le_refl]
   le_trans := by
     intro x y z x_le_y y_le_z
     rcases x with x | one
     <;> rcases y with y | one
     <;> rcases z with z | one
-    <;> simp at *
+    <;> simp only [ge_iff_le] at *
     · exact Preorder.le_trans x y z x_le_y y_le_z
     · rw [←not_pos_iff]
       exact le_not_pos_not_pos (not_pos_iff.mpr y_le_z) x_le_y
@@ -88,7 +89,7 @@ instance (not_one : ∀x : α, ¬is_one x): OrderedCommMonoid (with_one α) wher
     intro x y x_le_y y_le_x
     rcases x with x | one
     <;> rcases y with y | one
-    <;> simp at *
+    <;> simp only [ge_iff_le, reduceCtorEq] at *
     · rw [PartialOrder.le_antisymm x y x_le_y y_le_x]
     · exact not_one x (one_right_one_forall (PartialOrder.le_antisymm (x*x) x x_le_y y_le_x))
     · exact not_one y (one_right_one_forall (PartialOrder.le_antisymm (y*y) y y_le_x x_le_y))
@@ -98,14 +99,54 @@ instance (not_one : ∀x : α, ¬is_one x): OrderedCommMonoid (with_one α) wher
     <;> rcases y with y | one
     <;> rcases z with z | one
     <;> unfold_projs
-    <;> simp at *
+    <;> simp only [ge_iff_le, le_refl] at *
     · exact mul_le_mul_left' x_le_y z
     · trivial
     · exact not_pos_right (not_pos_iff.mpr x_le_y) z
     · exact x_le_y
     · exact not_neg_right (not_neg_iff.mpr x_le_y) z
     · trivial
+  le_total := by
+    intro x y
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> simp only [ge_iff_le, or_self] at *
+    · exact LinearOrder.le_total x y
+    · exact LinearOrder.le_total (x * x) x
+    · exact LinearOrder.le_total y (y * y)
+  decidableLE := by
+    simp [DecidableRel]
+    intro x y
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> simp at *
+    · exact instDecidableLe_mathlib x y
+    · exact instDecidableLe_mathlib (x * x) x
+    · exact instDecidableLe_mathlib y (y * y)
+    · exact instDecidableTrue
+  le_of_mul_le_mul_left := by
+    intro x y z xy_le_xz
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> rcases z with z | one
+    <;> unfold_projs at *
+    <;> simp only [ge_iff_le] at *
+    · exact (mul_le_mul_iff_left x).mp xy_le_xz
+    · exact not_pos_iff.1 (not_pos_right_not_pos xy_le_xz)
+    · exact not_neg_iff.1 (not_neg_right_not_neg xy_le_xz)
+    all_goals exact xy_le_xz
+
+instance {β : Type*} [Semigroup β] : Semigroup' β where
+
+instance {β : Type*} [OrderedCommMonoid β] : OrderedSemigroup β where
+  mul_le_mul_left := fun _ _ a_1 c ↦ mul_le_mul_left' a_1 c
+  mul_le_mul_right := fun _ _ a_1 c ↦ mul_le_mul_right' a_1 c
+
+instance toOrderedSemigroup {β : Type*} (_ : LinearOrderedCancelCommMonoid β) : OrderedSemigroup β :=
+  inferInstance
 
+theorem arch_semigroup_arch_monoid (not_one : ∀x : α, ¬is_one x) (arch : is_archimedean (α := α)) :
+    @is_archimedean (with_one α) (toOrderedSemigroup (to_monoid not_one)) := sorry
 
 
 end LinearOrderedCancelSemigroup

OrderedSemigroups/Sign.lean

@@ -257,17 +257,31 @@ theorem not_neg_iff {a : α} : ¬is_negative a ↔ a ≤ a * a := by
     simp [is_negative]
     use a
 
-theorem not_pos_or {a : α} (not_pos : ¬is_positive a) : is_negative a ∨ is_one a := by
-  obtain pos | neg | one := pos_neg_or_one a
-  · contradiction
-  · exact Or.symm (Or.inr neg)
-  · exact Or.inr one
+theorem not_pos_or {a : α} : ¬is_positive a ↔ is_negative a ∨ is_one a := by
+  constructor
+  · intro not_pos
+    obtain pos | neg | one := pos_neg_or_one a
+    · contradiction
+    · exact Or.symm (Or.inr neg)
+    · exact Or.inr one
+  · intro neg_or_one
+    rw [not_pos_iff]
+    obtain neg | one := neg_or_one
+    · exact le_of_lt (neg a)
+    · exact le_of_eq (one a)
 
-theorem not_neg_or {a : α} (not_neg : ¬is_negative a) : is_positive a ∨ is_one a := by
-  obtain pos | neg | one := pos_neg_or_one a
-  · exact Or.symm (Or.inr pos)
-  · contradiction
-  · exact Or.inr one
+theorem not_neg_or {a : α} : ¬is_negative a ↔ is_positive a ∨ is_one a := by
+  constructor
+  · intro not_neg
+    obtain pos | neg | one := pos_neg_or_one a
+    · exact Or.symm (Or.inr pos)
+    · contradiction
+    · exact Or.inr one
+  · intro pos_or_one
+    rw [not_neg_iff]
+    obtain pos | one := pos_or_one
+    · exact le_of_lt (pos a)
+    · exact Eq.ge (one a)
 
 theorem le_not_pos_not_pos {a b : α} (not_pos : ¬is_positive a) (h : b ≤ a) : ¬is_positive b := by
   obtain h | h := eq_or_lt_of_le h
@@ -290,36 +304,52 @@ theorem ge_not_neg_not_neg {a b : α} (not_neg : ¬is_negative a) (h : a ≤ b)
   · exact pos_not_neg (gt_one_pos one h)
 
 theorem not_pos_le_not_neg {a b : α} (not_pos : ¬is_positive a) (not_neg : ¬is_negative b) : a ≤ b := by
-  obtain neg_a | one_a := not_pos_or not_pos
-  <;> obtain pos_b | one_b := not_neg_or not_neg
+  obtain neg_a | one_a := not_pos_or.1 not_pos
+  <;> obtain pos_b | one_b := not_neg_or.1 not_neg
   · exact (neg_lt_pos neg_a pos_b).le
   · exact (neg_lt_one neg_a one_b).le
   · exact (one_lt_pos one_a pos_b).le
   · exact (one_unique one_a one_b).le
 
 theorem not_positive {a : α} (not_pos : ¬is_positive a) : ∀x : α, a * x ≤ x := by
   intro x
-  obtain neg_a | one_a := not_pos_or not_pos
+  obtain neg_a | one_a := not_pos_or.1 not_pos
   · exact le_of_lt (neg_a x)
   · exact le_of_eq (one_a x)
 
 theorem not_pos_right {a : α} (not_pos : ¬is_positive a) : ∀x : α, x * a ≤ x := by
   intro x
-  obtain neg_a | one_a := not_pos_or not_pos
+  obtain neg_a | one_a := not_pos_or.1 not_pos
   · exact le_of_lt (neg_right neg_a x)
   · exact le_of_eq (one_right one_a x)
 
 
 theorem not_negative {a : α} (not_neg : ¬is_negative a) : ∀x : α, a * x ≥ x := by
   intro x
-  obtain pos_a | one_a := not_neg_or not_neg
+  obtain pos_a | one_a := not_neg_or.1 not_neg
   · exact le_of_lt (pos_a x)
   · exact Eq.ge (one_a x)
 
 theorem not_neg_right {a : α} (not_neg : ¬is_negative a) : ∀x : α, x * a ≥ x := by
   intro x
-  obtain pos_a | one_a := not_neg_or not_neg
+  obtain pos_a | one_a := not_neg_or.1 not_neg
   · exact le_of_lt (pos_right pos_a x)
   · exact le_of_eq (one_right one_a x).symm
 
+theorem not_pos_right_not_pos {a b : α} (h : b * a ≤ b) : ¬is_positive a := by
+  rw [not_pos_or]
+  obtain lt | eq := h.lt_or_eq
+  · left
+    exact neg_right_neg_forall lt
+  · right
+    exact one_right_one_forall eq
+
+theorem not_neg_right_not_neg {a b : α} (h : b * a ≥ b) : ¬is_negative a := by
+  rw [not_neg_or]
+  obtain lt | eq := h.lt_or_eq
+  · left
+    exact pos_right_pos_forall lt
+  · right
+    exact one_right_one_forall eq.symm
+
 end LinearOrderedCancelSemigroup