diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index a170964a94..61878a505d 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -3128,6 +3128,12 @@ theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
       (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
   Impl.Const.compare_minKey_modify_eq t.wf
 
+@[simp]
+theorem ordCompare_minKey_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f he} :
+    compare (modify t k f |>.minKey he)
+      (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  compare_minKey_modify_eq
+
 theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
     (alter t k f).minKey he = k ↔
       (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
@@ -3266,6 +3272,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   Impl.Const.compare_minKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} [Inhabited α] {k f} :
+    compare (modify t k f).minKey! t.minKey! = .eq :=
+  compare_minKey!_modify_eq
+
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
@@ -3403,6 +3414,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   Impl.Const.compare_minKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f fallback} :
+    compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
+  compare_minKeyD_modify_eq
+
 theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
@@ -3754,6 +3770,12 @@ theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
       (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
   Impl.Const.compare_maxKey_modify_eq t.wf
 
+@[simp]
+theorem ordCompare_maxKey_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f he} :
+    compare (modify t k f |>.maxKey he)
+      (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  compare_maxKey_modify_eq
+
 theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
     (alter t k f).maxKey he = k ↔
       (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
@@ -3892,6 +3914,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   Impl.Const.compare_maxKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} [Inhabited α] {k f} :
+    compare (modify t k f).maxKey! t.maxKey! = .eq :=
+  compare_maxKey!_modify_eq
+
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
@@ -4029,6 +4056,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
   Impl.Const.compare_maxKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f fallback} :
+    compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
+  compare_maxKeyD_modify_eq
+
 theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 90e1d06982..94c361c71e 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -3120,6 +3120,12 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   Impl.Const.compare_minKey!_modify_eq h (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF)
+    {k f} :
+    compare (modify t k f).minKey! t.minKey! = .eq :=
+  compare_minKey!_modify_eq h
+
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
@@ -3257,6 +3263,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   Impl.Const.compare_minKeyD_modify_eq h (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
+    compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
+  compare_minKeyD_modify_eq h
+
 theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
@@ -3594,6 +3605,12 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   Impl.Const.compare_maxKey!_modify_eq h (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF)
+    {k f} :
+    compare (modify t k f).maxKey! t.maxKey! = .eq :=
+  compare_maxKey!_modify_eq h
+
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
@@ -3731,6 +3748,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
   Impl.Const.compare_maxKeyD_modify_eq h (instOrd := ⟨cmp⟩)
 
+@[simp]
+theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
+    compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
+  compare_maxKeyD_modify_eq h
+
 theorem maxKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index ee7450ce90..c0cd3b4dc0 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -2063,6 +2063,12 @@ theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
       (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
   DTreeMap.Const.compare_minKey_modify_eq
 
+@[simp]
+theorem ordCompare_minKey_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f he} :
+    compare (modify t k f |>.minKey he)
+      (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  compare_minKey_modify_eq
+
 theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
     (alter t k f).minKey he = k ↔
       (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
@@ -2185,6 +2191,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   DTreeMap.Const.compare_minKey!_modify_eq
 
+@[simp]
+theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} [Inhabited α] {k f} :
+    compare (modify t k f).minKey! t.minKey! = .eq :=
+  compare_minKey!_modify_eq
+
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
@@ -2306,6 +2317,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   DTreeMap.Const.compare_minKeyD_modify_eq
 
+@[simp]
+theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f fallback} :
+    compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
+  compare_minKeyD_modify_eq
+
 theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
@@ -2619,6 +2635,12 @@ theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
       (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
   DTreeMap.Const.compare_maxKey_modify_eq
 
+@[simp]
+theorem ordCompare_maxKey_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f he} :
+    compare (modify t k f |>.maxKey he)
+      (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  compare_maxKey_modify_eq
+
 theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
     (alter t k f).maxKey he = k ↔
       (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
@@ -2741,6 +2763,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   DTreeMap.Const.compare_maxKey!_modify_eq
 
+@[simp]
+theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} [Inhabited α] {k f} :
+    compare (modify t k f).maxKey! t.maxKey! = .eq :=
+  compare_maxKey!_modify_eq
+
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
@@ -2862,6 +2889,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] {k f fallback} :
     cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
   DTreeMap.Const.compare_maxKeyD_modify_eq
 
+@[simp]
+theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f fallback} :
+    compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
+  compare_maxKeyD_modify_eq
+
 theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index 2b4c3951ae..849ea659c6 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -2059,6 +2059,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     cmp (modify t k f).minKey! t.minKey! = .eq :=
   DTreeMap.Raw.Const.compare_minKey!_modify_eq h
 
+@[simp]
+theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF) {k f} :
+    compare (modify t k f).minKey! t.minKey! = .eq :=
+  compare_minKey!_modify_eq h
+
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
@@ -2180,6 +2185,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
   DTreeMap.Raw.Const.compare_minKeyD_modify_eq h
 
+@[simp]
+theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
+    compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
+  compare_minKeyD_modify_eq h
+
 theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
@@ -2480,6 +2490,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     cmp (modify t k f).maxKey! t.maxKey! = .eq :=
   DTreeMap.Raw.Const.compare_maxKey!_modify_eq h
 
+@[simp]
+theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF) {k f} :
+    compare (modify t k f).maxKey! t.maxKey! = .eq :=
+  compare_maxKey!_modify_eq h
+
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
@@ -2601,6 +2616,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
     cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
   DTreeMap.Raw.Const.compare_maxKeyD_modify_eq h
 
+@[simp]
+theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
+    compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
+  compare_maxKeyD_modify_eq h
+
 theorem maxKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔