From 9bb1256d57c5f6d1cf1ed17089030e22d02c2e19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Sun, 31 Jul 2022 20:14:27 +0000
Subject: [PATCH] =?UTF-8?q?feat(order/succ=5Fpred/basic):=20`a=20=E2=89=A4?=
 =?UTF-8?q?=20succ=20=E2=8A=A5=20=E2=86=94=20a=20=3D=20=E2=8A=A5=20?=
 =?UTF-8?q?=E2=88=A8=20a=20=3D=20succ=20=E2=8A=A5`=20and=20related=20(#155?=
 =?UTF-8?q?67)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We use these new results to golf down the ordinal API.
---
 src/order/succ_pred/basic.lean         | 20 ++++++++++++++++++--
 src/set_theory/ordinal/arithmetic.lean | 11 ++---------
 src/set_theory/ordinal/basic.lean      |  6 ++----
 3 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/src/order/succ_pred/basic.lean b/src/order/succ_pred/basic.lean
index c3a1904915278..5f731b9006596 100644
--- a/src/order/succ_pred/basic.lean
+++ b/src/order/succ_pred/basic.lean
@@ -362,7 +362,15 @@ lt_succ_iff_not_is_max.trans not_is_max_iff_ne_top
 end order_top
 
 section order_bot
-variables [order_bot α] [nontrivial α]
+variable [order_bot α]
+
+@[simp] lemma lt_succ_bot_iff [no_max_order α] : a < succ ⊥ ↔ a = ⊥ :=
+by rw [lt_succ_iff, le_bot_iff]
+
+lemma le_succ_bot_iff : a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥ :=
+by rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]
+
+variable [nontrivial α]
 
 lemma bot_lt_succ (a : α) : ⊥ < succ a :=
 (lt_succ_of_not_is_max not_is_max_bot).trans_le $ succ_mono bot_le
@@ -575,7 +583,15 @@ variables [order_bot α]
 end order_bot
 
 section order_top
-variables [order_top α] [nontrivial α]
+
+variable [order_top α]
+
+@[simp] lemma pred_top_lt_iff [no_min_order α] : pred ⊤ < a ↔ a = ⊤ :=
+@lt_succ_bot_iff αᵒᵈ _ _ _ _ _
+
+lemma pred_top_le_iff : pred ⊤ ≤ a ↔ a = ⊤ ∨ a = pred ⊤ := @le_succ_bot_iff αᵒᵈ _ _ _ _
+
+variable [nontrivial α]
 
 lemma pred_lt_top (a : α) : pred a < ⊤ :=
 (pred_mono le_top).trans_lt $ pred_lt_of_not_is_min not_is_min_top
diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean
index 5524d109f77eb..eccff6128b1a2 100644
--- a/src/set_theory/ordinal/arithmetic.lean
+++ b/src/set_theory/ordinal/arithmetic.lean
@@ -120,8 +120,7 @@ theorem nat_cast_succ (n : ℕ) : ↑n.succ = succ (n : ordinal) := rfl
 theorem add_left_cancel (a) {b c : ordinal} : a + b = a + c ↔ b = c :=
 by simp only [le_antisymm_iff, add_le_add_iff_left]
 
-theorem lt_one_iff_zero {a : ordinal} : a < 1 ↔ a = 0 :=
-by rw [←succ_zero, lt_succ_iff, ordinal.le_zero]
+theorem lt_one_iff_zero {a : ordinal} : a < 1 ↔ a = 0 := by simpa using @lt_succ_bot_iff _ _ _ a _ _
 
 private theorem add_lt_add_iff_left' (a) {b c : ordinal} : a + b < a + c ↔ b < c :=
 by rw [← not_le, ← not_le, add_le_add_iff_left]
@@ -185,13 +184,7 @@ unique.eq_default x
 by rw [one_out_eq x, typein_enum]
 
 theorem le_one_iff {a : ordinal} : a ≤ 1 ↔ a = 0 ∨ a = 1 :=
-begin
-  refine ⟨λ ha, _, _⟩,
-  { rcases eq_or_lt_of_le ha with rfl | ha,
-    exacts [or.inr rfl, or.inl (lt_one_iff_zero.1 ha)], },
-  { rintro (rfl | rfl),
-    exacts [zero_le_one, le_rfl], }
-end
+by simpa using @le_succ_bot_iff _ _ _ a _
 
 theorem add_eq_zero_iff {a b : ordinal} : a + b = 0 ↔ (a = 0 ∧ b = 0) :=
 induction_on a $ λ α r _, induction_on b $ λ β s _, begin
diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean
index 0a4f52e70e0c9..551a395dc6917 100644
--- a/src/set_theory/ordinal/basic.lean
+++ b/src/set_theory/ordinal/basic.lean
@@ -408,11 +408,9 @@ induction_on o $ λ α r _, ⟨⟨⟨embedding.of_is_empty, is_empty_elim⟩, is
 
 instance : order_bot ordinal := ⟨0, ordinal.zero_le⟩
 
-@[simp] protected theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 :=
-by simp only [le_antisymm_iff, ordinal.zero_le, and_true]
+@[simp] protected theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 := le_bot_iff
 
-protected theorem pos_iff_ne_zero {o : ordinal} : 0 < o ↔ o ≠ 0 :=
-by simp only [lt_iff_le_and_ne, ordinal.zero_le, true_and, ne.def, eq_comm]
+protected theorem pos_iff_ne_zero {o : ordinal} : 0 < o ↔ o ≠ 0 := bot_lt_iff_ne_bot
 
 @[simp] theorem out_empty_iff_eq_zero {o : ordinal} : is_empty o.out.α ↔ o = 0 :=
 by rw [←@type_eq_zero_iff_is_empty o.out.α (<), type_lt]