diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 32fef3471f15..38142ef99986 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian, Sebastian Ullrich
 -/
-
 module
 
 prelude
@@ -21,13 +20,13 @@ The relationship between the compared items may be:
  * `Ordering.gt`: greater than
 -/
 inductive Ordering where
-  | /-- Less than. -/
-    lt
-  | /-- Equal. -/
-    eq
-  | /-- Greater than. -/
-    gt
-deriving Inhabited, DecidableEq
+  /-- Less than. -/
+  | lt
+  /-- Equal. -/
+  | eq
+  /-- Greater than. -/
+  | gt
+deriving Inhabited, DecidableEq, Repr
 
 namespace Ordering
 
@@ -39,6 +38,7 @@ Examples:
  * `Ordering.eq.swap = Ordering.eq`
  * `Ordering.gt.swap = Ordering.lt`
 -/
+@[inline]
 def swap : Ordering → Ordering
   | .lt => .gt
   | .eq => .eq
@@ -96,6 +96,7 @@ Ordering.lt
 /--
 Checks whether the ordering is `eq`.
 -/
+@[inline]
 def isEq : Ordering → Bool
   | eq => true
   | _ => false
@@ -103,6 +104,7 @@ def isEq : Ordering → Bool
 /--
 Checks whether the ordering is not `eq`.
 -/
+@[inline]
 def isNe : Ordering → Bool
   | eq => false
   | _ => true
@@ -110,6 +112,7 @@ def isNe : Ordering → Bool
 /--
 Checks whether the ordering is `lt` or `eq`.
 -/
+@[inline]
 def isLE : Ordering → Bool
   | gt => false
   | _ => true
@@ -117,6 +120,7 @@ def isLE : Ordering → Bool
 /--
 Checks whether the ordering is `lt`.
 -/
+@[inline]
 def isLT : Ordering → Bool
   | lt => true
   | _ => false
@@ -124,6 +128,7 @@ def isLT : Ordering → Bool
 /--
 Checks whether the ordering is `gt`.
 -/
+@[inline]
 def isGT : Ordering → Bool
   | gt => true
   | _ => false
@@ -131,203 +136,158 @@ def isGT : Ordering → Bool
 /--
 Checks whether the ordering is `gt` or `eq`.
 -/
+@[inline]
 def isGE : Ordering → Bool
   | lt => false
   | _ => true
 
 section Lemmas
 
-@[simp]
-theorem isLT_lt : lt.isLT := rfl
-
-@[simp]
-theorem isLE_lt : lt.isLE := rfl
-
-@[simp]
-theorem isEq_lt : lt.isEq = false := rfl
-
-@[simp]
-theorem isNe_lt : lt.isNe = true := rfl
-
-@[simp]
-theorem isGE_lt : lt.isGE = false := rfl
-
-@[simp]
-theorem isGT_lt : lt.isGT = false := rfl
-
-@[simp]
-theorem isLT_eq : eq.isLT = false := rfl
-
-@[simp]
-theorem isLE_eq : eq.isLE := rfl
-
-@[simp]
-theorem isEq_eq : eq.isEq := rfl
-
-@[simp]
-theorem isNe_eq : eq.isNe = false := rfl
-
-@[simp]
-theorem isGE_eq : eq.isGE := rfl
-
-@[simp]
-theorem isGT_eq : eq.isGT = false := rfl
-
-@[simp]
-theorem isLT_gt : gt.isLT = false := rfl
-
-@[simp]
-theorem isLE_gt : gt.isLE = false := rfl
-
-@[simp]
-theorem isEq_gt : gt.isEq = false := rfl
-
-@[simp]
-theorem isNe_gt : gt.isNe = true := rfl
-
-@[simp]
-theorem isGE_gt : gt.isGE := rfl
-
-@[simp]
-theorem isGT_gt : gt.isGT := rfl
-
-@[simp]
-theorem swap_lt : lt.swap = .gt := rfl
-
-@[simp]
-theorem swap_eq : eq.swap = .eq := rfl
-
-@[simp]
-theorem swap_gt : gt.swap = .lt := rfl
-
-theorem eq_eq_of_isLE_of_isLE_swap {o : Ordering} : o.isLE → o.swap.isLE → o = .eq := by
-  cases o <;> simp
-
-theorem eq_eq_of_isGE_of_isGE_swap {o : Ordering} : o.isGE → o.swap.isGE → o = .eq := by
-  cases o <;> simp
-
-theorem eq_eq_of_isLE_of_isGE {o : Ordering} : o.isLE → o.isGE → o = .eq := by
-  cases o <;> simp
-
-theorem eq_swap_iff_eq_eq {o : Ordering} : o = o.swap ↔ o = .eq := by
-  cases o <;> simp
-
-theorem eq_eq_of_eq_swap {o : Ordering} : o = o.swap → o = .eq :=
-  eq_swap_iff_eq_eq.mp
-
-@[simp]
-theorem isLE_eq_false {o : Ordering} : o.isLE = false ↔ o = .gt := by
-  cases o <;> simp
-
-@[simp]
-theorem isGE_eq_false {o : Ordering} : o.isGE = false ↔ o = .lt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_eq_gt {o : Ordering} : o.swap = .gt ↔ o = .lt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_eq_lt {o : Ordering} : o.swap = .lt ↔ o = .gt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_eq_eq {o : Ordering} : o.swap = .eq ↔ o = .eq := by
-  cases o <;> simp
-
-@[simp]
-theorem isLT_swap {o : Ordering} : o.swap.isLT = o.isGT := by
-  cases o <;> simp
-
-@[simp]
-theorem isLE_swap {o : Ordering} : o.swap.isLE = o.isGE := by
-  cases o <;> simp
-
-@[simp]
-theorem isEq_swap {o : Ordering} : o.swap.isEq = o.isEq := by
-  cases o <;> simp
-
-@[simp]
-theorem isNe_swap {o : Ordering} : o.swap.isNe = o.isNe := by
-  cases o <;> simp
-
-@[simp]
-theorem isGE_swap {o : Ordering} : o.swap.isGE = o.isLE := by
-  cases o <;> simp
-
-@[simp]
-theorem isGT_swap {o : Ordering} : o.swap.isGT = o.isLT := by
-  cases o <;> simp
-
-theorem isLT_iff_eq_lt {o : Ordering} : o.isLT ↔ o = .lt := by
-  cases o <;> simp
-
-theorem isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE ↔ o = .lt ∨ o = .eq := by
-  cases o <;> simp
-
-theorem isLE_of_eq_lt {o : Ordering} : o = .lt → o.isLE := by
-  rintro rfl; rfl
-
-theorem isLE_of_eq_eq {o : Ordering} : o = .eq → o.isLE := by
-  rintro rfl; rfl
-
-theorem isEq_iff_eq_eq {o : Ordering} : o.isEq ↔ o = .eq := by
-  cases o <;> simp
-
-theorem isNe_iff_ne_eq {o : Ordering} : o.isNe ↔ o ≠ .eq := by
-  cases o <;> simp
-
-theorem isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE ↔ o = .gt ∨ o = .eq := by
-  cases o <;> simp
-
-theorem isGE_of_eq_gt {o : Ordering} : o = .gt → o.isGE := by
-  rintro rfl; rfl
-
-theorem isGE_of_eq_eq {o : Ordering} : o = .eq → o.isGE := by
-  rintro rfl; rfl
-
-theorem isGT_iff_eq_gt {o : Ordering} : o.isGT ↔ o = .gt := by
-  cases o <;> simp
-
-@[simp]
-theorem swap_swap {o : Ordering} : o.swap.swap = o := by
-  cases o <;> simp
-
-@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
-  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
-
-theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
-  cases o₁ <;> rfl
-
-theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by
-  cases o₁ <;> simp [«then»]
-
-theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-@[simp]
-theorem lt_then {o : Ordering} : lt.then o = lt := rfl
-
-@[simp]
-theorem gt_then {o : Ordering} : gt.then o = gt := rfl
-
-@[simp]
-theorem eq_then {o : Ordering} : eq.then o = o := rfl
-
-theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by
-  cases o₁ <;> simp
-
-theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by
-  cases o₁ <;> simp
-
-theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
-  cases o₁ <;> simp_all
+protected theorem «forall» {p : Ordering → Prop} : (∀ o, p o) ↔ p .lt ∧ p .eq ∧ p .gt := by
+  constructor
+  · intro h
+    exact ⟨h _, h _, h _⟩
+  · rintro ⟨h₁, h₂, h₃⟩ (_ | _ | _) <;> assumption
 
-theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
-  cases o₁ <;> simp_all
+protected theorem «exists» {p : Ordering → Prop} : (∃ o, p o) ↔ p .lt ∨ p .eq ∨ p .gt := by
+  constructor
+  · rintro ⟨(_ | _ | _), h⟩
+    · exact .inl h
+    · exact .inr (.inl h)
+    · exact .inr (.inr h)
+  · rintro (h | h | h) <;> exact ⟨_, h⟩
+
+instance [DecidablePred p] : Decidable (∀ o : Ordering, p o) :=
+  decidable_of_decidable_of_iff Ordering.«forall».symm
+
+instance [DecidablePred p] : Decidable (∃ o : Ordering, p o) :=
+  decidable_of_decidable_of_iff Ordering.«exists».symm
+
+@[simp] theorem isLT_lt : lt.isLT := rfl
+@[simp] theorem isLE_lt : lt.isLE := rfl
+@[simp] theorem isEq_lt : lt.isEq = false := rfl
+@[simp] theorem isNe_lt : lt.isNe = true := rfl
+@[simp] theorem isGE_lt : lt.isGE = false := rfl
+@[simp] theorem isGT_lt : lt.isGT = false := rfl
+
+@[simp] theorem isLT_eq : eq.isLT = false := rfl
+@[simp] theorem isLE_eq : eq.isLE := rfl
+@[simp] theorem isEq_eq : eq.isEq := rfl
+@[simp] theorem isNe_eq : eq.isNe = false := rfl
+@[simp] theorem isGE_eq : eq.isGE := rfl
+@[simp] theorem isGT_eq : eq.isGT = false := rfl
+
+@[simp] theorem isLT_gt : gt.isLT = false := rfl
+@[simp] theorem isLE_gt : gt.isLE = false := rfl
+@[simp] theorem isEq_gt : gt.isEq = false := rfl
+@[simp] theorem isNe_gt : gt.isNe = true := rfl
+@[simp] theorem isGE_gt : gt.isGE := rfl
+@[simp] theorem isGT_gt : gt.isGT := rfl
+
+@[simp] theorem lt_beq_eq : (lt == eq) = false := rfl
+@[simp] theorem lt_beq_gt : (lt == gt) = false := rfl
+@[simp] theorem eq_beq_lt : (eq == lt) = false := rfl
+@[simp] theorem eq_beq_gt : (eq == gt) = false := rfl
+@[simp] theorem gt_beq_lt : (gt == lt) = false := rfl
+@[simp] theorem gt_beq_eq : (gt == eq) = false := rfl
+
+@[simp] theorem swap_lt : lt.swap = .gt := rfl
+@[simp] theorem swap_eq : eq.swap = .eq := rfl
+@[simp] theorem swap_gt : gt.swap = .lt := rfl
+
+theorem eq_eq_of_isLE_of_isLE_swap : ∀ {o : Ordering}, o.isLE → o.swap.isLE → o = .eq := by decide
+theorem eq_eq_of_isGE_of_isGE_swap : ∀ {o : Ordering}, o.isGE → o.swap.isGE → o = .eq := by decide
+theorem eq_eq_of_isLE_of_isGE : ∀ {o : Ordering}, o.isLE → o.isGE → o = .eq := by decide
+theorem eq_swap_iff_eq_eq : ∀ {o : Ordering}, o = o.swap ↔ o = .eq := by decide
+theorem eq_eq_of_eq_swap : ∀ {o : Ordering}, o = o.swap → o = .eq := eq_swap_iff_eq_eq.mp
+
+@[simp] theorem isLE_eq_false : ∀ {o : Ordering}, o.isLE = false ↔ o = .gt := by decide
+@[simp] theorem isGE_eq_false : ∀ {o : Ordering}, o.isGE = false ↔ o = .lt := by decide
+@[simp] theorem isNe_eq_false : ∀ {o : Ordering}, o.isNe = false ↔ o = .eq := by decide
+@[simp] theorem isEq_eq_false : ∀ {o : Ordering}, o.isEq = false ↔ ¬o = .eq := by decide
+
+@[simp] theorem swap_eq_gt : ∀ {o : Ordering}, o.swap = .gt ↔ o = .lt := by decide
+@[simp] theorem swap_eq_lt : ∀ {o : Ordering}, o.swap = .lt ↔ o = .gt := by decide
+@[simp] theorem swap_eq_eq : ∀ {o : Ordering}, o.swap = .eq ↔ o = .eq := by decide
+
+@[simp] theorem isLT_swap : ∀ {o : Ordering}, o.swap.isLT = o.isGT := by decide
+@[simp] theorem isLE_swap : ∀ {o : Ordering}, o.swap.isLE = o.isGE := by decide
+@[simp] theorem isEq_swap : ∀ {o : Ordering}, o.swap.isEq = o.isEq := by decide
+@[simp] theorem isNe_swap : ∀ {o : Ordering}, o.swap.isNe = o.isNe := by decide
+@[simp] theorem isGE_swap : ∀ {o : Ordering}, o.swap.isGE = o.isLE := by decide
+@[simp] theorem isGT_swap : ∀ {o : Ordering}, o.swap.isGT = o.isLT := by decide
+
+theorem isLE_of_eq_lt : ∀ {o : Ordering}, o = .lt → o.isLE := by decide
+theorem isLE_of_eq_eq : ∀ {o : Ordering}, o = .eq → o.isLE := by decide
+theorem isGE_of_eq_gt : ∀ {o : Ordering}, o = .gt → o.isGE := by decide
+theorem isGE_of_eq_eq : ∀ {o : Ordering}, o = .eq → o.isGE := by decide
+
+theorem ne_eq_of_eq_lt : ∀ {o : Ordering}, o = .lt → o ≠ .eq := by decide
+theorem ne_eq_of_eq_gt : ∀ {o : Ordering}, o = .gt → o ≠ .eq := by decide
+
+@[simp] theorem isLT_iff_eq_lt : ∀ {o : Ordering}, o.isLT ↔ o = .lt := by decide
+@[simp] theorem isGT_iff_eq_gt : ∀ {o : Ordering}, o.isGT ↔ o = .gt := by decide
+@[simp] theorem isEq_iff_eq_eq : ∀ {o : Ordering}, o.isEq ↔ o = .eq := by decide
+@[simp] theorem isNe_iff_ne_eq : ∀ {o : Ordering}, o.isNe ↔ ¬o = .eq := by decide
+
+theorem isLE_iff_ne_gt : ∀ {o : Ordering}, o.isLE ↔ ¬o = .gt := by decide
+theorem isGE_iff_ne_lt : ∀ {o : Ordering}, o.isGE ↔ ¬o = .lt := by decide
+theorem isLE_iff_eq_lt_or_eq_eq : ∀ {o : Ordering}, o.isLE ↔ o = .lt ∨ o = .eq := by decide
+theorem isGE_iff_eq_gt_or_eq_eq : ∀ {o : Ordering}, o.isGE ↔ o = .gt ∨ o = .eq := by decide
+
+theorem isLT_eq_beq_lt : ∀ {o : Ordering}, o.isLT = (o == .lt) := by decide
+theorem isLE_eq_not_beq_gt : ∀ {o : Ordering}, o.isLE = (!o == .gt) := by decide
+theorem isLE_eq_isLT_or_isEq : ∀ {o : Ordering}, o.isLE = (o.isLT || o.isEq) := by decide
+theorem isGT_eq_beq_gt : ∀ {o : Ordering}, o.isGT = (o == .gt) := by decide
+theorem isGE_eq_not_beq_lt : ∀ {o : Ordering}, o.isGE = (!o == .lt) := by decide
+theorem isGE_eq_isGT_or_isEq : ∀ {o : Ordering}, o.isGE = (o.isGT || o.isEq) := by decide
+theorem isEq_eq_beq_eq : ∀ {o : Ordering}, o.isEq = (o == .eq) := by decide
+theorem isNe_eq_not_beq_eq : ∀ {o : Ordering}, o.isNe = (!o == .eq) := by decide
+theorem isNe_eq_isLT_or_isGT : ∀ {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide
+
+@[simp] theorem not_isLT_eq_isGE : ∀ {o : Ordering}, !o.isLT = o.isGE := by decide
+@[simp] theorem not_isLE_eq_isGT : ∀ {o : Ordering}, !o.isLE = o.isGT := by decide
+@[simp] theorem not_isGT_eq_isLE : ∀ {o : Ordering}, !o.isGT = o.isLE := by decide
+@[simp] theorem not_isGE_eq_isLT : ∀ {o : Ordering}, !o.isGE = o.isLT := by decide
+@[simp] theorem not_isNe_eq_isEq : ∀ {o : Ordering}, !o.isNe = o.isEq := by decide
+theorem not_isEq_eq_isNe : ∀ {o : Ordering}, !o.isEq = o.isNe := by decide
+
+theorem ne_lt_iff_isGE : ∀ {o : Ordering}, ¬o = .lt ↔ o.isGE := by decide
+theorem ne_gt_iff_isLE : ∀ {o : Ordering}, ¬o = .gt ↔ o.isLE := by decide
+
+@[simp] theorem swap_swap : ∀ {o : Ordering}, o.swap.swap = o := by decide
+@[simp] theorem swap_inj : ∀ {o₁ o₂ : Ordering}, o₁.swap = o₂.swap ↔ o₁ = o₂ := by decide
+
+theorem swap_then : ∀ (o₁ o₂ : Ordering), (o₁.then o₂).swap = o₁.swap.then o₂.swap := by decide
+
+theorem then_eq_lt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by decide
+theorem then_eq_gt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by decide
+@[simp] theorem then_eq_eq : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by decide
+
+theorem isLT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLT = (o₁.isLT || o₁.isEq && o₂.isLT) := by decide
+theorem isEq_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq) := by decide
+theorem isNe_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isNe = (o₁.isNe || o₂.isNe) := by decide
+theorem isGT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGT = (o₁.isGT || o₁.isEq && o₂.isGT) := by decide
+
+@[simp] theorem lt_then {o : Ordering} : lt.then o = lt := rfl
+@[simp] theorem gt_then {o : Ordering} : gt.then o = gt := rfl
+@[simp] theorem eq_then {o : Ordering} : eq.then o = o := rfl
+
+@[simp] theorem then_eq : ∀ {o : Ordering}, o.then eq = o := by decide
+@[simp] theorem then_self : ∀ {o : Ordering}, o.then o = o := by decide
+theorem then_assoc : ∀ (o₁ o₂ o₃ : Ordering), (o₁.then o₂).then o₃ = o₁.then (o₂.then o₃) := by decide
+
+theorem isLE_then_iff_or : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE ↔ o₁ = lt ∨ (o₁ = eq ∧ o₂.isLE) := by decide
+theorem isLE_then_iff_and : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE ↔ o₁.isLE ∧ (o₁ = lt ∨ o₂.isLE) := by decide
+theorem isLE_left_of_isLE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE → o₁.isLE := by decide
+theorem isGE_left_of_isGE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGE → o₁.isGE := by decide
+
+instance : Std.Associative Ordering.then := ⟨then_assoc⟩
+instance : Std.IdempotentOp Ordering.then := ⟨fun _ => then_self⟩
+
+instance : Std.LawfulIdentity Ordering.then eq where
+  left_id _ := eq_then
+  right_id _ := then_eq
 
 end Lemmas
 
@@ -375,7 +335,7 @@ section Lemmas
 @[simp]
 theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
     compareLex cmp₁ cmp₂ a b = .eq ↔ cmp₁ a b = .eq ∧ cmp₂ a b = .eq := by
-  simp [compareLex, Ordering.then_eq_eq]
+  simp [compareLex]
 
 theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
     (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) {x y : α} :
@@ -384,14 +344,14 @@ theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α]
   split
   · rename_i h'
     rw [h] at h'
-    simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
+    simp only [h'.1, h'.2.symm, ↓reduceIte, Ordering.swap_gt]
   · split
     · rename_i h'
       have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
-      simp only [h', this, reduceIte, Ordering.swap_eq]
+      simp only [h', this, ↓reduceIte, Ordering.swap_eq]
     · rename_i h' h''
       replace h' := (h y x).mpr ⟨h', Ne.symm h''⟩
-      simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
+      simp only [h', Ne.symm h'', ↓reduceIte, Ordering.swap_lt]
 
 theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
     {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
@@ -478,13 +438,13 @@ but this is not enforced by the typeclass.
 There is a derive handler, so appending `deriving Ord` to an inductive type or structure
 will attempt to create an `Ord` instance.
 -/
+@[ext]
 class Ord (α : Type u) where
   /-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance. -/
   compare : α → α → Ordering
 
 export Ord (compare)
 
-set_option linter.unusedVariables false in  -- allow specifying `ord` explicitly
 /--
 Compares two values by comparing the results of applying a function.
 
@@ -764,6 +724,13 @@ end Vector
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
+/--
+Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
+`Ordering.eq`.
+-/
+@[expose] def beqOfOrd [Ord α] : BEq α where
+  beq a b := (compare a b).isEq
+
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
@@ -771,8 +738,9 @@ Constructs an `LT` instance from an `Ord` instance that asserts that the result
 @[expose] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
-instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
+@[inline]
+instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
+  decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
@@ -781,35 +749,29 @@ satisfies `Ordering.isLE`.
 @[expose] def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
-instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
+@[inline]
+instance [Ord α] : DecidableRel (@LE.le α leOfOrd) := fun _ _ => instDecidableEqBool ..
 
 namespace Ord
 
 /--
 Constructs a `BEq` instance from an `Ord` instance.
 -/
-protected def toBEq (ord : Ord α) : BEq α where
-  beq x y := ord.compare x y == .eq
+@[expose] protected abbrev toBEq (ord : Ord α) : BEq α :=
+  beqOfOrd
 
 /--
 Constructs an `LT` instance from an `Ord` instance.
 -/
-@[expose] protected def toLT (ord : Ord α) : LT α :=
+@[expose] protected abbrev toLT (ord : Ord α) : LT α :=
   ltOfOrd
 
-instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
-
 /--
 Constructs an `LE` instance from an `Ord` instance.
 -/
-@[expose] protected def toLE (ord : Ord α) : LE α :=
+@[expose] protected abbrev toLE (ord : Ord α) : LE α :=
   leOfOrd
 
-instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
-  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
-
 /--
 Inverts the order of an `Ord` instance.
 
@@ -833,7 +795,7 @@ protected def on (_ : Ord β) (f : α → β) : Ord α where
 /--
 Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
 -/
-protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
+protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
   lexOrd
 
 /--
diff --git a/src/Std/Classes/Ord/Basic.lean b/src/Std/Classes/Ord/Basic.lean
index fbbc9c306eed..fab07820754e 100644
--- a/src/Std/Classes/Ord/Basic.lean
+++ b/src/Std/Classes/Ord/Basic.lean
@@ -75,23 +75,27 @@ instance [OrientedCmp cmp] : ReflCmp cmp where
 instance OrientedCmp.opposite [OrientedCmp cmp] : OrientedCmp fun a b => cmp b a where
   eq_swap := OrientedCmp.eq_swap (cmp := cmp)
 
-instance OrientedOrd.opposite [Ord α] [OrientedOrd α] :
-    letI : Ord α := .opposite inferInstance; OrientedOrd α :=
+instance OrientedOrd.opposite [Ord α] [OrientedOrd α] : letI := Ord.opposite ‹_›; OrientedOrd α :=
   OrientedCmp.opposite (cmp := compare)
 
 theorem OrientedCmp.gt_iff_lt [OrientedCmp cmp] {a b : α} : cmp a b = .gt ↔ cmp b a = .lt := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
   cases cmp b a <;> simp
 
+theorem OrientedCmp.isGT_eq_isLT [OrientedCmp cmp] {a b : α} : (cmp a b).isGT = (cmp b a).isLT := by
+  rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b), Ordering.isGT_swap]
+
 theorem OrientedCmp.lt_of_gt [OrientedCmp cmp] {a b : α} : cmp a b = .gt → cmp b a = .lt :=
   OrientedCmp.gt_iff_lt.1
 
 theorem OrientedCmp.gt_of_lt [OrientedCmp cmp] {a b : α} : cmp a b = .lt → cmp b a = .gt :=
   OrientedCmp.gt_iff_lt.2
 
-theorem OrientedCmp.isGE_iff_isLE [OrientedCmp cmp] {a b : α} : (cmp a b).isGE ↔ (cmp b a).isLE := by
-  rw [OrientedCmp.eq_swap (cmp := cmp)]
-  cases cmp b a <;> simp
+theorem OrientedCmp.isGE_eq_isLE [OrientedCmp cmp] {a b : α} : (cmp a b).isGE = (cmp b a).isLE := by
+  rw [OrientedCmp.eq_swap (cmp := cmp), Ordering.isGE_swap]
+
+theorem OrientedCmp.isGE_iff_isLE [OrientedCmp cmp] {a b : α} : (cmp a b).isGE ↔ (cmp b a).isLE :=
+  Bool.coe_iff_coe.mpr isGE_eq_isLE
 
 theorem OrientedCmp.isLE_of_isGE [OrientedCmp cmp] {a b : α} : (cmp b a).isGE → (cmp a b).isLE :=
   OrientedCmp.isGE_iff_isLE.1
@@ -101,7 +105,7 @@ theorem OrientedCmp.isGE_of_isLE [OrientedCmp cmp] {a b : α} : (cmp b a).isLE 
 
 theorem OrientedCmp.eq_comm [OrientedCmp cmp] {a b : α} : cmp a b = .eq ↔ cmp b a = .eq := by
   rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)]
-  cases cmp b a <;> simp [Ordering.swap]
+  cases cmp b a <;> decide
 
 theorem OrientedCmp.eq_symm [OrientedCmp cmp] {a b : α} : cmp a b = .eq → cmp b a = .eq :=
   OrientedCmp.eq_comm.1
@@ -186,8 +190,7 @@ theorem TransOrd.isGE_trans [Ord α] [TransOrd α] {a b c : α} :
 instance TransCmp.opposite [TransCmp cmp] : TransCmp fun a b => cmp b a where
   isLE_trans := flip TransCmp.isLE_trans
 
-instance TransOrd.opposite [Ord α] [TransOrd α] :
-    letI : Ord α := .opposite inferInstance; TransOrd α :=
+instance TransOrd.opposite [Ord α] [TransOrd α] : letI := Ord.opposite ‹_›; TransOrd α :=
   TransCmp.opposite (cmp := compare)
 
 theorem TransCmp.lt_of_lt_of_eq [TransCmp cmp] {a b c : α} (hab : cmp a b = .lt)
@@ -320,26 +323,28 @@ instance LawfulEqCmp.opposite [OrientedCmp cmp] [LawfulEqCmp cmp] :
     exact LawfulEqCmp.eq_of_compare
 
 instance LawfulEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulEqOrd α] :
-    letI : Ord α := .opposite inferInstance; LawfulEqOrd α :=
+    letI := Ord.opposite ‹_›; LawfulEqOrd α :=
   LawfulEqCmp.opposite (cmp := compare)
 
-@[simp]
-theorem compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b :=
-  ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; exact ReflCmp.compare_self⟩
+theorem LawfulEqCmp.compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b :=
+  ⟨LawfulEqCmp.eq_of_compare, fun h => h ▸ ReflCmp.compare_self⟩
 
-@[grind]
-theorem _root_.Ord.compare_eq_iff_eq [Ord α] [LawfulEqOrd α] (x y : α) :
-    compare x y = .eq ↔ x = y :=
-  Std.compare_eq_iff_eq
+theorem LawfulEqCmp.compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b :=
+  beq_iff_eq.trans compare_eq_iff_eq
 
-@[simp]
-theorem compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b :=
-  ⟨LawfulEqCmp.eq_of_compare ∘ eq_of_beq, by rintro rfl; simp⟩
+/-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_eq_iff_eq` -/
+@[simp, grind]
+theorem LawfulEqOrd.compare_eq_iff_eq [Ord α] [LawfulEqOrd α] {a b : α} :
+    compare a b = .eq ↔ a = b :=
+  LawfulEqCmp.compare_eq_iff_eq
 
-@[grind]
-theorem _root_.Ord.compare_beq_iff_eq [Ord α] [LawfulEqOrd α] (x y : α) :
-    compare x y == .eq ↔ x = y :=
-  Std.compare_beq_iff_eq
+/-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_beq_iff_eq` -/
+@[simp, grind]
+theorem LawfulEqOrd.compare_beq_iff_eq [Ord α] [LawfulEqOrd α] {a b : α} :
+    compare a b == .eq ↔ a = b :=
+  LawfulEqCmp.compare_beq_iff_eq
+
+export LawfulEqOrd (compare_eq_iff_eq compare_beq_iff_eq)
 
 end LawfulEq
 
@@ -353,7 +358,7 @@ This typeclass distinguishes itself from `LawfulEqCmp` by using boolean equality
 logical equality (`=`).
 -/
 class LawfulBEqCmp {α : Type u} [BEq α] (cmp : α → α → Ordering) : Prop where
-  /-- If two values compare equal, then they are logically equal. -/
+  /-- If two values compare equal, then they are boolean equal. -/
   compare_eq_iff_beq {a b : α} : cmp a b = .eq ↔ a == b
 
 theorem LawfulBEqCmp.not_compare_eq_iff_beq_eq_false {α : Type u} [BEq α] {cmp}
@@ -361,6 +366,14 @@ theorem LawfulBEqCmp.not_compare_eq_iff_beq_eq_false {α : Type u} [BEq α] {cmp
   rw [Bool.eq_false_iff, ne_eq, not_congr]
   exact compare_eq_iff_beq
 
+theorem LawfulBEqCmp.compare_beq_eq_beq {α : Type u} [BEq α] {cmp}
+    [LawfulBEqCmp (α := α) cmp] {a b : α} : (cmp a b == .eq) = (a == b) := by
+  rw [Bool.eq_iff_iff, beq_iff_eq, compare_eq_iff_beq]
+
+theorem LawfulBEqCmp.isEq_compare_eq_beq {α : Type u} [BEq α] {cmp}
+    [LawfulBEqCmp (α := α) cmp] {a b : α} : (cmp a b).isEq = (a == b) := by
+  rw [Bool.eq_iff_iff, Ordering.isEq_iff_eq_eq, compare_eq_iff_beq]
+
 /--
 A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if
 the boolean equality `a == b` holds.
@@ -380,14 +393,25 @@ theorem LawfulBEqOrd.not_compare_eq_iff_beq_eq_false {α : Type u} {_ : BEq α}
     [LawfulBEqOrd α] {a b : α} : ¬ compare a b = .eq ↔ (a == b) = false :=
   LawfulBEqCmp.not_compare_eq_iff_beq_eq_false
 
-export LawfulBEqOrd (compare_eq_iff_beq not_compare_eq_iff_beq_eq_false)
+theorem LawfulBEqOrd.compare_beq_eq_beq {α : Type u} {_ : Ord α} {_ : BEq α}
+    [LawfulBEqOrd α] {a b : α} : (compare a b == .eq) = (a == b) :=
+  LawfulBEqCmp.compare_beq_eq_beq
 
-instance [LawfulEqCmp cmp] [LawfulBEq α] :
-    LawfulBEqCmp cmp where
-  compare_eq_iff_beq := compare_eq_iff_eq.trans beq_iff_eq.symm
+theorem LawfulBEqOrd.isEq_compare_eq_beq {α : Type u} {_ : Ord α} {_ : BEq α}
+    [LawfulBEqOrd α] {a b : α} : (compare a b).isEq = (a == b) :=
+  LawfulBEqCmp.isEq_compare_eq_beq
 
-theorem LawfulBEqCmp.equivBEq [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBEq α where
+export LawfulBEqOrd (compare_eq_iff_beq not_compare_eq_iff_beq_eq_false
+  compare_beq_eq_beq isEq_compare_eq_beq)
+
+instance [LawfulEqCmp cmp] [LawfulBEq α] : LawfulBEqCmp cmp where
+  compare_eq_iff_beq := LawfulEqCmp.compare_eq_iff_eq.trans beq_iff_eq.symm
+
+theorem LawfulBEqCmp.reflBEq [inst : LawfulBEqCmp cmp] [ReflCmp cmp] : ReflBEq α where
   rfl := inst.compare_eq_iff_beq.mp ReflCmp.compare_self
+
+theorem LawfulBEqCmp.equivBEq [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBEq α where
+  toReflBEq := reflBEq (cmp := cmp)
   symm := by
     simp only [← inst.compare_eq_iff_beq]
     exact OrientedCmp.eq_symm
@@ -399,8 +423,8 @@ instance LawfulBEqOrd.equivBEq [Ord α] [LawfulBEqOrd α] [TransOrd α] : EquivB
   LawfulBEqCmp.equivBEq (cmp := compare)
 
 theorem LawfulBEqCmp.lawfulBEq [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : LawfulBEq α where
-  rfl := by simp [← inst.compare_eq_iff_beq, compare_eq_iff_eq]
-  eq_of_beq := by simp [← inst.compare_eq_iff_beq, compare_eq_iff_eq]
+  toReflBEq := reflBEq (cmp := cmp)
+  eq_of_beq := by simp [← inst.compare_eq_iff_beq, LawfulEqCmp.compare_eq_iff_eq]
 
 instance LawfulBEqOrd.lawfulBEq [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α :=
   LawfulBEqCmp.lawfulBEq (cmp := compare)
@@ -418,54 +442,22 @@ instance LawfulBEqCmp.opposite [OrientedCmp cmp] [LawfulBEqCmp cmp] :
     simp [OrientedCmp.eq_comm (cmp := cmp), LawfulBEqCmp.compare_eq_iff_beq]
 
 instance LawfulBEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulBEqOrd α] :
-    letI : Ord α := .opposite inferInstance; LawfulBEqOrd α :=
+    letI := Ord.opposite ‹_›; LawfulBEqOrd α :=
   LawfulBEqCmp.opposite (cmp := compare)
 
 end LawfulBEq
 
-namespace Internal
-
-variable {α : Type u}
+attribute [local instance] beqOfOrd in
+instance {α : Type u} {_ : Ord α} : LawfulBEqOrd α where
+  compare_eq_iff_beq {a b} := by simp only [beqOfOrd, Ordering.isEq_iff_eq_eq]
 
-/--
-Internal function to derive a `BEq` instance from an `Ord` instance in order to connect the
-verification machinery for tree maps to the verification machinery for hash maps.
--/
-@[local instance]
-def beqOfOrd [Ord α] : BEq α where
-  beq a b := compare a b = .eq
-
-instance {_ : Ord α} : LawfulBEqOrd α where
-  compare_eq_iff_beq {a b} := by simp only [beqOfOrd, decide_eq_true_eq]
-
-@[local simp]
-theorem beq_eq [Ord α] {a b : α} : (a == b) = (compare a b = .eq) := by
-  rw [compare_eq_iff_beq]
-
-theorem beq_iff [Ord α] {a b : α} : (a == b) = true ↔ compare a b = .eq :=
-  eq_iff_iff.mp beq_eq
-
-theorem eq_beqOfOrd_of_lawfulBEqOrd [Ord α] (inst : BEq α) [instLawful : LawfulBEqOrd α] :
-    inst = beqOfOrd := by
-  cases inst; rename_i instBEq
-  congr; ext a b
-  rw [Bool.eq_iff_iff, decide_eq_true_eq, instLawful.compare_eq_iff_beq]
-  rfl
-
-theorem equivBEq_of_transOrd [Ord α] [TransOrd α] : EquivBEq α where
-  symm {a b} h := by simp_all [OrientedCmp.eq_comm]
-  trans h₁ h₂ := by simp_all only [beq_eq, beq_iff_eq]; exact TransCmp.eq_trans h₁ h₂
-  rfl := by simp only [beq_eq, beq_iff_eq]; exact compare_self
-
-theorem lawfulBEq_of_lawfulEqOrd [Ord α] [LawfulEqOrd α] : LawfulBEq α where
-  eq_of_beq hbeq := by simp_all
-  rfl := by simp
-
-end Internal
+end Std
 
 section Instances
 
-theorem TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff
+open Std
+
+theorem Std.TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff
     {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
     (lt_trans : ∀ {a b c : α}, a < b → b < c → a < c)
     (h : ∀ x y : α, x < y ↔ ¬ y < x ∧ x ≠ y) :
@@ -481,7 +473,7 @@ theorem TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff
       · exact .inl h₁
     · exact h₂
 
-theorem TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
+theorem Std.TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
     {α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableLE α] [DecidableEq α]
     (antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y)
     (trans : ∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ z) (total : ∀ (x y : α), x ≤ y ∨ y ≤ x)
@@ -559,14 +551,16 @@ instance {α} [Ord α] [ReflOrd α] : ReflOrd (Option α) where
 
 instance {α} [Ord α] [LawfulEqOrd α] : LawfulEqOrd (Option α) where
   eq_of_compare {a b} := by
-    cases a <;> cases b <;> simp_all [Ord.compare, LawfulEqOrd.eq_of_compare]
+    cases a <;> cases b <;> simp [Ord.compare, compare_eq_iff_eq]
 
 instance {α} [Ord α] [BEq α] [LawfulBEqOrd α] : LawfulBEqOrd (Option α) where
   compare_eq_iff_beq {a b} := by
-    cases a <;> cases b <;> simp_all [Ord.compare, LawfulBEqOrd.compare_eq_iff_beq]
+    cases a <;> cases b <;> simp [Ord.compare, compare_eq_iff_beq]
 
 end Option
 
+namespace Std
+
 section Lex
 
 instance {α} {cmp₁ cmp₂} [ReflCmp cmp₁] [ReflCmp cmp₂] :
@@ -629,10 +623,10 @@ instance {α β} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] : LawfulEqO
 
 end Lex
 
-end Instances
-
 end Std
 
+end Instances
+
 namespace List
 
 open Std
@@ -653,8 +647,8 @@ instance [LawfulEqCmp cmp] : LawfulEqCmp (List.compareLex cmp) where
     | cons x xs ih =>
       cases b
       · simp [List.compareLex_nil_right_eq_eq] at h
-      · simp only [List.compareLex_cons_cons, Ordering.then_eq_eq, compare_eq_iff_eq,
-        List.cons.injEq] at *
+      · simp only [List.compareLex_cons_cons, Ordering.then_eq_eq, LawfulEqCmp.compare_eq_iff_eq,
+          List.cons.injEq] at *
         exact ⟨h.1, ih h.2⟩
 
 instance [BEq α] [LawfulBEqCmp cmp] : LawfulBEqCmp (List.compareLex cmp) where
@@ -721,7 +715,7 @@ instance [ReflCmp cmp] : ReflCmp (Array.compareLex cmp) where
 
 instance [LawfulEqCmp cmp] : LawfulEqCmp (Array.compareLex cmp) where
   eq_of_compare {a b} := by
-    simp only [Array.compareLex_eq_compareLex_toList, compare_eq_iff_eq]
+    simp only [Array.compareLex_eq_compareLex_toList, LawfulEqCmp.compare_eq_iff_eq]
     exact congrArg List.toArray
 
 instance [BEq α] [LawfulBEqCmp cmp] : LawfulBEqCmp (Array.compareLex cmp) where
diff --git a/src/Std/Classes/Ord/Vector.lean b/src/Std/Classes/Ord/Vector.lean
index 73f165d8998c..7d2a5c5c1bae 100644
--- a/src/Std/Classes/Ord/Vector.lean
+++ b/src/Std/Classes/Ord/Vector.lean
@@ -27,7 +27,7 @@ instance [ReflCmp cmp] {n} : ReflCmp (Vector.compareLex cmp (n := n)) where
   compare_self := ReflCmp.compare_self (cmp := Array.compareLex cmp)
 
 instance [LawfulEqCmp cmp] {n} : LawfulEqCmp (Vector.compareLex cmp (n := n)) where
-  eq_of_compare := by simp [Vector.compareLex_eq_compareLex_toArray]
+  eq_of_compare := by simp [Vector.compareLex_eq_compareLex_toArray, LawfulEqCmp.compare_eq_iff_eq]
 
 instance [BEq α] [LawfulBEqCmp cmp] {n} : LawfulBEqCmp (Vector.compareLex cmp (n := n)) where
   compare_eq_iff_beq := by simp [Vector.compareLex_eq_compareLex_toArray,
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index 5292598a9972..eb95b4dbdc31 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -28,8 +28,6 @@ variable {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β}
 private local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ
 
 attribute [local instance low] beqOfOrd
-attribute [local instance] equivBEq_of_transOrd
-attribute [local instance] lawfulBEq_of_lawfulEqOrd
 
 /-- Internal implementation detail of the tree map -/
 scoped syntax "wf_trivial" : tactic
@@ -55,7 +53,8 @@ theorem compare_ne_iff_beq_eq_false {a b : α} :
   simp only [ne_eq, compare_eq_iff_beq, Bool.not_eq_true]
 
 private def helperLemmaNames : Array Name :=
-  #[``compare_eq_iff_beq, ``compare_ne_iff_beq_eq_false, ``Bool.not_eq_true, ``mem_iff_contains]
+  #[``compare_eq_iff_beq, ``compare_beq_eq_beq, ``compare_ne_iff_beq_eq_false,
+    ``Bool.not_eq_true, ``mem_iff_contains]
 
 private def modifyMap : Std.HashMap Name Name :=
   .ofList
@@ -406,16 +405,16 @@ theorem isEmpty_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
   simpa only [insertIfNew_eq_insertIfNew!] using isEmpty_insertIfNew h
 
 theorem contains_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
-    (t.insertIfNew k v h.balanced).impl.contains a = (k == a || t.contains a) := by
+    (t.insertIfNew k v h.balanced).impl.contains a = (compare k a == .eq || t.contains a) := by
   simp_to_model [insertIfNew, contains] using List.containsKey_insertEntryIfNew
 
 theorem contains_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
-    (t.insertIfNew! k v).contains a = (k == a || t.contains a) := by
+    (t.insertIfNew! k v).contains a = (compare k a == .eq || t.contains a) := by
   simpa only [insertIfNew_eq_insertIfNew!] using contains_insertIfNew h
 
 theorem mem_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
     a ∈ (t.insertIfNew k v h.balanced).impl ↔ compare k a = .eq ∨ a ∈ t := by
-  simp [mem_iff_contains, contains_insertIfNew, h, beq_eq]
+  simp [mem_iff_contains, contains_insertIfNew, h, compare_eq_iff_beq]
 
 theorem mem_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
     a ∈ t.insertIfNew! k v ↔ compare k a = .eq ∨ a ∈ t := by
@@ -2389,8 +2388,7 @@ theorem get_insertMany!_list_of_mem [TransOrd α] (h : t.WF)
   simpa only [insertMany_eq_insertMany!] using get_insertMany_list_of_mem h
 
 /-- A variant of `contains_of_contains_insertMany_list` used in `get_insertMany_list`. -/
--- This should not really need `PartialEquivBEq`, but fixing it would require many changes.
-theorem contains_of_contains_insertMany_list' [TransOrd α] [BEq α] [PartialEquivBEq α] [LawfulBEqOrd α] (h : t.WF)
+theorem contains_of_contains_insertMany_list' [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
     {l : List (α × β)} {k : α}
     (h' : contains k (insertMany t l h.balanced).val = true)
     (w : l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none) = none) :
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index d96e58617254..a172e8458a7e 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -375,7 +375,7 @@ theorem exists_cell_of_updateCell [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd
   · conv => lhs; rw [toListModel_updateCell hlb hlo]
     simpa using List.perm_append_comm_assoc _ _ _
   · rw [containsKey_eq_false_iff_forall_mem_keys, keys_eq_map]
-    simp only [List.map_append, List.mem_append, List.mem_map, List.mem_filter, beq_iff_eq, beq_eq,
+    simp only [List.map_append, List.mem_append, List.mem_map, List.mem_filter, beq_iff_eq,
       beq_eq_false_iff_ne, ne_eq]
     rintro a (⟨p, ⟨⟨-, hp⟩, rfl⟩⟩|⟨p, ⟨⟨-, hp⟩, rfl⟩⟩) <;>
       simp_all [← not_compare_eq_iff_beq_eq_false]
@@ -477,8 +477,7 @@ theorem containsKey_toListModel [Ord α] [OrientedOrd α] [BEq α] [LawfulBEqOrd
   simp [containsKey_eq_true_iff_exists_mem]
   induction l
   · rename_i sz k' v' l r ih₁ ih₂
-    simp only [toListModel_inner, containsKey_append, containsKey_cons, beq_eq, Bool.or_eq_true,
-      beq_iff_eq]
+    simp only [toListModel_inner]
     rw [contains'] at h
     split at h <;> rename_i hcmp
     · obtain ⟨p, hp₁, hp₂⟩ := ih₁ h
@@ -534,7 +533,7 @@ theorem applyCell_eq_apply_toListModel [Ord α] [TransOrd α] [BEq α] [LawfulBE
     simp only [List.append_assoc]; exact List.perm_append_comm_assoc ll c.inner.toList rr
   rw [hfg, hg₁ _ _ _ _ hperm, hg]
   · simp only [containsKey_append, Bool.or_eq_false_iff, containsKey_eq_false_iff_forall_mem_keys,
-      keys_eq_map, List.mem_map, beq_eq, beq_eq_false_iff_ne, ne_eq, forall_exists_index, and_imp,
+      keys_eq_map, List.mem_map, beq_eq_false_iff_ne, forall_exists_index, and_imp,
       forall_apply_eq_imp_iff₂]
     exact ⟨fun p hp => by simp [hll p hp, ← not_compare_eq_iff_beq_eq_false],
       fun p hp => by simp [hrr p hp, ← not_compare_eq_iff_beq_eq_false]⟩
@@ -597,7 +596,7 @@ theorem get?ₘ_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α
   rw [get?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => getValueCast? k l)]
   · rintro ⟨(_|p), hp⟩ -
     · simp [Cell.get?]
-    · simp only [Cell.get?, Option.toList_some, getValueCast?, beq_eq, ← compare_eq_iff_beq,
+    · simp only [Cell.get?, Option.toList_some, getValueCast?, ← compare_eq_iff_beq,
         compare_eq_iff_eq, Option.some_eq_dite_none_right, exists_prop, and_true]
       simp [compare_eq_iff_eq.mp (hp p rfl)]
   · exact fun l₁ l₂ h => getValueCast?_of_perm
@@ -663,7 +662,7 @@ theorem getKey?ₘ_eq_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
   rw [getKey?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => List.getKey? k l)]
   · rintro ⟨(_|p), hp⟩ -
     · simp [Cell.getKey?]
-    · simp only [Cell.getKey?, Option.toList_some, List.getKey?, beq_eq,
+    · simp only [Cell.getKey?, Option.toList_some, List.getKey?,
         compare_eq_iff_eq, Option.some_eq_dite_none_right, exists_prop, and_true]
       simp [BEq.symm <| compare_eq_iff_beq.mp (hp p rfl)]
   · exact fun l₁ l₂ h => List.getKey?_of_perm
@@ -733,7 +732,7 @@ theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
   rw [get?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => getValue? k l)]
   · rintro ⟨(_|p), hp⟩ -
     · simp [Cell.Const.get?]
-    · simp only [Cell.Const.get?, Option.toList_some, getValue?, beq_eq,
+    · simp only [Cell.Const.get?, Option.toList_some, getValue?,
         compare_eq_iff_eq, Option.some_eq_dite_none_right, exists_prop, and_true]
       simp [BEq.symm <| compare_eq_iff_beq.mp (hp p rfl)]
   · exact fun l₁ l₂ h => getValue?_of_perm
@@ -1320,7 +1319,7 @@ theorem toListModel_alterₘ [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {
     cases f none <;> rfl
   · simp only [Cell.Const.alter, Cell.ofOption, Const.alterKey, Option.toList_some]
     have := OrientedCmp.eq_symm <| hl l rfl
-    simp only [getValue?, beq_eq, compare_eq_iff_beq.mp this, beq_self_eq_true, cond_eq_if,
+    simp only [getValue?, compare_eq_iff_beq.mp this, beq_self_eq_true, cond_eq_if,
       reduceIte]
     cases f _
     · simp [eraseKey, compare_eq_iff_beq.mp this]
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index ed56c825e527..c66362f30991 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -223,7 +223,7 @@ theorem get?_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
 
 theorem get?_insert [TransCmp cmp] [LawfulEqCmp cmp] {a k : α} {v : β k} :
     (t.insert k v).get? a =
-      if h : cmp k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a :=
+      if h : cmp k a = .eq then some (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v) else t.get? a :=
   Impl.get?_insert t.wf
 
 @[simp]
@@ -336,7 +336,7 @@ end Const
 theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁} :
     (t.insert k v).get a h₁ =
       if h₂ : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h₂)) v
       else
         t.get a (mem_of_mem_insert h₁ h₂) :=
   Impl.get_insert t.wf
@@ -399,7 +399,7 @@ theorem get!_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β
 
 theorem get!_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
     (t.insert k v).get! a =
-      if h : cmp k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a :=
+      if h : cmp k a = .eq then cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v else t.get! a :=
   Impl.get!_insert t.wf
 
 @[simp]
@@ -516,7 +516,7 @@ theorem getD_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β
 theorem getD_insert [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
     (t.insert k v).getD a fallback =
       if h : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v
       else t.getD a fallback :=
   Impl.getD_insert t.wf
 
@@ -924,7 +924,7 @@ theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} :
 theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} :
     (t.insertIfNew k v).get? a =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+        some (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v)
       else
         t.get? a :=
   Impl.get?_insertIfNew t.wf
@@ -932,7 +932,7 @@ theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k}
 theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁} :
     (t.insertIfNew k v).get a h₁ =
       if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h₂.1)) v
       else
         t.get a (mem_of_mem_insertIfNew' h₁ h₂) :=
   Impl.get_insertIfNew t.wf
@@ -940,7 +940,7 @@ theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {
 theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
     (t.insertIfNew k v).get! a =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v
       else
         t.get! a :=
   Impl.get!_insertIfNew t.wf
@@ -948,7 +948,7 @@ theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited
 theorem getD_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
     (t.insertIfNew k v).getD a fallback =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v
       else
         t.getD a fallback :=
   Impl.getD_insertIfNew t.wf
@@ -1323,7 +1323,7 @@ theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cm
 theorem get?_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
+    (t.insertMany l).get? k' = some (cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v) :=
   Impl.get?_insertMany_list_of_mem t.wf k_eq distinct mem
 
 theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
@@ -1340,7 +1340,7 @@ theorem get_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l)
     {h'} :
-    (t.insertMany l).get k' h' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).get k' h' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get_insertMany_list_of_mem t.wf k_eq distinct mem
 
 theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp]
@@ -1354,7 +1354,7 @@ theorem get!_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).get! k' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get!_insertMany_list_of_mem t.wf k_eq distinct mem
 
 theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
@@ -1368,7 +1368,7 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).getD k' fallback = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.getD_insertMany_list_of_mem t.wf k_eq distinct mem
 
 theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1813,7 +1813,7 @@ theorem get?_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
+    (ofList l cmp).get? k' = some (cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v) :=
   Impl.get?_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
@@ -1821,7 +1821,7 @@ theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
-    (ofList l cmp).get k' h = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).get k' h = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1834,7 +1834,7 @@ theorem get!_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).get! k' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get!_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1847,7 +1847,7 @@ theorem getD_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).getD k' fallback = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.getD_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -2264,7 +2264,7 @@ theorem get?_alter [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α}
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get? k' =
       if h : cmp k k' = .eq then
-        cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) (f (t.get? k))
+        cast (congrArg (Option ∘ β) (LawfulEqCmp.compare_eq_iff_eq.mp h)) (f (t.get? k))
       else
         t.get? k' :=
   Impl.get?_alter t.wf
@@ -2273,14 +2273,14 @@ theorem get?_alter [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α}
 theorem get?_alter_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α}
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get? k = f (t.get? k) := by
-  simp [get?_alter]
+  simp [get?_alter, ReflCmp.compare_self]
 
 theorem get_alter [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α}
     {f : Option (β k) → Option (β k)} {hc : k' ∈ (t.alter k f)} :
     (t.alter k f).get k' hc =
       if heq : cmp k k' = .eq then
         haveI h' : (f (t.get? k)).isSome := mem_alter_of_compare_eq heq |>.mp hc
-        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| (f (t.get? k)).get <| h'
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq)) <| (f (t.get? k)).get <| h'
       else
         haveI h' : k' ∈ t := mem_alter_of_not_compare_eq heq |>.mp hc
         t.get k' h' :=
@@ -2297,7 +2297,7 @@ theorem get!_alter [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} [Inhabited (β k
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get! k' =
       if heq : cmp k k' = .eq then
-        (f (t.get? k)).map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+        (f (t.get? k)).map (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq))) |>.get!
       else
         t.get! k' :=
   Impl.get!_alter t.wf
@@ -2312,7 +2312,7 @@ theorem getD_alter [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {fallback : β k
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).getD k' fallback =
       if heq : cmp k k' = .eq then
-        f (t.get? k) |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+        f (t.get? k) |>.map (cast (congrArg β <| LawfulEqCmp.compare_eq_iff_eq.mp heq)) |>.getD fallback
       else
         t.getD k' fallback :=
   Impl.getD_alter t.wf
@@ -2615,7 +2615,7 @@ theorem size_modify {k : α} {f : β k → β k} :
 theorem get?_modify {k k' : α} {f : β k → β k} :
     (t.modify k f).get? k' =
       if h : cmp k k' = .eq then
-        (cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) ((t.get? k).map f))
+        (cast (congrArg (Option ∘ β) (LawfulEqCmp.compare_eq_iff_eq.mp h)) ((t.get? k).map f))
       else
         t.get? k' :=
   Impl.get?_modify t.wf
@@ -2629,7 +2629,7 @@ theorem get_modify {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f} :
     (t.modify k f).get k' hc =
       if heq : cmp k k' = .eq then
         haveI h' : k ∈ t := mem_congr heq |>.mpr <| mem_modify.mp hc
-        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| f (t.get k h')
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq)) <| f (t.get k h')
       else
         haveI h' : k' ∈ t := mem_modify.mp hc
         t.get k' h' :=
@@ -2644,7 +2644,7 @@ theorem get_modify_self {k : α} {f : β k → β k} {hc : k ∈ t.modify k f} :
 theorem get!_modify {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
     (t.modify k f).get! k' =
       if heq : cmp k k' = .eq then
-        t.get? k |>.map f |>.map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+        t.get? k |>.map f |>.map (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq))) |>.get!
       else
         t.get! k' :=
   Impl.get!_modify t.wf
@@ -2657,7 +2657,7 @@ theorem get!_modify_self {k : α} [Inhabited (β k)] {f : β k → β k} :
 theorem getD_modify {k k' : α} {fallback : β k'} {f : β k → β k} :
     (t.modify k f).getD k' fallback =
       if heq : cmp k k' = .eq then
-        t.get? k |>.map f |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+        t.get? k |>.map f |>.map (cast (congrArg β <| LawfulEqCmp.compare_eq_iff_eq.mp heq)) |>.getD fallback
       else
         t.getD k' fallback :=
   Impl.getD_modify t.wf
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 21fa9bab1aca..79b951f92aed 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -224,7 +224,7 @@ theorem get?_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
 
 theorem get?_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a k : α} {v : β k} :
     (t.insert k v).get? a =
-      if h : cmp k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a :=
+      if h : cmp k a = .eq then some (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v) else t.get? a :=
   Impl.get?_insert! h
 
 @[simp]
@@ -337,7 +337,7 @@ end Const
 theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
     (t.insert k v).get a h₁ =
       if h₂ : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h₂)) v
       else
         t.get a (mem_of_mem_insert h h₁ h₂) :=
   Impl.get_insert! h
@@ -401,7 +401,7 @@ theorem get!_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} [In
 
 theorem get!_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} [Inhabited (β a)]
     {v : β k} : (t.insert k v).get! a =
-      if h : cmp k a = .eq then cast (congrArg β (compare_eq_iff_eq.mp h)) v else t.get! a :=
+      if h : cmp k a = .eq then cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v else t.get! a :=
   Impl.get!_insert! h
 
 @[simp]
@@ -519,7 +519,7 @@ theorem getD_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} {fa
 theorem getD_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
     (t.insert k v).getD a fallback =
       if h : cmp k a = .eq then
-        cast (congrArg β (compare_eq_iff_eq.mp h)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h)) v
       else t.getD a fallback :=
   Impl.getD_insert! h
 
@@ -928,7 +928,7 @@ theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
 theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} :
     (t.insertIfNew k v).get? a =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+        some (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v)
       else
         t.get? a :=
   Impl.get?_insertIfNew! h
@@ -936,7 +936,7 @@ theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α}
 theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
     (t.insertIfNew k v).get a h₁ =
       if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h₂.1)) v
       else
         t.get a (mem_of_mem_insertIfNew' h h₁ h₂) :=
   Impl.get_insertIfNew! h
@@ -944,7 +944,7 @@ theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {
 theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
     (t.insertIfNew k v).get! a =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v
       else
         t.get! a :=
   Impl.get!_insertIfNew! h
@@ -952,7 +952,7 @@ theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α}
 theorem getD_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
     (t.insertIfNew k v).getD a fallback =
       if h : cmp k a = .eq ∧ ¬ k ∈ t then
-        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp h.1)) v
       else
         t.getD a fallback :=
   Impl.getD_insertIfNew! h
@@ -1330,7 +1330,7 @@ theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cm
 theorem get?_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
+    (t.insertMany l).get? k' = some (cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v) :=
   Impl.get?_insertMany!_list_of_mem h k_eq distinct mem
 
 theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
@@ -1347,7 +1347,7 @@ theorem get_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l)
     {h'} :
-    (t.insertMany l).get k' h' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).get k' h' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get_insertMany!_list_of_mem h k_eq distinct mem
 
 theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp]
@@ -1361,7 +1361,7 @@ theorem get!_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).get! k' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get!_insertMany!_list_of_mem h k_eq distinct mem
 
 theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
@@ -1375,7 +1375,7 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (t.insertMany l).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (t.insertMany l).getD k' fallback = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.getD_insertMany!_list_of_mem h k_eq distinct mem
 
 theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1843,7 +1843,7 @@ theorem get?_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
+    (ofList l cmp).get? k' = some (cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v) :=
   Impl.get?_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
@@ -1851,7 +1851,7 @@ theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
-    (ofList l cmp).get k' h = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).get k' h = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1864,7 +1864,7 @@ theorem get!_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).get! k' = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.get!_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -1877,7 +1877,7 @@ theorem getD_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
     {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
     (mem : ⟨k, v⟩ ∈ l) :
-    (ofList l cmp).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
+    (ofList l cmp).getD k' fallback = cast (by congr; apply LawfulEqCmp.compare_eq_iff_eq.mp k_eq) v :=
   Impl.getD_insertMany_empty_list_of_mem k_eq distinct mem
 
 theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -2295,7 +2295,7 @@ theorem get?_alter [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k k' : α}
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get? k' =
       if h : cmp k k' = .eq then
-        cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) (f (t.get? k))
+        cast (congrArg (Option ∘ β) (LawfulEqCmp.compare_eq_iff_eq.mp h)) (f (t.get? k))
       else
         t.get? k' :=
   Impl.get?_alter! h
@@ -2304,14 +2304,14 @@ theorem get?_alter [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k k' : α}
 theorem get?_alter_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α}
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get? k = f (t.get? k) := by
-  simp [get?_alter h]
+  simp [get?_alter h, ReflCmp.compare_self]
 
 theorem get_alter [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k k' : α}
     {f : Option (β k) → Option (β k)} {hc : k' ∈ (t.alter k f)} :
     (t.alter k f).get k' hc =
       if heq : cmp k k' = .eq then
         haveI h' : (f (t.get? k)).isSome := mem_alter_of_compare_eq h heq |>.mp hc
-        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| (f (t.get? k)).get <| h'
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq)) <| (f (t.get? k)).get <| h'
       else
         haveI h' : k' ∈ t := mem_alter_of_not_compare_eq h heq |>.mp hc
         t.get k' h' :=
@@ -2328,7 +2328,7 @@ theorem get!_alter [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k k' : α} [Inha
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).get! k' =
       if heq : cmp k k' = .eq then
-        (f (t.get? k)).map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+        (f (t.get? k)).map (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq))) |>.get!
       else
         t.get! k' :=
   Impl.get!_alter! h
@@ -2343,7 +2343,7 @@ theorem getD_alter [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k k' : α} {fall
     {f : Option (β k) → Option (β k)} :
     (t.alter k f).getD k' fallback =
       if heq : cmp k k' = .eq then
-        f (t.get? k) |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+        f (t.get? k) |>.map (cast (congrArg β <| LawfulEqCmp.compare_eq_iff_eq.mp heq)) |>.getD fallback
       else
         t.getD k' fallback :=
   Impl.getD_alter! h
@@ -2646,7 +2646,7 @@ theorem size_modify (h : t.WF) {k : α} {f : β k → β k} :
 theorem get?_modify (h : t.WF) {k k' : α} {f : β k → β k} :
     (t.modify k f).get? k' =
       if h : cmp k k' = .eq then
-        (cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) ((t.get? k).map f))
+        (cast (congrArg (Option ∘ β) (LawfulEqCmp.compare_eq_iff_eq.mp h)) ((t.get? k).map f))
       else
         t.get? k' :=
   Impl.get?_modify h
@@ -2660,7 +2660,7 @@ theorem get_modify (h : t.WF) {k k' : α} {f : β k → β k} {hc : k' ∈ t.mod
     (t.modify k f).get k' hc =
       if heq : cmp k k' = .eq then
         haveI h' : k ∈ t := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
-        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| f (t.get k h')
+        cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq)) <| f (t.get k h')
       else
         haveI h' : k' ∈ t := (mem_modify h).mp hc
         t.get k' h' :=
@@ -2675,7 +2675,7 @@ theorem get_modify_self (h : t.WF) {k : α} {f : β k → β k} {hc : k ∈ t.mo
 theorem get!_modify (h : t.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
     (t.modify k f).get! k' =
       if heq : cmp k k' = .eq then
-        t.get? k |>.map f |>.map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+        t.get? k |>.map f |>.map (cast (congrArg β (LawfulEqCmp.compare_eq_iff_eq.mp heq))) |>.get!
       else
         t.get! k' :=
   Impl.get!_modify h
@@ -2688,7 +2688,7 @@ theorem get!_modify_self (h : t.WF) {k : α} [Inhabited (β k)] {f : β k → β
 theorem getD_modify (h : t.WF) {k k' : α} {fallback : β k'} {f : β k → β k} :
     (t.modify k f).getD k' fallback =
       if heq : cmp k k' = .eq then
-        t.get? k |>.map f |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+        t.get? k |>.map f |>.map (cast (congrArg β <| LawfulEqCmp.compare_eq_iff_eq.mp heq)) |>.getD fallback
       else
         t.getD k' fallback :=
   Impl.getD_modify h