feat: Iic 2 = {0, 1, 2} (leanprover-community#37557)

Author: vihdzp

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.Monoid.Defs
 public import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 public import Mathlib.Algebra.NeZero
 public import Mathlib.Order.BoundedOrder.Basic
+public import Mathlib.Order.Interval.Set.Defs
 
 /-!
 # Canonically ordered monoids
@@ -137,6 +138,10 @@ end LE
 section Preorder
 variable [Preorder α] [CanonicallyOrderedMul α] {a b : α}
 
+@[to_additive]
+instance isEmpty_Iio_one : IsEmpty (Set.Iio (1 : α)) :=
+  ⟨fun ⟨a, ha⟩ ↦ not_le_of_gt ha (isBot_one a)⟩
+
 @[to_additive (attr := simp) not_lt_zero] lemma not_lt_one : ¬ a < 1 := (one_le a).not_gt
 
 @[deprecated (since := "2025-12-03")] alias not_neg := not_lt_zero

Mathlib/Algebra/Order/SuccPred.lean

@@ -259,13 +259,26 @@ theorem lt_one_iff [CanonicallyOrderedAdd α] : x < 1 ↔ x = 0 := by
 theorem le_one_iff [CanonicallyOrderedAdd α] : x ≤ 1 ↔ x = 0 ∨ x = 1 := by
   rw [le_iff_lt_or_eq, lt_one_iff]
 
+@[simp]
+theorem Iio_one [CanonicallyOrderedAdd α] : Set.Iio (1 : α) = {0} := by
+  ext; simp
+
+theorem Iic_one [CanonicallyOrderedAdd α] : Set.Iic (1 : α) = {0, 1} := by
+  ext; simp [le_one_iff]
+
 @[simp]
 theorem lt_two_iff : x < 2 ↔ x ≤ 1 := by
   rw [← one_add_one_eq_two, lt_add_one_iff]
 
 theorem le_two_iff [CanonicallyOrderedAdd α] : x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2 := by
   rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
 
+theorem Iio_two [CanonicallyOrderedAdd α] : Set.Iio (2 : α) = {0, 1} := by
+  ext; simp [le_one_iff]
+
+theorem Iic_two [CanonicallyOrderedAdd α] : Set.Iic (2 : α) = {0, 1, 2} := by
+  ext; simp [le_two_iff]
+
 end AddMonoidWithOne
 
 section Sub

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -343,14 +343,10 @@ instance : OrderBot Ordinal where
 theorem bot_eq_zero : (⊥ : Ordinal) = 0 :=
   rfl
 
-instance instIsEmptyIioZero : IsEmpty (Iio (0 : Ordinal)) := by
-  simp [← bot_eq_zero]
-
 @[deprecated nonpos_iff_eq_zero (since := "2025-11-21")]
 protected theorem le_zero {o : Ordinal} : o ≤ 0 ↔ o = 0 :=
   le_bot_iff
 
-
 @[deprecated not_neg (since := "2025-11-21")]
 protected theorem not_lt_zero (o : Ordinal) : ¬o < 0 :=
   not_lt_bot