chore(order/with_bot): lemmas about unbot and untop (#18582)

leanprover-community · Mar 15, 2023 · 0111834 · 0111834
1 parent 10bf4f8
commit 0111834
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 5 deletions.
diff --git a/src/algebra/order/monoid/with_top.lean b/src/algebra/order/monoid/with_top.lean
@@ -11,7 +11,8 @@ import data.nat.cast.defs
 /-! # Adjoining top/bottom elements to ordered monoids.
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
-> Any changes to this file require a corresponding PR to mathlib4.-/
+> Any changes to this file require a corresponding PR to mathlib4.
+-/
 
 universes u v
 variables {α : Type u} {β : Type v}
@@ -31,6 +32,9 @@ variables [has_one α]
 @[simp, norm_cast, to_additive] lemma coe_eq_one {a : α} : (a : with_top α) = 1 ↔ a = 1 :=
 coe_eq_coe
 
+@[simp, to_additive] lemma untop_one : (1 : with_top α).untop coe_ne_top = 1 := rfl
+@[simp, to_additive] lemma untop_one' (d : α) : (1 : with_top α).untop' d = 1 := rfl
+
 @[simp, norm_cast, to_additive coe_nonneg]
 lemma one_le_coe [has_le α] {a : α} : 1 ≤ (a : with_top α) ↔ 1 ≤ a := coe_le_coe
 
@@ -347,6 +351,9 @@ lemma coe_one [has_one α] : ((1 : α) : with_bot α) = 1 := rfl
 lemma coe_eq_one [has_one α] {a : α} : (a : with_bot α) = 1 ↔ a = 1 :=
 with_top.coe_eq_one
 
+@[simp, to_additive] lemma unbot_one [has_one α] : (1 : with_bot α).unbot coe_ne_bot = 1 := rfl
+@[simp, to_additive] lemma unbot_one' [has_one α] (d : α) : (1 : with_bot α).unbot' d = 1 := rfl
+
 @[simp, norm_cast, to_additive coe_nonneg]
 lemma one_le_coe [has_one α] [has_le α] {a : α} : 1 ≤ (a : with_bot α) ↔ 1 ≤ a := coe_le_coe
 

diff --git a/src/algebra/order/ring/with_top.lean b/src/algebra/order/ring/with_top.lean
@@ -20,8 +20,6 @@ variables {α : Type*}
 
 namespace with_top
 
-instance [nonempty α] : nontrivial (with_top α) := option.nontrivial
-
 variable [decidable_eq α]
 
 section has_mul
@@ -198,8 +196,6 @@ end with_top
 
 namespace with_bot
 
-instance [nonempty α] : nontrivial (with_bot α) := option.nontrivial
-
 variable [decidable_eq α]
 
 section has_mul

diff --git a/src/order/succ_pred/basic.lean b/src/order/succ_pred/basic.lean
@@ -825,6 +825,11 @@ instance : pred_order (with_top α) :=
 @[simp] lemma pred_top : pred (⊤ : with_top α) = ↑(⊤ : α) := rfl
 @[simp] lemma pred_coe (a : α) : pred (↑a : with_top α) = ↑(pred a) := rfl
 
+@[simp] lemma pred_untop : ∀ (a : with_top α) (ha : a ≠ ⊤),
+  pred (a.untop ha) = (pred a).untop (by induction a using with_top.rec_top_coe; simp)
+| ⊤ ha := (ha rfl).elim
+| (a : α) ha := rfl
+
 end pred
 
 /-! #### Adding a `⊤` to a `no_max_order` -/
@@ -922,6 +927,11 @@ instance : succ_order (with_bot α) :=
 @[simp] lemma succ_bot : succ (⊥ : with_bot α) = ↑(⊥ : α) := rfl
 @[simp] lemma succ_coe (a : α) : succ (↑a : with_bot α) = ↑(succ a) := rfl
 
+@[simp] lemma succ_unbot : ∀ (a : with_bot α) (ha : a ≠ ⊥),
+  succ (a.unbot ha) = (succ a).unbot (by induction a using with_bot.rec_bot_coe; simp)
+| ⊥ ha := (ha rfl).elim
+| (a : α) ha := rfl
+
 end succ
 
 section pred

diff --git a/src/order/with_bot.lean b/src/order/with_bot.lean
@@ -48,6 +48,8 @@ meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_
 
 instance : inhabited (with_bot α) := ⟨⊥⟩
 
+instance [nonempty α] : nontrivial (with_bot α) := option.nontrivial
+
 open function
 
 lemma coe_injective : injective (coe : α → with_bot α) := option.some_injective _
@@ -420,6 +422,8 @@ meta instance {α : Type} [reflected _ α] [has_reflect α] : has_reflect (with_
 
 instance : inhabited (with_top α) := ⟨⊤⟩
 
+instance [nonempty α] : nontrivial (with_top α) := option.nontrivial
+
 protected lemma «forall» {p : with_top α → Prop} : (∀ x, p x) ↔ p ⊤ ∧ ∀ x : α, p x := option.forall
 protected lemma «exists» {p : with_top α → Prop} : (∃ x, p x) ↔ p ⊤ ∨ ∃ x : α, p x := option.exists