From 44365811cc0e9b079fe273e8e4ddcc07469fd3b8 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 25 Mar 2025 11:27:47 +0100
Subject: [PATCH] feat: add missing treemap lemmas (#7674)

This PR add missing lemmas about the tree map: `minKey*` variants return
the head of `keys`, `keys` and `toList` are ordered and `getKey*
t.minKey?` equals the minimum.

---------

Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
---
 src/Std/Data/DTreeMap/Internal/Lemmas.lean  | 42 ++++++++++++++
 src/Std/Data/DTreeMap/Lemmas.lean           | 40 ++++++++++++++
 src/Std/Data/DTreeMap/Raw/Lemmas.lean       | 36 ++++++++++++
 src/Std/Data/Internal/List/Associative.lean | 61 ++++++++++++++++++---
 src/Std/Data/TreeMap/Lemmas.lean            | 36 ++++++++++++
 src/Std/Data/TreeMap/Raw/Lemmas.lean        | 32 +++++++++++
 src/Std/Data/TreeSet/Lemmas.lean            | 32 +++++++++++
 src/Std/Data/TreeSet/Raw/Lemmas.lean        | 28 ++++++++++
 8 files changed, 298 insertions(+), 9 deletions(-)

diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index fe4d3d3251..ebee4cce6e 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -1560,6 +1560,11 @@ theorem distinct_keys [TransOrd α] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ compare a b = .eq) := by
   simp_to_model [keys] using h.ordered.distinctKeys.distinct
 
+theorem ordered_keys [TransOrd α] (h : t.WF) :
+    t.keys.Pairwise (fun a b => compare a b = .lt) := by
+  simp_to_model; simp only [keys_eq_map]
+  exact h.ordered.map _ fun _ _ hcmp => hcmp
+
 theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys := by
   simp_to_model [toList, keys] using (List.keys_eq_map ..).symm
@@ -1593,6 +1598,10 @@ theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
   simp_to_model [toList] using List.pairwise_fst_eq_false
 
+theorem ordered_keys_toList [TransOrd α] (h : t.WF) :
+    t.toList.Pairwise (fun a b => compare a.1 b.1 = .lt) := by
+  simp_to_model [toList] using h.ordered
+
 namespace Const
 
 variable {β : Type v} {t : Impl α β}
@@ -1642,6 +1651,11 @@ theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
   simp_to_model [Const.toList] using List.pairwise_fst_eq_false_map_toProd
 
+theorem ordered_keys_toList [TransOrd α] (h : t.WF) :
+    (toList t).Pairwise (fun a b => compare a.1 b.1 = .lt) := by
+  simp_to_model
+  exact h.ordered.map _ fun _ _ hcmp => hcmp
+
 end Const
 
 section monadic
@@ -4350,6 +4364,18 @@ theorem getKey?_minKey? [TransOrd α] (h : t.WF) {km} :
     (hkm : t.minKey? = some km) → t.getKey? km = some km := by
   simp_to_model using List.getKey?_minKey?
 
+theorem getKey_minKey? [TransOrd α] (h : t.WF) {km hc} :
+    (hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km := by
+  simp_to_model using List.getKey_minKey?
+
+theorem getKey!_minKey? [TransOrd α] [Inhabited α] (h : t.WF) {km} :
+    (hkm : t.minKey? = some km) → t.getKey! km = km := by
+  simp_to_model using List.getKey!_minKey?
+
+theorem getKeyD_minKey? [TransOrd α] (h : t.WF) {km fallback} :
+    (hkm : t.minKey? = some km) → t.getKeyD km fallback = km := by
+  simp_to_model using List.getKeyD_minKey?
+
 @[simp]
 theorem minKey?_bind_getKey? [TransOrd α] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? := by
@@ -4440,6 +4466,10 @@ theorem minKey?_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v kmi} :
     compare kmi k |>.isLE := by
   simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_self h
 
+theorem minKey?_eq_head?_keys [TransOrd α] (h : t.WF) :
+    t.minKey? = t.keys.head? := by
+  simp_to_model [minKey?, keys] using List.minKey?_eq_head?_keys h.ordered
+
 theorem minKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) :
     (t.modify k f).minKey? = t.minKey? := by
   simp_to_model [modify] using List.minKey?_modifyKey
@@ -4590,6 +4620,10 @@ theorem minKey_insertIfNew_le_self [TransOrd α] (h : t.WF) {k v} :
     compare (t.insertIfNew k v h.balanced |>.impl.minKey <| isEmpty_insertIfNew h) k |>.isLE := by
   simp_to_model [minKey, insertIfNew] using List.minKey_insertEntryIfNew_le_self
 
+theorem minKey_eq_head_keys [TransOrd α] (h : t.WF) {he} :
+    t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
+  simp_to_model [minKey, keys] using List.minKey_eq_head_keys h.ordered
+
 theorem minKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
     (t.modify k f).minKey he = t.minKey (isEmpty_modify h ▸ he):= by
   simp_to_model [minKey, modify] using List.minKey_modifyKey
@@ -4784,6 +4818,10 @@ theorem minKey!_insertIfNew!_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k
     compare (t.insertIfNew! k v |>.minKey!) k |>.isLE := by
   simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_le_self h
 
+theorem minKey!_eq_head!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keys.head! := by
+  simp_to_model [minKey!, keys] using List.minKey!_eq_head!_keys h.ordered
+
 theorem minKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
     (t.modify k f |>.minKey!) = t.minKey! := by
   simp_to_model [minKey!, modify] using List.minKey!_modifyKey
@@ -4997,6 +5035,10 @@ theorem minKeyD_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v fallback} :
     compare (t.insertIfNew! k v |>.minKeyD fallback) k |>.isLE := by
   simpa only [insertIfNew_eq_insertIfNew!] using minKeyD_insertIfNew_le_self h
 
+theorem minKeyD_eq_headD_keys [TransOrd α] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keys.headD fallback := by
+  simp_to_model [minKeyD, keys] using List.minKeyD_eq_headD_keys h.ordered
+
 theorem minKeyD_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) : ∀ {k f fallback},
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback := by
   simp_to_model [minKeyD, modify] using List.minKeyD_modifyKey
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index e1b6ed073e..4e08ebaee9 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -1015,6 +1015,10 @@ theorem distinct_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   Impl.distinct_keys t.wf
 
+theorem ordered_keys [TransCmp cmp] :
+    t.keys.Pairwise (fun a b => cmp a b = .lt) :=
+  Impl.ordered_keys t.wf
+
 @[simp]
 theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
@@ -1052,6 +1056,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
     t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.distinct_keys_toList t.wf
 
+theorem ordered_keys_toList [TransCmp cmp] :
+    t.toList.Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  Impl.ordered_keys_toList t.wf
+
 namespace Const
 
 variable {β : Type v} {t : DTreeMap α β cmp}
@@ -1103,6 +1111,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.Const.distinct_keys_toList t.wf
 
+theorem ordered_keys_toList [TransCmp cmp] :
+    (toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  Impl.Const.ordered_keys_toList t.wf
+
 end Const
 
 section monadic
@@ -2871,6 +2883,18 @@ theorem getKey?_minKey? [TransCmp cmp] {km} :
     (hkm : t.minKey? = some km) → t.getKey? km = some km :=
   Impl.getKey?_minKey? t.wf
 
+theorem getKey_minKey? [TransCmp cmp] {km hc} :
+    (hkm : t.minKey?.get (isSome_minKey?_of_contains hc) = km) → t.getKey km hc = km :=
+  Impl.getKey_minKey? t.wf
+
+theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] {km} :
+    (hkm : t.minKey? = some km) → t.getKey! km = km :=
+  Impl.getKey!_minKey? t.wf
+
+theorem getKeyD_minKey? [TransCmp cmp] {km fallback} :
+    (hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
+  Impl.getKeyD_minKey? t.wf
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -2918,6 +2942,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
     cmp kmi k |>.isLE :=
   Impl.minKey?_insertIfNew_le_self t.wf
 
+theorem minKey?_eq_head?_keys [TransCmp cmp] :
+    t.minKey? = t.keys.head? :=
+  Impl.minKey?_eq_head?_keys t.wf
+
 @[simp]
 theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey? :=
@@ -3064,6 +3092,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
     cmp (t.insertIfNew k v |>.minKey <| isEmpty_insertIfNew) k |>.isLE :=
   Impl.minKey_insertIfNew_le_self t.wf
 
+theorem minKey_eq_head_keys [TransCmp cmp] {he} :
+    t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
+  Impl.minKey_eq_head_keys t.wf
+
 @[simp]
 theorem minKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (t.modify k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
@@ -3199,6 +3231,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
     cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
   Impl.minKey!_insertIfNew_le_self t.wf
 
+theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
+    t.minKey! = t.keys.head! :=
+  Impl.minKey!_eq_head!_keys t.wf
+
 @[simp]
 theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
     (t.modify k f |>.minKey!) = t.minKey! :=
@@ -3332,6 +3368,10 @@ theorem minKeyD_insertIfNew_le_self [TransCmp cmp] {k v fallback} :
     cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
   Impl.minKeyD_insertIfNew_le_self t.wf (instOrd := ⟨cmp⟩)
 
+theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} :
+    t.minKeyD fallback = t.keys.headD fallback :=
+  Impl.minKeyD_eq_headD_keys t.wf
+
 @[simp]
 theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 3a0b06318c..03cb990c11 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -1025,6 +1025,10 @@ theorem distinct_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   Impl.distinct_keys h.out
 
+theorem ordered_keys [TransCmp cmp] (h : t.WF) :
+    t.keys.Pairwise (fun a b => cmp a b = .lt) :=
+  Impl.ordered_keys h.out
+
 @[simp]
 theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
@@ -1062,6 +1066,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.distinct_keys_toList h.out
 
+theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
+    t.toList.Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  Impl.ordered_keys_toList h.out
+
 namespace Const
 
 variable {β : Type v} {t : Raw α β cmp}
@@ -1114,6 +1122,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.Const.distinct_keys_toList h.out
 
+theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
+    (toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  Impl.Const.ordered_keys_toList h.out
+
 end Const
 
 section monadic
@@ -2876,6 +2888,18 @@ theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
     (hkm : t.minKey? = some km) → t.getKey? km = some km :=
   Impl.getKey?_minKey? h
 
+theorem getKey_minKey? [TransCmp cmp] (h : t.WF) {km hc} :
+    (hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km :=
+  Impl.getKey_minKey? h
+
+theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
+    (hkm : t.minKey? = some km) → t.getKey! km = km :=
+  Impl.getKey!_minKey? h
+
+theorem getKeyD_minKey? [TransCmp cmp] (h : t.WF) {km fallback} :
+    (hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
+  Impl.getKeyD_minKey? h
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -2923,6 +2947,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
     cmp kmi k |>.isLE :=
   Impl.minKey?_insertIfNew!_le_self h
 
+theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
+    t.minKey? = t.keys.head? :=
+  Impl.minKey?_eq_head?_keys h
+
 @[simp]
 theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
     (t.modify k f).minKey? = t.minKey? :=
@@ -3060,6 +3088,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k
     cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
   Impl.minKey!_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
 
+theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keys.head! :=
+  Impl.minKey!_eq_head!_keys h
+
 @[simp]
 theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     (t.modify k f |>.minKey!) = t.minKey! :=
@@ -3193,6 +3225,10 @@ theorem minKeyD_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
     cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
   Impl.minKeyD_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
 
+theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keys.headD fallback :=
+  Impl.minKeyD_eq_headD_keys h
+
 @[simp]
 theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index fd8db51dfe..8ccf75d491 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -4500,6 +4500,34 @@ theorem getKey?_minKey? [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd 
     getKey? km l = some km := by
   simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd]
 
+private theorem Option.get_eq_iff_eq_some {o : Option α} {h k} :
+    o.get h = k ↔ o = some k := by
+  simp [Option.eq_some_iff_get_eq, exists_prop_of_true h]
+
+private theorem Option.eq_get_iff_some_eq {o : Option α} {h k} :
+    k = o.get h ↔ some k = o := by
+  conv => congr <;> rw [eq_comm]
+  exact get_eq_iff_eq_some
+
+theorem getKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km hc} :
+    (hkm : (minKey? l |>.get <| isSome_minKey?_of_containsKey hc) = km) → getKey km l hc = km := by
+  have := (Option.eq_some_iff_get_eq.mp <| getKey?_eq_some_getKey hc).2
+  simp only [← this, Option.get_eq_iff_eq_some]
+  exact getKey?_minKey? hd
+
+theorem getKey!_minKey? [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} :
+    (hkm : minKey? l = some km) → getKey! km l = km := by
+  intro h
+  simp [getKey!_eq_getKey?, getKey?_minKey? hd h]
+
+theorem getKeyD_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback} :
+    (hkm : minKey? l = some km) → getKeyD km l fallback = km := by
+  intro h
+  simp [getKeyD_eq_getKey?, getKey?_minKey? hd h]
+
 theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
     (minKey? l |>.bind fun k => getKey? k l) = minKey? l := by
@@ -4665,6 +4693,11 @@ theorem minKey?_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
       rw [OrientedCmp.eq_swap (cmp := compare)]
       simp_all
 
+theorem minKey?_eq_head?_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) :
+    minKey? l = (keys l).head? := by
+  simp [minKey?, minEntry?_eq_head? ho, keys_eq_map]
+
 theorem minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
     minKey? (modifyKey k f l) = minKey? l := by
@@ -4785,15 +4818,6 @@ theorem minKey?_eq_some_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     minKey? l = some (minKey l he) := by
   simp [minKey_eq_get_minKey?]
 
-private theorem Option.get_eq_iff_eq_some {o : Option α} {h k} :
-    o.get h = k ↔ o = some k := by
-  simp [Option.eq_some_iff_get_eq, exists_prop_of_true h]
-
-private theorem Option.eq_get_iff_some_eq {o : Option α} {h k} :
-    k = o.get h ↔ some k = o := by
-  conv => congr <;> rw [eq_comm]
-  exact get_eq_iff_eq_some
-
 theorem minKey_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
     minKey l he = km ↔ getKey? km l = some km ∧ ∀ k, containsKey k l → (compare km k).isLE := by
@@ -4903,6 +4927,12 @@ theorem minKey_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulB
     compare (insertEntryIfNew k v l  |> minKey <| isEmpty_insertEntryIfNew) k |>.isLE :=
   minKey?_insertEntryIfNew_le_self hd minKey_eq_get_minKey?.symm
 
+theorem minKey_eq_head_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {he} :
+    minKey l he = (keys l).head (by simp_all [keys_eq_map, List.isEmpty_eq_false_iff]) := by
+  simp [minKey_eq_get_minKey?, Option.get_eq_iff_eq_some, ← List.head?_eq_head,
+    minKey?_eq_head?_keys ho]
+
 theorem minKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
     (modifyKey k f l |> minKey <| he) = minKey l (isEmpty_modifyKey k f l ▸ he):= by
@@ -5080,6 +5110,14 @@ theorem minKey!_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
     compare (insertEntryIfNew k v l |> minKey!) k |>.isLE := by
   simpa only [minKey_eq_minKey!] using minKey_insertEntryIfNew_le_self hd
 
+theorem minKey!_eq_head!_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
+    {l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) :
+    minKey! l = (keys l).head! := by
+  cases l
+  · rfl
+  · simp only [minKey!_eq_get!_minKey?, minKey?_eq_head?_keys ho]
+    rfl
+
 theorem minKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
     [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f} :
     (modifyKey k f l |> minKey!) = minKey! l := by
@@ -5284,6 +5322,11 @@ theorem minKeyD_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
     compare (insertEntryIfNew k v l |> minKeyD <| fallback) k |>.isLE := by
   simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntryIfNew_le_self hd
 
+theorem minKeyD_eq_headD_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {fallback} :
+    minKeyD l fallback = (keys l).headD fallback := by
+  simp [minKeyD_eq_getD_minKey?, minKey?_eq_head?_keys ho]
+
 theorem minKeyD_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f fallback} :
     (modifyKey k f l |> minKeyD <| fallback) = minKeyD l fallback := by
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index 1d265c3339..fea60b540c 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -753,6 +753,10 @@ theorem distinct_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.distinct_keys
 
+theorem ordered_keys [TransCmp cmp] :
+    t.keys.Pairwise (fun a b => cmp a b = .lt) :=
+  DTreeMap.ordered_keys
+
 @[simp]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
@@ -801,6 +805,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   DTreeMap.Const.distinct_keys_toList
 
+theorem ordered_keys_toList [TransCmp cmp] :
+    (toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  DTreeMap.Const.ordered_keys_toList
+
 section monadic
 
 variable {δ : Type w} {m : Type w → Type w}
@@ -1840,6 +1848,18 @@ theorem getKey?_minKey? [TransCmp cmp] {km} :
     (hkm : t.minKey? = some km) → t.getKey? km = some km :=
   DTreeMap.getKey?_minKey?
 
+theorem getKey_minKey? [TransCmp cmp] {km hc} :
+    (hkm : t.minKey?.get (isSome_minKey?_of_contains hc) = km) → t.getKey km hc = km :=
+  DTreeMap.getKey_minKey?
+
+theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] {km} :
+    (hkm : t.minKey? = some km) → t.getKey! km = km :=
+  DTreeMap.getKey!_minKey?
+
+theorem getKeyD_minKey? [TransCmp cmp] {km fallback} :
+    (hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
+  DTreeMap.getKeyD_minKey?
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -1887,6 +1907,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
     cmp kmi k |>.isLE :=
   DTreeMap.minKey?_insertIfNew_le_self
 
+theorem minKey?_eq_head?_keys [TransCmp cmp] :
+    t.minKey? = t.keys.head? :=
+  DTreeMap.minKey?_eq_head?_keys
+
 theorem minKey?_modify [TransCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Const.minKey?_modify
@@ -2017,6 +2041,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
     cmp (t.insertIfNew k v |>.minKey <| isEmpty_insertIfNew) k |>.isLE :=
   DTreeMap.minKey_insertIfNew_le_self
 
+theorem minKey_eq_head_keys [TransCmp cmp] {he} :
+    t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
+  DTreeMap.minKey_eq_head_keys
+
 theorem minKey_modify [TransCmp cmp] {k f he} :
     (modify t k f).minKey he =
       if cmp (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
@@ -2135,6 +2163,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
     cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
   DTreeMap.minKey!_insertIfNew_le_self
 
+theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
+    t.minKey! = t.keys.head! :=
+  DTreeMap.minKey!_eq_head!_keys
+
 theorem minKey!_modify [TransCmp cmp] [Inhabited α] {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
@@ -2252,6 +2284,10 @@ theorem minKeyD_insertIfNew_le_self [TransCmp cmp] {k v fallback} :
     cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
   DTreeMap.minKeyD_insertIfNew_le_self
 
+theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} :
+    t.minKeyD fallback = t.keys.headD fallback :=
+  DTreeMap.minKeyD_eq_headD_keys
+
 theorem minKeyD_modify [TransCmp cmp] {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.minKeyD fallback) =
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index 59d35177bb..0bf1a627b3 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -761,6 +761,10 @@ theorem distinct_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.Raw.distinct_keys h
 
+theorem ordered_keys [TransCmp cmp] (h : t.WF) :
+    t.keys.Pairwise (fun a b => cmp a b = .lt) :=
+  DTreeMap.Raw.ordered_keys h
+
 @[simp]
 theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
@@ -810,6 +814,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   DTreeMap.Raw.Const.distinct_keys_toList h
 
+theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
+    (toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
+  DTreeMap.Raw.Const.ordered_keys_toList h
+
 section monadic
 
 variable {δ : Type w} {m : Type w → Type w}
@@ -1849,6 +1857,18 @@ theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
     (hkm : t.minKey? = some km) → t.getKey? km = some km :=
   DTreeMap.Raw.getKey?_minKey? h
 
+theorem getKey_minKey? [TransCmp cmp] (h : t.WF) {km hc} :
+    (hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km :=
+  DTreeMap.Raw.getKey_minKey? h
+
+theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
+    (hkm : t.minKey? = some km) → t.getKey! km = km :=
+  DTreeMap.Raw.getKey!_minKey? h
+
+theorem getKeyD_minKey? [TransCmp cmp] (h : t.WF) {km fallback} :
+    (hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
+  DTreeMap.Raw.getKeyD_minKey? h
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -1896,6 +1916,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
     cmp kmi k |>.isLE :=
   DTreeMap.Raw.minKey?_insertIfNew_le_self h
 
+theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
+    t.minKey? = t.keys.head? :=
+  DTreeMap.Raw.minKey?_eq_head?_keys h
+
 theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Raw.Const.minKey?_modify h
@@ -2017,6 +2041,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k
     cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
   DTreeMap.Raw.minKey!_insertIfNew_le_self h
 
+theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keys.head! :=
+  DTreeMap.Raw.minKey!_eq_head!_keys h
+
 theorem minKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
@@ -2134,6 +2162,10 @@ theorem minKeyD_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
     cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
   DTreeMap.Raw.minKeyD_insertIfNew_le_self h
 
+theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keys.headD fallback :=
+  DTreeMap.Raw.minKeyD_eq_headD_keys h
+
 theorem minKeyD_modify [TransCmp cmp] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.minKeyD fallback) =
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index b8b581ea40..abb5109113 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -425,6 +425,10 @@ theorem distinct_toList [TransCmp cmp] :
     t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.distinct_keys
 
+theorem ordered_toList [TransCmp cmp] :
+    t.toList.Pairwise (fun a b => cmp a b = .lt) :=
+  DTreeMap.ordered_keys
+
 section monadic
 
 variable {δ : Type w} {m : Type w → Type w}
@@ -757,6 +761,18 @@ theorem get?_min? [TransCmp cmp] {km} :
     (hkm : t.min? = some km) → t.get? km = some km :=
   DTreeMap.getKey?_minKey?
 
+theorem get_min? [TransCmp cmp] {km hc} :
+    (hkm : t.min?.get (isSome_min?_of_contains hc) = km) → t.get km hc = km :=
+  DTreeMap.getKey_minKey?
+
+theorem get!_min? [TransCmp cmp] [Inhabited α] {km} :
+    (hkm : t.min? = some km) → t.get! km = km :=
+  DTreeMap.getKey!_minKey?
+
+theorem getD_min? [TransCmp cmp] {km fallback} :
+    (hkm : t.min? = some km) → t.getD km fallback = km :=
+  DTreeMap.getKeyD_minKey?
+
 @[simp]
 theorem min?_bind_get? [TransCmp cmp] :
     t.min?.bind t.get? = t.min? :=
@@ -872,6 +888,10 @@ theorem min_le_min_erase [TransCmp cmp] {k he} :
       (t.erase k |>.min he) |>.isLE :=
   DTreeMap.minKey_le_minKey_erase
 
+theorem min?_eq_head?_toList [TransCmp cmp] :
+    t.min? = t.toList.head? :=
+  TreeMap.minKey?_eq_head?_keys
+
 theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.min? = some t.min! :=
   DTreeMap.minKey?_eq_some_minKey! he
@@ -954,6 +974,10 @@ theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] {k}
     cmp t.min! (t.erase k |>.min!) |>.isLE :=
   DTreeMap.minKey!_le_minKey!_erase he
 
+theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] :
+    t.min! = t.toList.head! :=
+  TreeMap.minKey!_eq_head!_keys
+
 theorem min?_eq_some_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.min? = some (t.minD fallback) :=
   TreeMap.minKey?_eq_some_minKeyD he
@@ -1036,6 +1060,14 @@ theorem minD_le_minD_erase [TransCmp cmp] {k}
     cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
   TreeMap.minKeyD_le_minKeyD_erase he
 
+theorem min_eq_head_toList [TransCmp cmp] {he} :
+    t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
+  DTreeMap.minKey_eq_head_keys
+
+theorem minD_eq_headD_toList [TransCmp cmp] {fallback} :
+    t.minD fallback = t.toList.headD fallback :=
+  TreeMap.minKeyD_eq_headD_keys
+
 end Min
 
 end Std.TreeSet
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index bbd60c32af..2ee541a1f3 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -428,6 +428,10 @@ theorem distinct_toList [TransCmp cmp] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.Raw.distinct_keys h
 
+theorem ordered_toList [TransCmp cmp] (h : t.WF) :
+    t.toList.Pairwise (fun a b => cmp a b = .lt) :=
+  DTreeMap.Raw.ordered_keys h
+
 section monadic
 
 variable {δ : Type w} {m : Type w → Type w}
@@ -755,6 +759,18 @@ theorem get?_min? [TransCmp cmp] (h : t.WF) {km} :
     (hkm : t.min? = some km) → t.get? km = some km :=
   TreeMap.Raw.getKey?_minKey? h
 
+theorem get_min? [TransCmp cmp] (h : t.WF) {km hc} :
+    (hkm : t.min?.get (isSome_min?_of_contains h hc) = km) → t.get km hc = km :=
+  TreeMap.Raw.getKey_minKey? h
+
+theorem get!_min? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
+    (hkm : t.min? = some km) → t.get! km = km :=
+  TreeMap.Raw.getKey!_minKey? h
+
+theorem getD_min? [TransCmp cmp] (h : t.WF) {km fallback} :
+    (hkm : t.min? = some km) → t.getD km fallback = km :=
+  TreeMap.Raw.getKeyD_minKey? h
+
 @[simp]
 theorem min?_bind_get? [TransCmp cmp] (h : t.WF) :
     t.min?.bind t.get? = t.min? :=
@@ -782,6 +798,10 @@ theorem min?_le_min?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
     cmp km kme |>.isLE :=
   TreeMap.Raw.minKey?_le_minKey?_erase h
 
+theorem min?_eq_head?_toList [TransCmp cmp] (h : t.WF) :
+    t.min? = t.toList.head? :=
+  TreeMap.Raw.minKey?_eq_head?_keys h
+
 theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.min? = some t.min! :=
   DTreeMap.Raw.minKey?_eq_some_minKey! h he
@@ -860,6 +880,10 @@ theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
     cmp t.min! (t.erase k |>.min!) |>.isLE :=
   DTreeMap.Raw.minKey!_le_minKey!_erase h he
 
+theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.min! = t.toList.head! :=
+  TreeMap.Raw.minKey!_eq_head!_keys h
+
 theorem min?_eq_some_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.min? = some (t.minD fallback) :=
   DTreeMap.Raw.minKey?_eq_some_minKeyD h he
@@ -942,6 +966,10 @@ theorem minD_le_minD_erase [TransCmp cmp] (h : t.WF) {k}
     cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
   DTreeMap.Raw.minKeyD_le_minKeyD_erase h he
 
+theorem minD_eq_headD_toList [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minD fallback = t.toList.headD fallback :=
+  TreeMap.Raw.minKeyD_eq_headD_keys h
+
 end Min
 
 end Std.TreeSet.Raw