From fa48d7924e37d13a2e2dd15b20dca6c50600610d Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 25 Feb 2025 09:29:55 +0100
Subject: [PATCH 1/2] replace bad catch-all simp lemma

---
 src/Std/Classes/Ord.lean                 | 13 ++++++++-----
 src/Std/Data/DTreeMap/Internal/Cell.lean |  2 +-
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean
index 5b17a3532f8b..8498dd447500 100644
--- a/src/Std/Classes/Ord.lean
+++ b/src/Std/Classes/Ord.lean
@@ -28,12 +28,15 @@ class ReflCmp {α : Type u} (cmp : α → α → Ordering) : Prop where
   /-- Comparison is reflexive. -/
   compare_self {a : α} : cmp a a = .eq
 
-export ReflCmp (compare_self)
-
 /-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
-attribute [simp] compare_self
+theorem ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} : compare a a = .eq :=
+    ReflCmp.compare_self
+
+attribute [simp] ReflOrd.compare_self
+
+export ReflOrd (compare_self)
 
 end Refl
 
@@ -266,7 +269,7 @@ variable {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp]
 
 @[simp]
 theorem compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b :=
-  ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; simp⟩
+  ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; exact ReflCmp.compare_self⟩
 
 @[simp]
 theorem compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b :=
@@ -293,7 +296,7 @@ theorem beq_eq [Ord α] {a b : α} : (a == b) = (compare a b == .eq) :=
 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₂
-  refl := by simp
+  refl := 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
diff --git a/src/Std/Data/DTreeMap/Internal/Cell.lean b/src/Std/Data/DTreeMap/Internal/Cell.lean
index 7f9e712017a9..3ffd990507a2 100644
--- a/src/Std/Data/DTreeMap/Internal/Cell.lean
+++ b/src/Std/Data/DTreeMap/Internal/Cell.lean
@@ -43,7 +43,7 @@ def ofEq [Ord α] {k : α → Ordering} (k' : α) (v' : β k') (hcmp : ∀ [Orie
 
 /-- Create a cell with a matching key. Internal implementation detail of the tree map -/
 def of [Ord α] (k : α) (v : β k) : Cell α β (compare k) :=
-  .ofEq k v (by intro; simp)
+  .ofEq k v compare_self
 
 @[simp]
 theorem ofEq_inner [Ord α] {k : α → Ordering} {k' : α} {v' : β k'} {h} :

From 42691c76f3c8b07d68936e36c555d68c04de564a Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 25 Feb 2025 10:45:34 +0100
Subject: [PATCH 2/2] apply suggestion

---
 src/Std/Classes/Ord.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean
index 8498dd447500..7af038e0fcab 100644
--- a/src/Std/Classes/Ord.lean
+++ b/src/Std/Classes/Ord.lean
@@ -31,11 +31,10 @@ class ReflCmp {α : Type u} (cmp : α → α → Ordering) : Prop where
 /-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 
+@[simp]
 theorem ReflOrd.compare_self {α : Type u} [Ord α] [ReflOrd α] {a : α} : compare a a = .eq :=
     ReflCmp.compare_self
 
-attribute [simp] ReflOrd.compare_self
-
 export ReflOrd (compare_self)
 
 end Refl