refactor: make LinearOrderedCommMonoidWithZeros cancellative (leanprover-community#31749)

It appears that the only interesting `LinearOrderedCommMonoidWithZero`s are the ones for which every non-zero element is regular. This PR therefore strenghtens `LinearOrderedCommMonoidWithZero`, and similarly for `LinearOrderedAddCommMonoidWithTop`, its additive counterpart.

Here are the instances we lose:
* `ENNReal`: multiplication by `\top` isn't injective
* `ERealᵒᵈ`: multiplication by `\top` isn't injective
* `Cardinal`: multiplication by anything but 1 isn't injective
* `ArchimedeanClass R` where `R` is a non-strict ordered ring
* the pathological counterexample of a `LinearOrderedCommMonoidWithZero` where two positive numbers multiply to zero

I believe these are all fine to lose since they had no mathematical motivation (we never use those as targets of valuations).

There is an argument to be made that we could keep the existing typeclass as is and instead have the one I'm currently replacing it with under the name `LinearOrderedCancelCommMonoidWithZero`. There are at least two reasons I do not want to do this:
1. We have no evidence that the weaker typeclass is actually useful
2. `LinearOrderedCommMonoidWithZero`, weak or strong version, extends both the algebra and order hierarchy, which is something we want to move away from. Therefore, if anything, we should not be adding more of those typeclasses.

This will be used in a later PR to replace `pow_eq_one_iff` with `IsMulTorsionFree.pow_eq_one_iff_left`.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20linear.20ordered.20comm.20monoids.20with.20zero.20be.20torsion-free)

Author: YaelDillies

Counterexamples.lean

@@ -12,7 +12,6 @@ import Counterexamples.Girard
 import Counterexamples.HeawoodUnitDistance
 import Counterexamples.HomogeneousPrimeNotPrime
 import Counterexamples.IrrationalPowerOfIrrational
-import Counterexamples.LinearOrderWithPosMulPosEqZero
 import Counterexamples.MapFloor
 import Counterexamples.MonicNonRegular
 import Counterexamples.Motzkin

Counterexamples/LinearOrderWithPosMulPosEqZero.lean

@@ -9,7 +9,9 @@ public import Mathlib.Algebra.CharZero.Defs
 public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 public import Mathlib.Algebra.Order.Monoid.WithTop
+public import Mathlib.Algebra.Regular.Basic
 
+import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.TermCongr
 
 /-!
@@ -37,16 +39,22 @@ class LinearOrderedAddCommMonoidWithTop (α : Type*) extends
     AddCommMonoid α, LinearOrder α, IsOrderedAddMonoid α, OrderTop α where
   /-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is invariant under addition. -/
   protected top_add' : ∀ x : α, ⊤ + x = ⊤
+  protected isAddLeftRegular_of_ne_top ⦃x : α⦄ : x ≠ ⊤ → IsAddLeftRegular x
 
 /-- A linearly ordered commutative group with an additively absorbing `⊤` element.
   Instances should include number systems with an infinite element adjoined. -/
-class LinearOrderedAddCommGroupWithTop (α : Type*) extends LinearOrderedAddCommMonoidWithTop α,
-  SubNegMonoid α, Nontrivial α where
+-- We do not extend `LinearOrderedAddCommMonoidWithTop` as that would bring in the unnecessary
+-- `isAddLeftRegular_of_ne_top` field.
+class LinearOrderedAddCommGroupWithTop (α : Type*)
+    extends AddCommMonoid α, LinearOrder α, IsOrderedAddMonoid α, OrderTop α, SubNegMonoid α,
+    Nontrivial α where
+  /-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is invariant under addition. -/
+  protected top_add' (x : α) : ⊤ + x = ⊤
   neg_top : -(⊤ : α) = ⊤
   add_neg_cancel_of_ne_top ⦃x : α⦄ : x ≠ ⊤ → x + -x = 0
 
 section LinearOrderedAddCommMonoidWithTop
-variable [LinearOrderedAddCommMonoidWithTop α]
+variable [LinearOrderedAddCommMonoidWithTop α] {a b c : α}
 
 @[simp]
 theorem top_add (a : α) : ⊤ + a = ⊤ :=
@@ -56,13 +64,52 @@ theorem top_add (a : α) : ⊤ + a = ⊤ :=
 theorem add_top (a : α) : a + ⊤ = ⊤ :=
   Trans.trans (add_comm _ _) (top_add _)
 
+@[simp] lemma IsAddRegular.of_ne_top (ha : a ≠ ⊤) : IsAddRegular a := by
+  simpa using LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top ha
+
+lemma add_left_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective (fun x ↦ x + b) :=
+  (IsAddRegular.of_ne_top h).2
+
+lemma add_right_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective (fun x ↦ b + x) :=
+  (IsAddRegular.of_ne_top h).1
+
+@[simp]
+lemma add_left_inj_of_ne_top (h : a ≠ ⊤) : b + a = c + a ↔ b = c :=
+  (add_left_injective_of_ne_top _ h).eq_iff
+
+@[simp]
+lemma add_right_inj_of_ne_top (h : a ≠ ⊤) : a + b = a + c ↔ b = c :=
+  (add_right_injective_of_ne_top _ h).eq_iff
+
+lemma add_left_strictMono_of_ne_top (h : b ≠ ⊤) : StrictMono (fun x ↦ x + b) :=
+  add_left_mono.strictMono_of_injective <| add_left_injective_of_ne_top _ h
+
+lemma add_right_strictMono_of_ne_top (h : b ≠ ⊤) : StrictMono (fun x ↦ b + x) :=
+  add_right_mono.strictMono_of_injective <| add_right_injective_of_ne_top _ h
+
+@[simp]
+lemma add_le_add_iff_left_of_ne_top (h : a ≠ ⊤) : b + a ≤ c + a ↔ b ≤ c :=
+  (add_left_strictMono_of_ne_top h).le_iff_le
+
+@[simp]
+lemma add_le_add_iff_right_of_ne_top (h : a ≠ ⊤) : a + b ≤ a + c ↔ b ≤ c :=
+  (add_right_strictMono_of_ne_top h).le_iff_le
+
+@[simp]
+lemma add_lt_add_iff_left_of_ne_top (h : a ≠ ⊤) : b + a < c + a ↔ b < c :=
+  (add_left_strictMono_of_ne_top h).lt_iff_lt
+
+@[simp]
+lemma add_lt_add_iff_right_of_ne_top (h : a ≠ ⊤) : a + b < a + c ↔ b < c :=
+  (add_right_strictMono_of_ne_top h).lt_iff_lt
+
 end LinearOrderedAddCommMonoidWithTop
 
 namespace LinearOrderedAddCommGroupWithTop
 
-variable [LinearOrderedAddCommGroupWithTop α] {a b : α}
+variable [LinearOrderedAddCommGroupWithTop α] {a b c : α}
 
-attribute [simp] LinearOrderedAddCommGroupWithTop.neg_top
+attribute [simp] neg_top
 
 @[deprecated (since := "2025-12-14")] protected alias add_neg_cancel := add_neg_cancel_of_ne_top
 
@@ -87,29 +134,19 @@ lemma neg_add_cancel_right_of_ne_top (hb : b ≠ ⊤) (a : α) : a + -b + b = a
   intro h
   obtain ⟨a, ha⟩ := exists_ne (0 : α)
   rw [← zero_add a] at ha
-  simp [top_add, -zero_add, ← h] at ha
+  simp [LinearOrderedAddCommGroupWithTop.top_add', -zero_add, ← h] at ha
 
 @[simp] lemma zero_ne_top : 0 ≠ (⊤ : α) := top_ne_zero.symm
 
 @[simp] lemma top_pos : (0 : α) < ⊤ := lt_top_iff_ne_top.2 top_ne_zero.symm
 
-@[simp]
-lemma add_neg_cancel_iff_ne_top : a + -a = 0 ↔ a ≠ ⊤ where
-  mp := by contrapose; simp +contextual
-  mpr h := add_neg_cancel_of_ne_top h
-
-@[simp]
-lemma sub_self_eq_zero_iff_ne_top : a - a = 0 ↔ a ≠ ⊤ := by
-  rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]
-
-alias ⟨_, sub_self_eq_zero_of_ne_top⟩ := sub_self_eq_zero_iff_ne_top
-
 @[simp] lemma isAddUnit_iff : IsAddUnit a ↔ a ≠ ⊤ where
-  mp := by rintro ⟨⟨b, c, hbc, -⟩, rfl⟩ rfl; simp [top_add] at hbc
+  mp := by rintro ⟨⟨b, c, hbc, -⟩, rfl⟩ rfl; simp [LinearOrderedAddCommGroupWithTop.top_add'] at hbc
   mpr ha := .of_add_eq_zero (-a) <| by simp [ha, add_neg_cancel_of_ne_top]
 
 instance : LinearOrderedAddCommMonoidWithTop α where
-  top_add' := top_add
+  top_add' := LinearOrderedAddCommGroupWithTop.top_add'
+  isAddLeftRegular_of_ne_top _a ha := (isAddUnit_iff.2 ha).isAddRegular.1
 
 lemma add_ne_top : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤ := by simp [← isAddUnit_iff]
 
@@ -140,92 +177,67 @@ instance (priority := 100) toSubtractionMonoid : SubtractionMonoid α where
     have ha : a ≠ ⊤ := by rintro rfl; simp at h
     exact left_neg_eq_right_neg (a := a) (by simp [neg_add_cancel_of_ne_top, *]) h
 
-lemma add_left_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective fun x ↦ x + b :=
-  fun x y hxy ↦ by simpa [h] using congr($hxy - b)
-
 @[deprecated (since := "2025-12-27")]
 alias injective_add_left_of_ne_top := add_left_injective_of_ne_top
 
-lemma add_right_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective fun x ↦ b + x := by
-  simpa [add_comm] using add_left_injective_of_ne_top b h
-
 @[deprecated (since := "2025-12-27")]
 alias injective_add_right_of_ne_top := add_right_injective_of_ne_top
 
-@[simp]
-lemma add_left_inj_of_ne_top {a b c : α} (h : a ≠ ⊤) : b + a = c + a ↔ b = c :=
-  (add_left_injective_of_ne_top _ h).eq_iff
-
-@[simp]
-lemma add_right_inj_of_ne_top {a b c : α} (h : a ≠ ⊤) : a + b = a + c ↔ b = c :=
-  (add_right_injective_of_ne_top _ h).eq_iff
-
-lemma sub_left_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective fun x ↦ x - b := by
+lemma sub_left_injective_of_ne_top (h : b ≠ ⊤) : Function.Injective fun x ↦ x - b := by
   simpa [sub_eq_add_neg] using add_left_injective_of_ne_top (-b) (by simpa)
 
-lemma sub_right_injective_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective fun x ↦ b - x := by
+lemma sub_right_injective_of_ne_top (h : b ≠ ⊤) : Function.Injective fun x ↦ b - x := by
   simpa [sub_eq_add_neg] using (add_right_injective_of_ne_top b h).comp neg_injective
 
 @[simp]
-lemma sub_left_inj_of_ne_top {a b c : α} (h : a ≠ ⊤) : b - a = c - a ↔ b = c :=
-  (sub_left_injective_of_ne_top _ h).eq_iff
+lemma sub_left_inj_of_ne_top (h : a ≠ ⊤) : b - a = c - a ↔ b = c :=
+  (sub_left_injective_of_ne_top h).eq_iff
 
 @[simp]
-lemma sub_right_inj_of_ne_top {a b c : α} (h : a ≠ ⊤) : a - b = a - c ↔ b = c :=
-  (sub_right_injective_of_ne_top _ h).eq_iff
-
-lemma add_left_strictMono_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono fun x ↦ x + b :=
-  (Monotone.add_const monotone_id _).strictMono_of_injective (add_left_injective_of_ne_top _ h)
+lemma sub_right_inj_of_ne_top (h : a ≠ ⊤) : a - b = a - c ↔ b = c :=
+  (sub_right_injective_of_ne_top h).eq_iff
 
 @[deprecated (since := "2025-12-27")]
 alias strictMono_add_left_of_ne_top := add_left_strictMono_of_ne_top
 
-lemma add_right_strictMono_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono fun x ↦ b + x := by
-  simpa [add_comm] using add_left_strictMono_of_ne_top b h
-
 @[deprecated (since := "2025-12-27")]
 alias strictMono_add_right_of_ne_top := add_right_strictMono_of_ne_top
 
-@[simp]
-lemma add_le_add_iff_left_of_ne_top {a b c : α} (h : a ≠ ⊤) : b + a ≤ c + a ↔ b ≤ c :=
-  (add_left_strictMono_of_ne_top _ h).le_iff_le
+lemma sub_left_strictMono_of_ne_top (h : b ≠ ⊤) : StrictMono fun x ↦ x - b := by
+  simpa [sub_eq_add_neg] using add_left_strictMono_of_ne_top (b := -b) (by simpa)
 
 @[simp]
-lemma add_le_add_iff_right_of_ne_top {a b c : α} (h : a ≠ ⊤) : a + b ≤ a + c ↔ b ≤ c :=
-  (add_right_strictMono_of_ne_top _ h).le_iff_le
+lemma sub_le_sub_iff_left_of_ne_top (h : a ≠ ⊤) : b - a ≤ c - a ↔ b ≤ c :=
+  (sub_left_strictMono_of_ne_top h).le_iff_le
 
 @[simp]
-lemma add_lt_add_iff_left_of_ne_top {a b c : α} (h : a ≠ ⊤) : b + a < c + a ↔ b < c :=
-  (add_left_strictMono_of_ne_top _ h).lt_iff_lt
+lemma sub_lt_sub_iff_left_of_ne_top (h : a ≠ ⊤) : b - a < c - a ↔ b < c :=
+  (sub_left_strictMono_of_ne_top h).lt_iff_lt
 
 @[simp]
-lemma add_lt_add_iff_right_of_ne_top {a b c : α} (h : a ≠ ⊤) : a + b < a + c ↔ b < c :=
-  (add_right_strictMono_of_ne_top _ h).lt_iff_lt
-
-lemma sub_left_strictMono_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono fun x ↦ x - b := by
-  simpa [sub_eq_add_neg] using add_left_strictMono_of_ne_top (-b) (by simpa)
+lemma add_neg_cancel_iff_ne_top : a + -a = 0 ↔ a ≠ ⊤ where
+  mp := by contrapose; simp +contextual
+  mpr h := add_neg_cancel_of_ne_top h
 
 @[simp]
-lemma sub_le_sub_iff_left_of_ne_top {a b c : α} (h : a ≠ ⊤) : b - a ≤ c - a ↔ b ≤ c :=
-  (sub_left_strictMono_of_ne_top _ h).le_iff_le
+lemma sub_self_eq_zero_iff_ne_top : a - a = 0 ↔ a ≠ ⊤ := by
+  rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]
 
-@[simp]
-lemma sub_lt_sub_iff_left_of_ne_top {a b c : α} (h : a ≠ ⊤) : b - a < c - a ↔ b < c :=
-  (sub_left_strictMono_of_ne_top _ h).lt_iff_lt
+alias ⟨_, sub_self_eq_zero_of_ne_top⟩ := sub_self_eq_zero_iff_ne_top
 
-lemma sub_pos (a b : α) : 0 < a - b ↔ b < a ∨ b = ⊤ := by
+lemma sub_pos : 0 < a - b ↔ b < a ∨ b = ⊤ := by
   obtain rfl | hb := eq_or_ne b ⊤
   · simp
-  · rw [← sub_self_eq_zero_of_ne_top hb]
-    simp [hb]
+  · simp [← sub_self_eq_zero_of_ne_top hb, hb]
 
 end LinearOrderedAddCommGroupWithTop
 
 namespace WithTop
 
-instance linearOrderedAddCommMonoidWithTop [AddCommMonoid α] [LinearOrder α]
+instance linearOrderedAddCommMonoidWithTop [AddCancelCommMonoid α] [LinearOrder α]
     [IsOrderedAddMonoid α] : LinearOrderedAddCommMonoidWithTop (WithTop α) where
   top_add' := WithTop.top_add
+  isAddLeftRegular_of_ne_top _a ha _b _c := WithTop.add_left_cancel ha
 
 namespace LinearOrderedAddCommGroup
 variable [AddCommGroup G] {x y : WithTop G}
@@ -254,6 +266,7 @@ instance instSub : Sub (WithTop G) where
   cases x <;> cases y <;> simp [← coe_sub]
 
 instance [LinearOrder G] [IsOrderedAddMonoid G] : LinearOrderedAddCommGroupWithTop (WithTop G) where
+  __ := WithTop.linearOrderedAddCommMonoidWithTop
   sub_eq_add_neg a b := by cases a <;> cases b <;> simp [← coe_sub, ← coe_neg, sub_eq_add_neg]
   neg_top := WithTop.map_top _
   zsmul := zsmulRec

Mathlib/Algebra/Order/AddGroupWithTop.lean

@@ -23,8 +23,10 @@ abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero α where
   bot := 0
   bot_le := zero_le
-  zero_le_one := zero_le_one
-  mul_le_mul_left _ _ h _ := by grw [h]
+  zero_le := zero_le
+  mul_lt_mul_of_pos_left _a ha _b _c hbc :=
+    have : PosMulStrictMono α := PosMulReflectLT.toPosMulStrictMono _
+    mul_lt_mul_of_pos_left hbc ha
 
 variable [IsStrictOrderedRing α] [Sub α] [OrderedSub α]