Show most of not anomalous pair means commutative

OrderedSemigroups/Archimedean.lean

@@ -27,6 +27,10 @@ def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ (same_sign a b →
 class Archimedean (α : Type u) [OrderedSemigroup α] where
   arch : is_archimedean (α := α)
 
+theorem not_has_anomalous_not_pair (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : ¬anomalous_pair a b := by
+  simp at *
+  tauto
+
 end OrderedSemigroup
 
 section LinearOrderedCancelSemigroup
@@ -143,6 +147,94 @@ theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α))
     · exact neg_not_archimedean_anomalous_pair neg_a neg_b hab h
     · exact neg_not_archimedean_anomalous_pair' neg_a neg_b hab h
 
-theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by sorry
+theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
+    (h : a * b < b * a) : anomalous_pair (a*b) (b*a) := by
+  intro n
+  have : ∀n : ℕ+, (b*a)^n < (a*b)^(n+1) := by
+    intro n
+    calc
+      (b * a) ^ n < (b * a) ^ n * b := pos_right pos_b ((b * a) ^ n)
+      _           < a * (b * a) ^ n * b := mul_lt_mul_right' (pos_a ((b * a) ^ n)) b
+      _           = (a * b) ^ (n + 1) := Eq.symm split_first_and_last_factor_of_product
+  left
+  exact ⟨comm_swap_lt h n, this n⟩
+
+theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
+    (h : a * b < b * a) : anomalous_pair (b*a) (a*b) := by
+  intro n
+  have : ∀n : ℕ+, (a*b)^n >(b*a)^(n+1) := by
+    intro n
+    calc
+      (a * b) ^ n > (a * b) ^ n * a := neg_right neg_a ((a * b) ^ n)
+      _           > b * (a * b) ^ n * a := mul_lt_mul_right' (neg_b ((a * b) ^ n)) a
+      _           = (b * a) ^ (n + 1) := Eq.symm split_first_and_last_factor_of_product
+  right
+  exact ⟨comm_swap_lt h n, this n⟩
+
+theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
+    (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
+  rcases lt_trichotomy (a*b) (b*a) with h | h | h
+  · have : has_anomalous_pair (α := α) := by
+      use (a*b), (b*a)
+      exact pos_not_comm_anomalous_pair pos_a pos_b h
+    contradiction
+  · trivial
+  · have : has_anomalous_pair (α := α) := by
+      use (b*a), (a*b)
+      exact pos_not_comm_anomalous_pair pos_b pos_a h
+    contradiction
+
+theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
+    (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
+  rcases lt_trichotomy (a*b) (b*a) with h | h | h
+  · have : has_anomalous_pair (α := α) := by
+      use (b*a), (a*b)
+      exact neg_not_comm_anomalous_pair neg_a neg_b h
+    contradiction
+  · trivial
+  · have : has_anomalous_pair (α := α) := by
+      use (a*b), (b*a)
+      exact neg_not_comm_anomalous_pair neg_b neg_a h
+    contradiction
+
+theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by
+  rcases pos_neg_or_one a with pos_a | neg_a | one_a
+  <;> rcases pos_neg_or_one b with pos_b | neg_b | one_b
+  all_goals try simp [one_b a, one_right one_b a]
+  all_goals try simp [one_a b, one_right one_a b]
+  · exact pos_not_anomalous_comm pos_a pos_b not_anomalous
+  · rcases pos_neg_or_one (a*b) with pos_ab | neg_ab | one_ab
+    · sorry
+    · sorry
+    · have : is_one (b * a) := by
+        apply one_right_one_forall (b := a)
+        rw [Eq.symm (mul_assoc a b a)]
+        exact one_ab a
+      exact one_unique one_ab this
+  · rcases pos_neg_or_one (b*a) with pos_ba | neg_ba | one_ba
+    have := pos_not_anomalous_comm pos_ba pos_b not_anomalous
+    · rcases lt_trichotomy (a*b) (b*a) with h | h | h
+      · have : a * b * a * b > a * b * a * b := calc
+          a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
+          _             = a * (b * (b * a)) := by simp [←this]
+          _             = (a * b) * (b * a) := by simp [mul_assoc]
+          _             > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
+          _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+        exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+      · trivial
+      · have : a * b * a * b > a * b * a * b := calc
+          a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
+          _             = a * (b * (b * a)) := by simp [←this]
+          _             = (a * b) * (b * a) := by simp [mul_assoc]
+          _             < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
+          _             = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
+        exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
+    · sorry
+    · have : is_one (a * b) := by
+        apply one_right_one_forall (b := b)
+        rw [Eq.symm (mul_assoc b a b)]
+        exact one_ba b
+      exact one_unique this one_ba
+  · exact neg_not_anomalous_comm neg_a neg_b not_anomalous
 
 end LinearOrderedCancelSemigroup

OrderedSemigroups/Basic.lean

@@ -55,8 +55,7 @@ variable [OrderedSemigroup α]
 theorem le_pow {a b : α} (h : a ≤ b) (n : ℕ+) : a^n ≤ b^n := by
   induction n using PNat.recOn with
   | p1 =>
-    simp
-    assumption
+    simpa
   | hp n ih =>
     simp [ppow_succ]
     exact mul_le_mul' ih h
@@ -77,9 +76,9 @@ theorem comm_factor_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : a^n * b^n ≤ (
       _                 ≤ a * (b * a)^n * b := middle_swap (le_pow h n)
       _                 = (a * b)^(n+1) := by rw [←split_first_and_last_factor_of_product]
 
-theorem comm_swap_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (a*b)^n ≤ (b*a)^n := le_pow h n
+theorem comm_swap_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (a*b)^n ≤ (b*a)^n := le_pow h n
 
-theorem comm_dist_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (b*a)^n ≤ b^n * a^n := by
+theorem comm_dist_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (b*a)^n ≤ b^n * a^n := by
   induction n using PNat.recOn with
   | p1 => simp
   | hp n ih =>
@@ -91,3 +90,29 @@ theorem comm_dist_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ
       _           = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ']
 
 end OrderedSemigroup
+
+section OrderedCancelSemigroup
+variable [OrderedCancelSemigroup α]
+
+theorem lt_pow {a b : α} (h : a < b) (n : ℕ+) : a^n < b^n := by
+  induction n using PNat.recOn with
+  | p1 => simpa
+  | hp n ih =>
+    simp [ppow_succ]
+    exact Left.mul_lt_mul ih h
+
+theorem comm_swap_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : (a*b)^n < (b*a)^n := lt_pow h n
+
+/-
+theorem comm_dist_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : n > 1 → (b*a)^n < b^n * a^n := by
+  induction n using PNat.recOn with
+  | p1 => intro; contradiction
+  | hp n ih =>
+    calc
+      (b*a)^(n+1) = b * (a*b)^n * a := by rw [split_first_and_last_factor_of_product]
+      _           ≤ b * (b*a)^n * a := middle_swap (le_pow h n)
+      _           ≤ b * (b^n * a^n) * a := middle_swap ih
+      _           = (b * b^n) * (a^n * a) := by simp [mul_assoc]
+      _           = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ']-/
+
+end OrderedCancelSemigroup

OrderedSemigroups/Sign.lean

@@ -186,4 +186,7 @@ theorem pos_le_pow_pos {a b : α} (pos : is_positive a) (n : ℕ+) (h : a ≤ b^
 theorem pow_le_neg_neg {a b : α} (neg : is_negative a) (n : ℕ+) (h : b^n ≤ a) : is_negative b :=
   pow_neg_neg n (le_neg_neg neg h)
 
+theorem one_unique {a b : α} (one_a : is_one a) (one_b : is_one b) : a = b := by
+  rw [←one_right one_b a, one_a b]
+
 end LinearOrderedCancelSemigroup