diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index be2fe23005cfe..e9e050019e5fd 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -155,22 +155,19 @@ theorem add_lt_top [LT α] {a b : WithTop α} : a + b < ⊤ ↔ a < ⊤ ∧ b <
 
 theorem add_eq_coe :
     ∀ {a b : WithTop α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
-  | none, b, c => by simp [none_eq_top]
-  | Option.some a, none, c => by simp [none_eq_top]
-  | Option.some a, Option.some b, c =>
-  by simp only [some_eq_coe, ← coe_add, coe_eq_coe, exists_and_left, exists_eq_left]
+  | ⊤, b, c => by simp
+  | some a, ⊤, c => by simp
+  | some a, some b, c => by norm_cast; simp
 #align with_top.add_eq_coe WithTop.add_eq_coe
 
 -- Porting note: simp can already prove this.
 -- @[simp]
-theorem add_coe_eq_top_iff {x : WithTop α} {y : α} : x + y = ⊤ ↔ x = ⊤ := by
-  induction x using WithTop.recTopCoe <;> simp [← coe_add]
+theorem add_coe_eq_top_iff {x : WithTop α} {y : α} : x + y = ⊤ ↔ x = ⊤ := by simp
 #align with_top.add_coe_eq_top_iff WithTop.add_coe_eq_top_iff
 
 -- Porting note: simp can already prove this.
 -- @[simp]
-theorem coe_add_eq_top_iff {y : WithTop α} : ↑x + y = ⊤ ↔ y = ⊤ := by
-  induction y using WithTop.recTopCoe <;> simp [← coe_add]
+theorem coe_add_eq_top_iff {y : WithTop α} : ↑x + y = ⊤ ↔ y = ⊤ := by simp
 #align with_top.coe_add_eq_top_iff WithTop.coe_add_eq_top_iff
 
 theorem add_right_cancel_iff [IsRightCancelAdd α] (ha : a ≠ ⊤) : b + a = c + a ↔ b = c := by
@@ -364,8 +361,7 @@ instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
       rw [Nat.cast_zero, WithTop.coe_zero],
     natCast_succ := fun n => by
       simp only -- Porting note: Had to add this...?
-      rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one]
-  }
+      rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one] }
 
 @[simp, norm_cast] lemma coe_nat (n : ℕ) : ((n : α) : WithTop α) = n := rfl
 #align with_top.coe_nat WithTop.coe_nat
@@ -385,14 +381,8 @@ instance charZero [AddMonoidWithOne α] [CharZero α] : CharZero (WithTop α) :=
 instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α) :=
   { WithTop.addMonoidWithOne, WithTop.addCommMonoid with }
 
-instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α) :=
-  { WithTop.partialOrder, WithTop.addCommMonoid with
-    add_le_add_left := by
-      rintro a b h (_ | c); · simp [none_eq_top]
-      rcases b with (_ | b); · simp [none_eq_top]
-      rcases le_coe_iff.1 h with ⟨a, rfl, _⟩
-      simp only [some_eq_coe, ← coe_add, coe_le_coe] at h ⊢
-      exact add_le_add_left h c }
+instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α) where
+  add_le_add_left _ _ := add_le_add_left
 
 instance linearOrderedAddCommMonoidWithTop [LinearOrderedAddCommMonoid α] :
     LinearOrderedAddCommMonoidWithTop (WithTop α) :=
diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
index bfa33337f27cd..fc2d218f2ba85 100644
--- a/Mathlib/Order/WithBot.lean
+++ b/Mathlib/Order/WithBot.lean
@@ -96,8 +96,8 @@ theorem coe_ne_bot : (a : WithBot α) ≠ ⊥ :=
 /-- Recursor for `WithBot` using the preferred forms `⊥` and `↑a`. -/
 @[elab_as_elim]
 def recBotCoe {C : WithBot α → Sort*} (bot : C ⊥) (coe : ∀ a : α, C a) : ∀ n : WithBot α, C n
-  | none => bot
-  | Option.some a => coe a
+  | ⊥ => bot
+  | (a : α) => coe a
 #align with_bot.rec_bot_coe WithBot.recBotCoe
 
 @[simp]
@@ -239,18 +239,18 @@ theorem coe_le : ∀ {o : Option α}, b ∈ o → ((a : WithBot α) ≤ o ↔ a
 #align with_bot.coe_le WithBot.coe_le
 
 theorem coe_le_iff : ∀ {x : WithBot α}, (a : WithBot α) ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b
-  | Option.some x => by simp [some_eq_coe]
-  | none => iff_of_false (not_coe_le_bot _) <| by simp [none_eq_bot]
+  | (x : α) => by simp
+  | ⊥ => iff_of_false (not_coe_le_bot _) <| by simp
 #align with_bot.coe_le_iff WithBot.coe_le_iff
 
 theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b
-  | Option.some b => by simp [some_eq_coe, coe_eq_coe]
-  | none => by simp [none_eq_bot]
+  | (b : α) => by simp
+  | ⊥ => by simp
 #align with_bot.le_coe_iff WithBot.le_coe_iff
 
 protected theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α)
-  | none, _ => bot_le
-  | Option.some _, hb => some_le_some.2 <| h <| some_le_some.1 hb
+  | ⊥, _ => bot_le
+  | (_ : α), hb => some_le_some.2 <| h <| some_le_some.1 hb
 #align is_max.with_bot IsMax.withBot
 
 theorem le_unbot_iff {a : α} {b : WithBot α} (h : b ≠ ⊥) :
@@ -305,13 +305,13 @@ theorem not_lt_none (a : WithBot α) : ¬@LT.lt (WithBot α) _ a none :=
 #align with_bot.not_lt_none WithBot.not_lt_none
 
 theorem lt_iff_exists_coe : ∀ {a b : WithBot α}, a < b ↔ ∃ p : α, b = p ∧ a < p
-  | a, Option.some b => by simp [some_eq_coe, coe_eq_coe]
-  | a, none => iff_of_false (not_lt_none _) <| by simp [none_eq_bot]
+  | a, some b => by simp [coe_eq_coe]
+  | a, ⊥ => iff_of_false (not_lt_none _) <| by simp
 #align with_bot.lt_iff_exists_coe WithBot.lt_iff_exists_coe
 
-theorem lt_coe_iff : ∀ {x : WithBot α}, x < b ↔ ∀ a : α, x = ↑a → a < b
-  | Option.some b => by simp [some_eq_coe, coe_eq_coe, coe_lt_coe]
-  | none => by simp [none_eq_bot, bot_lt_coe]
+theorem lt_coe_iff : ∀ {x : WithBot α}, x < b ↔ ∀ a : α, x = a → a < b
+  | (_ : α) => by simp
+  | ⊥ => by simp [bot_lt_coe]
 #align with_bot.lt_coe_iff WithBot.lt_coe_iff
 
 /-- A version of `bot_lt_iff_ne_bot` for `WithBot` that only requires `LT α`, not
@@ -1300,12 +1300,11 @@ instance instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop 
 
 instance trichotomous.lt [Preorder α] [IsTrichotomous α (· < ·)] :
     IsTrichotomous (WithTop α) (· < ·) :=
-  ⟨by
-    rintro (a | a) (b | b)
-    · simp
-    · simp
-    · simp
-    · simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· < ·) _ a b⟩
+  ⟨fun
+    | (a : α), (b : α) => by simp [trichotomous]
+    | ⊤, (b : α) => by simp
+    | (a : α), ⊤ => by simp
+    | ⊤, ⊤ => by simp⟩
 #align with_top.trichotomous.lt WithTop.trichotomous.lt
 
 instance IsWellOrder.lt [Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (WithTop α) (· < ·) where
@@ -1313,12 +1312,7 @@ instance IsWellOrder.lt [Preorder α] [IsWellOrder α (· < ·)] : IsWellOrder (
 
 instance trichotomous.gt [Preorder α] [IsTrichotomous α (· > ·)] :
     IsTrichotomous (WithTop α) (· > ·) :=
-  ⟨by
-    rintro (a | a) (b | b)
-    · simp
-    · simp
-    · simp
-    · simpa [some_eq_coe, IsTrichotomous, coe_eq_coe] using @trichotomous α (· > ·) _ a b⟩
+  have : IsTrichotomous α (· < ·) := .swap _; .swap _
 #align with_top.trichotomous.gt WithTop.trichotomous.gt
 
 instance IsWellOrder.gt [Preorder α] [IsWellOrder α (· > ·)] : IsWellOrder (WithTop α) (· > ·) where