feat: IsBotOneClass and IsBotZeroClass (leanprover-community#38730)

We create typeclasses expressing that `0` or `1` is a bottom element in a type. We use this to unify and generalize various theorems which are currently stated for canonically ordered monoids.

This has provisionally left us with a bunch of unnecessary aliases; these will be deprecated in a follow-up PR (tentatively leanprover-community#38663).

See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Typeclass.20for.20IsBot.200/near/586314552).

Author: vihdzp

Mathlib.lean

@@ -1007,6 +1007,7 @@ public import Mathlib.Algebra.Order.Interval.Set.Instances
 public import Mathlib.Algebra.Order.Interval.Set.Monoid
 public import Mathlib.Algebra.Order.Interval.Set.SuccPred
 public import Mathlib.Algebra.Order.Invertible
+public import Mathlib.Algebra.Order.IsBotOne
 public import Mathlib.Algebra.Order.Kleene
 public import Mathlib.Algebra.Order.Module.Algebra
 public import Mathlib.Algebra.Order.Module.Archimedean

Mathlib/Algebra/Order/Field/Canonical.lean

@@ -23,7 +23,7 @@ abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero α where
   bot := 0
   bot_le _ := zero_le
-  zero_le _ := zero_le
+  isBot_zero _ := 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

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -38,8 +38,7 @@ variable {α β : Type*}
 
 /-- A linearly ordered commutative monoid with a zero element. -/
 class LinearOrderedCommMonoidWithZero (α : Type*) extends CommMonoidWithZero α, LinearOrder α,
-    PosMulStrictMono α, OrderBot α where
-  protected zero_le (a : α) : 0 ≤ a
+    PosMulStrictMono α, OrderBot α, IsBotZeroClass α where
 
 /-- A linearly ordered commutative group with a zero element. -/
 class LinearOrderedCommGroupWithZero (α : Type*) extends LinearOrderedCommMonoidWithZero α,
@@ -52,20 +51,6 @@ variable [LinearOrderedCommMonoidWithZero α] {a b : α} {n : ℕ}
 The following facts are true more generally in a (linearly) ordered commutative monoid.
 -/
 
-@[simp] lemma zero_le' : 0 ≤ a := LinearOrderedCommMonoidWithZero.zero_le _
-@[simp] lemma not_lt_zero' : ¬a < 0 := zero_le'.not_gt
-@[simp] lemma le_zero_iff : a ≤ 0 ↔ a = 0 := by simp [le_antisymm_iff]
-
-lemma zero_lt_iff : 0 < a ↔ a ≠ 0 := by simp [lt_iff_le_and_ne, eq_comm]
-lemma ne_zero_of_lt (h : b < a) : a ≠ 0 := fun h1 ↦ not_lt_zero' <| show b < 0 from h1 ▸ h
-
-/-- See also `bot_eq_zero` and `bot_eq_zero'` for canonically ordered monoids. -/
-lemma bot_eq_zero'' : (⊥ : α) = 0 := eq_of_forall_ge_iff fun _ ↦ by simp
-
--- See note [lower instance priority]
-instance (priority := 100) LinearOrderedCommMonoidWithZero.toZeroLeOneClass : ZeroLEOneClass α where
-  zero_le_one := zero_le'
-
 -- See note [lower instance priority]
 instance (priority := 100) LinearOrderedCommMonoidWithZero.toMulPosStrictMono :
     MulPosStrictMono α := posMulStrictMono_iff_mulPosStrictMono.1 inferInstance
@@ -78,12 +63,12 @@ instance (priority := 100) LinearOrderedCommMonoidWithZero.toIsOrderedMonoid :
     · simp
     obtain rfl | hab := hab.eq_or_lt
     · simp
-    · exact (mul_lt_mul_of_pos_right hab <| zero_lt_iff.2 hc).le
+    · exact (mul_lt_mul_of_pos_right hab hc.pos).le
 
 -- See note [lower instance priority]
 instance (priority := 100) : IsCancelMulZero α where
-  mul_left_cancel_of_ne_zero ha := (strictMono_mul_left_of_pos <| zero_lt_iff.2 ha).injective
-  mul_right_cancel_of_ne_zero ha := (strictMono_mul_right_of_pos <| zero_lt_iff.2 ha).injective
+  mul_left_cancel_of_ne_zero ha := (strictMono_mul_left_of_pos ha.pos).injective
+  mul_right_cancel_of_ne_zero ha := (strictMono_mul_right_of_pos ha.pos).injective
 
 /-- Pullback a `LinearOrderedCommMonoidWithZero` under an injective map.
 See note [reducible non-instances]. -/
@@ -100,7 +85,7 @@ abbrev Function.Injective.linearOrderedCommMonoidWithZero {β : Type*} [Zero β]
   __ := hf.linearOrder f le lt hinf hsup compare
   __ := hf.commMonoidWithZero f zero one mul npow
   __ := Function.Injective.posMulStrictMono f zero mul lt
-  zero_le _ := le.1 <| zero ▸ zero_le'
+  isBot_zero _ := le.1 <| zero ▸ zero_le
   bot_le _ := le.1 <| bot ▸ bot_le
 
 instance (priority := 100) LinearOrderedCommMonoidWithZero.toIsMulTorsionFree :
@@ -109,17 +94,18 @@ instance (priority := 100) LinearOrderedCommMonoidWithZero.toIsMulTorsionFree :
 
 instance instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual :
     LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ) where
-  top_add' a := by ext; simp [bot_eq_zero'']
-  isAddLeftRegular_of_ne_top := by simp +contextual [IsRegular.of_ne_zero, bot_eq_zero'']
+  top_add' a := by ext; simp [bot_eq_zero]
+  isAddLeftRegular_of_ne_top := by simp +contextual [IsRegular.of_ne_zero, bot_eq_zero]
 
 instance instLinearOrderedAddCommMonoidWithTopOrderDualAdditive :
     LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ where
-  top_add' a := by ext; simp; simp [bot_eq_zero'' (α := α)]
-  isAddLeftRegular_of_ne_top := by simp; simp +contextual [bot_eq_zero'', IsRegular.of_ne_zero]
+  top_add' a := by ext; simp; simp [bot_eq_zero (α := α)]
+  isAddLeftRegular_of_ne_top := by simp; simp +contextual [bot_eq_zero, IsRegular.of_ne_zero]
 
 variable [NoZeroDivisors α]
 
-lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
+lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by
+  simp_rw [pos_iff_ne_zero, pow_ne_zero_iff hn]
 
 end LinearOrderedCommMonoidWithZero
 
@@ -128,35 +114,35 @@ variable [LinearOrderedCommGroupWithZero α] {a b c d : α} {m n : ℕ}
 
 @[simp]
 theorem Units.zero_lt (u : αˣ) : (0 : α) < u :=
-  zero_lt_iff.2 u.ne_zero
+  u.ne_zero.pos
 
 theorem mul_inv_lt_of_lt_mul₀ (h : a < b * c) : a * c⁻¹ < b := by
   contrapose! h
-  simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le' zero_le' h
+  simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le zero_le h
 
 theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c := by
   rw [mul_comm] at *
   exact mul_inv_lt_of_lt_mul₀ h
 
 theorem lt_of_mul_lt_mul_of_le₀ (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d := by
   have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
-  rw [← inv_le_inv₀ (zero_lt_iff.2 ha) hc] at hh
+  rw [← inv_le_inv₀ ha.pos hc] at hh
   simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
-    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le' (inv_pos.2 hc)
+    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh h zero_le (inv_pos.2 hc)
 
 instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) where
   top_add' := by simp
-  neg_top := by ext; simp [bot_eq_zero'']
+  neg_top := by ext; simp [bot_eq_zero]
   add_neg_cancel_of_ne_top := by
-    simp +contextual [bot_eq_zero'', Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
+    simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
       -ofDual_eq_zero]
 
 instance : LinearOrderedAddCommGroupWithTop (Additive α)ᵒᵈ where
   top_add' := by simp
-  neg_top := by ext; simp; simp [bot_eq_zero'']
+  neg_top := by ext; simp; simp [bot_eq_zero]
   add_neg_cancel_of_ne_top := by
     simp
-    simp +contextual [bot_eq_zero'', Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
+    simp +contextual [bot_eq_zero, Additive.ext_iff, OrderDual.ext_iff, -Additive.toMul_eq_top,
       -ofDual_eq_zero]
 
 -- Counterexample with monoid for the backward direction:
@@ -171,7 +157,7 @@ lemma denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units :
     refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩
   · refine ⟨fun x y h ↦ ?_⟩
     lift y to αˣ using (ne_zero_of_lt h).isUnit
-    obtain rfl | hx := (zero_le' (a := x)).eq_or_lt
+    obtain rfl | hx := eq_zero_or_pos x
     · obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
       exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
     · lift x to αˣ using hx.ne'.isUnit
@@ -201,7 +187,7 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual
   zero := .ofAdd <| .toDual ⊤
   zero_mul := @top_add _ (_)
   mul_zero := @add_top _ (_)
-  zero_le _ := (le_top : _ ≤ ⊤)
+  isBot_zero _ := (le_top : _ ≤ ⊤)
   mul_lt_mul_of_pos_left := by
     simpa [← ofAdd_add, ← toDual_add]
       using fun a ha b c hbc ↦ add_right_strictMono_of_ne_top (by simpa using ha.ne') hbc
@@ -214,7 +200,7 @@ theorem ofAdd_toDual_eq_zero_iff [LinearOrderedAddCommMonoidWithTop α]
 theorem ofDual_toAdd_eq_top_iff [LinearOrderedAddCommMonoidWithTop α]
     (x : Multiplicative αᵒᵈ) : OrderDual.ofDual x.toAdd = ⊤ ↔ x = 0 := Iff.rfl
 
-@[deprecated bot_eq_zero'' (since := "2025-11-17")]
+@[deprecated bot_eq_zero (since := "2025-11-17")]
 theorem ofAdd_bot [LinearOrderedAddCommMonoidWithTop α] :
     Multiplicative.ofAdd ⊥ = (0 : Multiplicative αᵒᵈ) := rfl
 
@@ -255,7 +241,11 @@ instance instOrderBot : OrderBot (WithZero α) := inferInstanceAs <| OrderBot (W
 instance instBoundedOrder [OrderTop α] : BoundedOrder (WithZero α) :=
   inferInstanceAs <| BoundedOrder (WithBot α)
 
-@[simp] lemma zero_le (a : WithZero α) : 0 ≤ a := bot_le (a := a)
+instance : IsBotZeroClass (WithZero α) where
+  isBot_zero _ := bot_le
+
+-- TODO: deprecate
+lemma zero_le (a : WithZero α) : 0 ≤ a := by simp
 
 /-- There is a general version `le_zero_iff`, but this lemma does not require a `PartialOrder`. -/
 @[simp]
@@ -521,7 +511,7 @@ instance instCanonicallyOrderedAdd [AddZeroClass α] [Preorder α] [CanonicallyO
 
 instance instLinearOrderedCommMonoidWithZero [CommMonoid α] [LinearOrder α]
     [IsOrderedCancelMonoid α] : LinearOrderedCommMonoidWithZero (WithZero α) where
-  zero_le := WithZero.zero_le
+  isBot_zero := WithZero.zero_le
   mul_lt_mul_of_pos_left
   | (a : α), _, 0, (c : α), _ => by simp [← WithZero.coe_mul]
   | (a : α), _, (b : α), (c : α), hbc => by norm_cast at *; exact mul_lt_mul_right hbc _

Mathlib/Algebra/Order/GroupWithZero/Range.lean

@@ -47,7 +47,7 @@ instance : IsOrderedMonoid (ValueGroup₀ f) :=
   Function.Injective.isOrderedMonoid embedding (map_mul _) embedding_strictMono.le_iff_le
 
 instance : LinearOrderedCommGroupWithZero (ValueGroup₀ f) where
-  zero_le := by simp
+  isBot_zero _ := by simp
   mul_lt_mul_of_pos_left a ha b c hbc := by
     simp only [← (embedding_strictMono (f := f)).lt_iff_lt, map_mul] at *
     exact (mul_lt_mul_iff_of_pos_left ha).mpr hbc

Mathlib/Algebra/Order/IsBotOne.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import Mathlib.Algebra.Order.ZeroLEOne
+public import Mathlib.Tactic.ToAdditive
+public import Mathlib.Order.Max
+public import Mathlib.Order.BoundedOrder.Basic
+
+/-!
+# Typeclasses expressing `IsBot 1` and `IsBot 0`
+-/
+
+public section
+
+/-- A typeclass expressing that the `0` of a type is a bottom element. In a partial `OrderBot`, this
+is equivalent to `⊥ = 0`. -/
+class IsBotZeroClass (α : Type*) [LE α] [Zero α] : Prop where
+  isBot_zero : IsBot (0 : α)
+
+/-- A typeclass expressing that the `1` of a type is a bottom element. In a partial `OrderBot`, this
+is equivalent to `⊥ = 1`. -/
+@[to_additive existing]
+class IsBotOneClass (α : Type*) [LE α] [One α] : Prop where
+  isBot_one : IsBot (1 : α)
+
+variable {α : Type*} {a b : α}
+
+section LE
+variable [LE α] [One α] [IsBotOneClass α]
+
+@[to_additive]
+theorem isBot_one : IsBot (1 : α) :=
+  IsBotOneClass.isBot_one
+
+@[to_additive (attr := simp) zero_le]
+theorem one_le {a : α} : 1 ≤ a :=
+  isBot_one a
+
+-- TODO: deprecate
+alias zero_le' := zero_le
+
+variable (α) in
+/-- Create an `OrderBot` instance, setting `1` as the bottom element. -/
+@[to_additive (attr := implicit_reducible)
+/-- Create an `OrderBot` instance, setting `0` as the bottom element. -/]
+def IsBotOneClass.toOrderBot : OrderBot α where
+  bot := 1
+  bot_le _ := one_le
+
+end LE
+
+-- See note [lower instance priority]
+instance (priority := 100) [LE α] [Zero α] [One α] [IsBotZeroClass α] : ZeroLEOneClass α where
+  zero_le_one := zero_le
+
+section Preorder
+variable [Preorder α] [One α] [IsBotOneClass α]
+
+@[to_additive (attr := simp) not_lt_zero]
+theorem not_lt_one : ¬ a < 1 := one_le.not_gt
+
+@[deprecated (since := "2025-12-03")] alias not_neg := not_lt_zero
+
+-- TODO: deprecate
+alias not_lt_zero' := not_lt_zero
+
+@[to_additive] -- `(attr := simp)` cannot be used here because `a` cannot be inferred by `simp`.
+theorem one_lt_of_gt (h : a < b) : 1 < b :=
+  one_le.trans_lt h
+
+@[to_additive] alias LT.lt.one_lt := one_lt_of_gt
+
+@[to_additive]
+theorem ne_one_of_lt (h : a < b) : b ≠ 1 :=
+  h.one_lt.ne'
+
+@[to_additive] alias LT.lt.ne_one := ne_one_of_lt
+
+end Preorder
+
+section PartialOrder
+variable [PartialOrder α] [One α] [IsBotOneClass α]
+
+-- Not `simp`, as different types might have a different preferred form.
+@[to_additive]
+theorem bot_eq_one [OrderBot α] : (⊥ : α) = 1 := isBot_one.eq_bot.symm
+
+-- TODO: deprecate
+alias bot_eq_zero'' := bot_eq_zero
+
+@[to_additive (attr := simp)]
+theorem le_one_iff_eq_one : a ≤ 1 ↔ a = 1 :=
+  one_le.ge_iff_eq'
+
+-- TODO: deprecate
+alias le_zero_iff := nonpos_iff_eq_zero
+
+@[to_additive] alias ⟨eq_one_of_le_one, _⟩ := le_one_iff_eq_one
+@[to_additive] alias LE.le.eq_one := eq_one_of_le_one
+
+@[to_additive]
+theorem one_lt_iff_ne_one : 1 < a ↔ a ≠ 1 :=
+  one_le.lt_iff_ne.trans ne_comm
+
+-- TODO: deprecate
+alias zero_lt_iff := pos_iff_ne_zero
+
+@[to_additive] alias ⟨_, one_lt_of_ne_one⟩ := one_lt_iff_ne_one
+@[to_additive] alias Ne.one_lt := one_lt_of_ne_one
+
+@[to_additive]
+theorem eq_one_or_one_lt (a : α) : a = 1 ∨ 1 < a := one_le.eq_or_lt'
+
+@[to_additive]
+lemma one_notMem_iff {s : Set α} : 1 ∉ s ↔ ∀ x ∈ s, 1 < x :=
+  let := IsBotOneClass.toOrderBot α
+  bot_notMem_iff
+
+@[deprecated (since := "2026-02-17")] alias NE.ne.pos := Ne.pos
+@[deprecated (since := "2026-02-17")] alias NE.ne.one_lt := Ne.one_lt
+
+end PartialOrder
+
+section LinearOrder
+variable [LinearOrder α] [One α] [IsBotOneClass α]
+
+@[to_additive]
+theorem one_min (a : α) : min 1 a = 1 :=
+  min_eq_left one_le
+
+@[to_additive]
+theorem min_one (a : α) : min a 1 = 1 :=
+  min_eq_right one_le
+
+end LinearOrder
+
+namespace NeZero
+variable [Zero α]
+
+theorem of_gt [Preorder α] [IsBotZeroClass α] (h : a < b) : NeZero b :=
+  ⟨h.ne_zero⟩
+
+theorem pos [PartialOrder α] [IsBotZeroClass α] (a : α) [NeZero a] : 0 < a :=
+  NeZero.out.pos
+
+-- 1 < p is still an often-used `Fact`, due to `Nat.Prime` implying it, and it implying `Nontrivial`
+-- on `ZMod`'s ring structure. We cannot just set this to be any `x < y`, else that becomes a
+-- metavariable and it will hugely slow down typeclass inference.
+instance (priority := 10) of_gt' [Preorder α] [IsBotZeroClass α] [One α]
+    [Fact (1 < a)] : NeZero a := of_gt <| @Fact.out (1 < a) _
+
+theorem of_ge [PartialOrder α] [IsBotZeroClass α] [NeZero a] (h : a ≤ b) : NeZero b :=
+  ⟨((pos a).trans_le h).ne_zero⟩
+
+end NeZero