diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index 3faca645b890d..c9994ce05b174 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 Ported by: Jon Eugster
 
 ! This file was ported from Lean 3 source module algebra.order.monoid.with_top
-! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
+! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,7 +15,8 @@ import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Algebra.Order.ZeroLEOne
 
-/-! # Adjoining top/bottom elements to ordered monoids. -/
+/-! # Adjoining top/bottom elements to ordered monoids.
+-/
 
 universe u v
 
@@ -47,6 +48,18 @@ theorem coe_eq_one {a : α} : (a : WithTop α) = 1 ↔ a = 1 :=
 #align with_top.coe_eq_one WithTop.coe_eq_one
 #align with_top.coe_eq_zero WithTop.coe_eq_zero
 
+@[to_additive (attr := simp)]
+theorem untop_one : (1 : WithTop α).untop coe_ne_top = 1 :=
+  rfl
+#align with_top.untop_one WithTop.untop_one
+#align with_top.untop_zero WithTop.untop_zero
+
+@[to_additive (attr := simp)]
+theorem untop_one' (d : α) : (1 : WithTop α).untop' d = 1 :=
+  rfl
+#align with_top.untop_one' WithTop.untop_one'
+#align with_top.untop_zero' WithTop.untop_zero'
+
 @[to_additive (attr := simp, norm_cast) coe_nonneg]
 theorem one_le_coe [LE α] {a : α} : 1 ≤ (a : WithTop α) ↔ 1 ≤ a :=
   coe_le_coe
@@ -480,6 +493,18 @@ theorem coe_eq_one [One α] {a : α} : (a : WithBot α) = 1 ↔ a = 1 :=
 #align with_bot.coe_eq_one WithBot.coe_eq_one
 #align with_bot.coe_eq_zero WithBot.coe_eq_zero
 
+@[to_additive (attr := simp)]
+theorem unbot_one [One α] : (1 : WithBot α).unbot coe_ne_bot = 1 :=
+  rfl
+#align with_bot.unbot_one WithBot.unbot_one
+#align with_bot.unbot_zero WithBot.unbot_zero
+
+@[to_additive (attr := simp)]
+theorem unbot_one' [One α] (d : α) : (1 : WithBot α).unbot' d = 1 :=
+  rfl
+#align with_bot.unbot_one' WithBot.unbot_one'
+#align with_bot.unbot_zero' WithBot.unbot_zero'
+
 @[to_additive (attr := simp, norm_cast) coe_nonneg]
 theorem one_le_coe [One α] [LE α] {a : α} : 1 ≤ (a : WithBot α) ↔ 1 ≤ a :=
   coe_le_coe
diff --git a/Mathlib/Algebra/Order/Ring/WithTop.lean b/Mathlib/Algebra/Order/Ring/WithTop.lean
index 3e5752f27163f..4b0c747dc42e6 100644
--- a/Mathlib/Algebra/Order/Ring/WithTop.lean
+++ b/Mathlib/Algebra/Order/Ring/WithTop.lean
@@ -2,8 +2,9 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+
 ! This file was ported from Lean 3 source module algebra.order.ring.with_top
-! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
+! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -21,9 +22,6 @@ variable {α : Type _}
 
 namespace WithTop
 
-instance [Nonempty α] : Nontrivial (WithTop α) :=
-  Option.nontrivial
-
 variable [DecidableEq α]
 
 instance : DecidableEq (WithTop α) := instDecidableEqOption
@@ -221,9 +219,6 @@ end WithTop
 
 namespace WithBot
 
-instance [Nonempty α] : Nontrivial (WithBot α) :=
-  Option.nontrivial
-
 variable [DecidableEq α]
 
 instance : DecidableEq (WithBot α) := instDecidableEqOption
diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean
index 635f402b9d68a..46093bd49ace8 100644
--- a/Mathlib/Order/SuccPred/Basic.lean
+++ b/Mathlib/Order/SuccPred/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module order.succ_pred.basic
-! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
+! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1105,6 +1105,14 @@ theorem pred_coe (a : α) : pred (↑a : WithTop α) = ↑(pred a) :=
   rfl
 #align with_top.pred_coe WithTop.pred_coe
 
+@[simp]
+theorem pred_untop :
+    ∀ (a : WithTop α) (ha : a ≠ ⊤),
+      pred (a.untop ha) = (pred a).untop (by induction a using WithTop.recTopCoe <;> simp)
+  | ⊤, ha => (ha rfl).elim
+  | (a : α), _ => rfl
+#align with_top.pred_untop WithTop.pred_untop
+
 end Pred
 
 /-! #### Adding a `⊤` to a `NoMaxOrder` -/
@@ -1208,6 +1216,14 @@ theorem succ_coe (a : α) : succ (↑a : WithBot α) = ↑(succ a) :=
   rfl
 #align with_bot.succ_coe WithBot.succ_coe
 
+@[simp]
+theorem succ_unbot :
+    ∀ (a : WithBot α) (ha : a ≠ ⊥),
+      succ (a.unbot ha) = (succ a).unbot (by induction a using WithBot.recBotCoe <;> simp)
+  | ⊥, ha => (ha rfl).elim
+  | (a : α), _ => rfl
+#align with_bot.succ_unbot WithBot.succ_unbot
+
 end Succ
 
 section Pred
diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
index ecf94bce09226..0f9ad5b0175d0 100644
--- a/Mathlib/Order/WithBot.lean
+++ b/Mathlib/Order/WithBot.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module order.with_bot
-! leanprover-community/mathlib commit afdb4fa3b32d41106a4a09b371ce549ad7958abd
+! leanprover-community/mathlib commit 0111834459f5d7400215223ea95ae38a1265a907
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -53,6 +53,9 @@ instance bot : Bot (WithBot α) :=
 instance inhabited : Inhabited (WithBot α) :=
   ⟨⊥⟩
 
+instance nontrivial [Nonempty α] : Nontrivial (WithBot α) :=
+  Option.nontrivial
+
 open Function
 
 theorem coe_injective : Injective (fun (a : α) => (a : WithBot α)) :=
@@ -578,6 +581,9 @@ instance top : Top (WithTop α) :=
 instance inhabited : Inhabited (WithTop α) :=
   ⟨⊤⟩
 
+instance nontrivial [Nonempty α] : Nontrivial (WithTop α) :=
+  Option.nontrivial
+
 protected theorem «forall» {p : WithTop α → Prop} : (∀ x, p x) ↔ p ⊤ ∧ ∀ x : α, p x :=
   Option.forall
 #align with_top.forall WithTop.forall