From b2da85971d7e6c8f71da817bf4289b4990215bf6 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 26 Mar 2025 13:49:33 +0100
Subject: [PATCH] fix: fix `maxKey`/`maxEntry` tree map functions and add
 lemmas for `maxKey` (#7664)

This PR fixes a bug in the definition of the tree map functions `maxKey`
and `maxEntry`. Moreover, it provides lemmas for this function and its
interactions with other function for which lemmas already exist.

---------

Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
---
 src/Std/Data/DTreeMap/Internal/Lemmas.lean    | 137 ++++++++++++-
 src/Std/Data/DTreeMap/Internal/Model.lean     |   8 +
 src/Std/Data/DTreeMap/Internal/Queries.lean   |  12 +-
 src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean |   4 +
 src/Std/Data/DTreeMap/Lemmas.lean             | 146 +++++++++++++
 src/Std/Data/Internal/List/Associative.lean   | 193 ++++++++++++++++++
 src/Std/Data/TreeMap/Lemmas.lean              | 135 +++++++++++-
 src/Std/Data/TreeSet/Lemmas.lean              | 100 ++++++++-
 8 files changed, 724 insertions(+), 11 deletions(-)

diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index 0f3d99890b..fa9b153f81 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -100,7 +100,8 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
      ⟨`minKey, (``minKey_eq_minKey, #[``(minKey_of_perm _)])⟩,
      ⟨`minKey!, (``minKey!_eq_minKey!, #[``(minKey!_of_perm _)])⟩,
      ⟨`minKeyD, (``minKeyD_eq_minKeyD, #[``(minKeyD_of_perm _)])⟩,
-     ⟨`maxKey?, (``maxKey?_eq_maxKey?, #[``(maxKey?_of_perm _)])⟩]
+     ⟨`maxKey?, (``maxKey?_eq_maxKey?, #[``(maxKey?_of_perm _)])⟩,
+     ⟨`maxKey, (``maxKey_eq_maxKey, #[``(maxKey_of_perm _)])⟩]
 
 /-- Internal implementation detail of the tree map -/
 scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
@@ -5361,6 +5362,140 @@ theorem maxKey?_alter!_eq_self [TransOrd α] (h : t.WF) {k f} :
 
 end Const
 
+theorem maxKey?_eq_some_maxKey [TransOrd α] (h : t.WF) {he} :
+    t.maxKey? = some (t.maxKey he) := by
+  simp_to_model [maxKey, maxKey?] using List.maxKey?_eq_some_maxKey
+
+theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) {he km} :
+    t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE := by
+  simp_to_model [maxKey, getKey?, contains] using List.maxKey_eq_iff_getKey?_eq_self_and_forall
+
+theorem maxKey_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.WF) {he km} :
+    t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE := by
+  simp_to_model [maxKey, contains] using List.maxKey_eq_some_iff_mem_and_forall
+
+theorem maxKey_insert [TransOrd α] (h : t.WF) {k v} :
+    (t.insert k v h.balanced).impl.maxKey (isEmpty_insert h) =
+      t.maxKey?.elim k fun k' => if compare k' k |>.isLE then k else k' := by
+  simp_to_model [insert, maxKey, maxKey?] using List.maxKey_insertEntry
+
+theorem maxKey_le_maxKey_insert [TransOrd α] (h : t.WF) {k v he} :
+    compare (t.maxKey he) (t.insert k v h.balanced |>.impl.maxKey <| isEmpty_insert h) |>.isLE := by
+  simp_to_model [maxKey, insert] using List.maxKey_le_maxKey_insertEntry
+
+theorem self_le_maxKey_insert [TransOrd α] (h : t.WF) {k v} :
+    compare k (t.insert k v h.balanced |>.impl.maxKey <| isEmpty_insert h) |>.isLE := by
+  simp_to_model [maxKey, insert] using List.self_le_maxKey_insertEntry
+
+theorem contains_maxKey [TransOrd α] (h : t.WF) {he} :
+    t.contains (t.maxKey he) := by
+  simp_to_model [maxKey, contains] using List.containsKey_maxKey
+
+theorem maxKey_mem [TransOrd α] (h : t.WF) {he} :
+    t.maxKey he ∈ t :=
+  contains_maxKey h
+
+theorem le_maxKey_of_contains [TransOrd α] (h : t.WF) {k} :
+    (hc : t.contains k) →
+    compare k (t.maxKey <| (isEmpty_eq_false_iff_exists_contains_eq_true h).mpr ⟨k, hc⟩) |>.isLE := by
+   simp_to_model [maxKey, contains] using le_maxKey_of_containsKey
+
+theorem le_maxKey_of_mem [TransOrd α] (h : t.WF) {k} (hc : k ∈ t) :
+    compare k (t.maxKey <| (isEmpty_eq_false_iff_exists_contains_eq_true h).mpr ⟨k, hc⟩) |>.isLE :=
+  le_maxKey_of_contains h hc
+
+theorem maxKey_le [TransOrd α] (h : t.WF) {k he} :
+    (compare (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (compare k' k).isLE) := by
+  simp_to_model [maxKey, contains] using List.maxKey_le
+
+theorem getKey?_maxKey [TransOrd α] (h : t.WF) {he} :
+    t.getKey? (t.maxKey he) = some (t.maxKey he) := by
+  simp_to_model [getKey?, maxKey] using List.getKey?_maxKey
+
+theorem getKey_maxKey [TransOrd α] (h : t.WF) {he hc} :
+    t.getKey (t.maxKey he) hc = t.maxKey he := by
+  simp_to_model [getKey, maxKey] using List.getKey_maxKey
+
+theorem getKey!_maxKey [TransOrd α] [Inhabited α] (h : t.WF) {he} :
+    t.getKey! (t.maxKey he) = t.maxKey he := by
+  simp_to_model [getKey!, maxKey] using List.getKey!_maxKey
+
+theorem getKeyD_maxKey [TransOrd α] (h : t.WF) {he fallback} :
+    t.getKeyD (t.maxKey he) fallback = t.maxKey he := by
+  simp_to_model [getKeyD, maxKey] using List.getKeyD_maxKey
+
+theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransOrd α] (h : t.WF) {k he} :
+    (t.erase k h.balanced |>.impl.maxKey he) =
+        t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he) ↔
+      ¬ compare k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false h he) = .eq := by
+  simp_to_model [maxKey, erase] using List.maxKey_eraseKey_eq_iff_beq_maxKey_eq_false
+
+theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransOrd α] (h : t.WF) {k he} :
+    (hc : ¬ compare k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he)) = .eq) →
+    (t.erase k h.balanced |>.impl.maxKey he) =
+      t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he) := by
+  simp_to_model [maxKey, erase] using List.maxKey_eraseKey_eq_of_beq_maxKey_eq_false
+
+theorem maxKey_erase_le_maxKey [TransOrd α] (h : t.WF) {k he} :
+    compare (t.erase k h.balanced |>.impl.maxKey he)
+        (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false h he) |>.isLE := by
+  simp_to_model [maxKey, erase] using List.maxKey_eraseKey_le_maxKey
+
+theorem maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v} :
+    (t.insertIfNew k v h.balanced).impl.maxKey (isEmpty_insertIfNew h) =
+      t.maxKey?.elim k fun k' => if compare k' k = .lt then k else k' := by
+  simp_to_model [maxKey, maxKey?, insertIfNew] using List.maxKey_insertEntryIfNew
+
+theorem maxKey_le_maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v he} :
+    compare (t.maxKey he)
+      (t.insertIfNew k v h.balanced |>.impl.maxKey <| isEmpty_insertIfNew h) |>.isLE := by
+  simp_to_model [maxKey, insertIfNew] using List.maxKey_le_maxKey_insertEntryIfNew
+
+theorem self_le_maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v} :
+    compare k (t.insertIfNew k v h.balanced |>.impl.maxKey <| isEmpty_insertIfNew h) |>.isLE := by
+  simp_to_model [maxKey, insertIfNew] using List.self_le_maxKey_insertEntryIfNew
+
+theorem maxKey_eq_getLast_keys [TransOrd α] (h : t.WF) {he} :
+    t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
+  simp_to_model [maxKey, keys] using List.maxKey_eq_getLast_keys h.ordered.distinctKeys h.ordered
+
+theorem maxKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
+    (t.modify k f).maxKey he = t.maxKey (isEmpty_modify h ▸ he):= by
+  simp_to_model [maxKey, modify] using List.maxKey_modifyKey
+
+theorem maxKey_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
+    (t.alter k f h.balanced).impl.maxKey he = k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
+  simp_to_model [maxKey, alter, get?, contains] using List.maxKey_alterKey_eq_self
+
+namespace Const
+
+variable {β : Type v} {t : Impl α β}
+
+theorem maxKey_modify [TransOrd α] (h : t.WF) {k f he} :
+    (modify k f t).maxKey he =
+      if compare (t.maxKey <| isEmpty_modify h ▸ he) k = .eq then
+        k
+      else
+        (t.maxKey <| Const.isEmpty_modify h ▸ he) := by
+  simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey
+
+theorem maxKey_modify_eq_maxKey [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
+    (modify k f t).maxKey he = t.maxKey (isEmpty_modify h ▸ he) := by
+  simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey_eq_maxKey
+
+theorem compare_maxKey_modify_eq [TransOrd α] (h : t.WF) {k f he} :
+    compare (modify k f t |>.maxKey he) (t.maxKey <| isEmpty_modify h ▸ he) = .eq := by
+  simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey_beq
+
+theorem maxKey_alter_eq_self [TransOrd α] (h : t.WF) {k f he} :
+    (alter k f t h.balanced).impl.maxKey he = k ↔
+      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
+  simp_to_model [maxKey, Const.alter, contains, Const.get?] using List.Const.maxKey_alterKey_eq_self
+
+end Const
+
+
 end Max
 
 end Std.DTreeMap.Internal.Impl
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index dc68f07e1e..9db993de01 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -493,6 +493,14 @@ theorem maxKey?_eq_minKey?_reverse [Ord α] {l : Impl α β} :
     l.maxKey? = (letI : Ord α := .opposite inferInstance; (reverse l).minKey?) := by
   induction l using maxKey?.induct <;> simp_all only [minKey?, maxKey?, reverse]
 
+theorem some_maxKey_eq_maxKey? [Ord α] {l : Impl α β} {he} :
+    some (l.maxKey he) = l.maxKey? := by
+  induction l, he using maxKey.induct <;> simp_all [maxKey, maxKey?]
+
+theorem maxKey_eq_get_maxKey? [Ord α] {l : Impl α β} {he} :
+    l.maxKey he = l.maxKey?.get (by simp [← some_maxKey_eq_maxKey? (he := he)]) := by
+  simp [← some_maxKey_eq_maxKey? (he := he)]
+
 theorem balanceL_eq_balance {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
     balanceL k v l r hlb hrb hlr = balance k v l r hlb hrb (Or.inl hlr.erase) := by
   rw [balanceL_eq_balanceLErase, balanceLErase_eq_balanceL!,
diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean
index 48ab5fdb1e..e53acedc50 100644
--- a/src/Std/Data/DTreeMap/Internal/Queries.lean
+++ b/src/Std/Data/DTreeMap/Internal/Queries.lean
@@ -307,8 +307,8 @@ def maxEntry? : Impl α β → Option ((a : α) × β a)
 
 /-- Implementation detail of the tree map -/
 def maxEntry : (t : Impl α β) → (h : t.isEmpty = false) → (a : α) × β a
-  | .inner _ k v .leaf _, _ => ⟨k, v⟩
-  | .inner _ _ _ l@(.inner ..) _, h => l.maxEntry (by simp_all [isEmpty])
+  | .inner _ k v _ .leaf, _ => ⟨k, v⟩
+  | .inner _ _ _ _ l@(.inner ..), h => l.maxEntry (by simp_all [isEmpty])
 
 /-- Implementation detail of the tree map -/
 def maxEntry! [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a
@@ -353,8 +353,8 @@ def maxKey? : Impl α β → Option α
 
 /-- Implementation detail of the tree map -/
 def maxKey : (t : Impl α β) → (h : t.isEmpty = false) → α
-  | .inner _ k _ .leaf _, _ => k
-  | .inner _ _ _ l@(.inner ..) _, h => l.maxKey (by simp_all [isEmpty])
+  | .inner _ k _ _ .leaf, _ => k
+  | .inner _ _ _ _ l@(.inner ..), h => l.maxKey (by simp_all [isEmpty])
 
 /-- Implementation detail of the tree map -/
 def maxKey! [Inhabited α] : Impl α β → α
@@ -756,8 +756,8 @@ def maxEntry? : Impl α β → Option (α × β)
 
 /-- Implementation detail of the tree map -/
 def maxEntry : (t : Impl α β) → (h : t.isEmpty = false) → α × β
-  | .inner _ k v .leaf _, _ => ⟨k, v⟩
-  | .inner _ _ _ l@(.inner ..) _, h => maxEntry l (by simp_all [isEmpty])
+  | .inner _ k v _ .leaf, _ => ⟨k, v⟩
+  | .inner _ _ _ _ l@(.inner ..), h => maxEntry l (by simp_all [isEmpty])
 
 /-- Implementation detail of the tree map -/
 def maxEntry! [Inhabited (α × β)] : Impl α β → α × β
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index 294cd162ed..53eedb0e4b 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -1856,4 +1856,8 @@ theorem maxKey?_eq_maxKey? [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Orde
   rw [maxKey?_of_perm hlo.distinctKeys (List.reverse_perm t.toListModel).symm, List.maxKey?]
   rw [maxKey?_eq_minKey?_reverse, minKey?_eq_minKey? hlo.reverse, toListModel_reverse]
 
+theorem maxKey_eq_maxKey [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Ordered) {he} :
+    t.maxKey he = List.maxKey t.toListModel (isEmpty_eq_isEmpty ▸ he) := by
+  simp only [List.maxKey_eq_get_maxKey?, maxKey_eq_get_maxKey?, maxKey?_eq_maxKey? hlo]
+
 end Std.DTreeMap.Internal.Impl
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index df5e17b1b5..65ff43fd73 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -3615,6 +3615,152 @@ theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} :
 
 end Const
 
+theorem maxKey_eq_get_maxKey? [TransCmp cmp] {he} :
+    t.maxKey he = t.maxKey?.get (isSome_maxKey?_iff_isEmpty_eq_false.mpr he) :=
+  letI : Ord α := ⟨cmp⟩
+  Impl.maxKey_eq_get_maxKey?
+
+theorem maxKey?_eq_some_maxKey [TransCmp cmp] {he} :
+    t.maxKey? = some (t.maxKey he) :=
+  Impl.maxKey?_eq_some_maxKey t.wf
+
+theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
+    t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  Impl.maxKey_eq_iff_getKey?_eq_self_and_forall t.wf
+
+theorem maxKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
+    t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  Impl.maxKey_eq_some_iff_mem_and_forall t.wf
+
+theorem maxKey_insert [TransCmp cmp] {k v} :
+    (t.insert k v).maxKey isEmpty_insert =
+      t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k' :=
+  Impl.maxKey_insert t.wf
+
+theorem maxKey_le_maxKey_insert [TransCmp cmp] {k v he} :
+    cmp (t.maxKey he) (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
+  Impl.maxKey_le_maxKey_insert t.wf
+
+theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
+    cmp k (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
+  Impl.self_le_maxKey_insert t.wf
+
+theorem contains_maxKey [TransCmp cmp] {he} :
+    t.contains (t.maxKey he) :=
+  Impl.contains_maxKey t.wf
+
+theorem maxKey_mem [TransCmp cmp] {he} :
+    t.maxKey he ∈ t :=
+  Impl.maxKey_mem t.wf
+
+theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
+    cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  Impl.le_maxKey_of_contains t.wf hc
+
+theorem le_maxKey_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
+    cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  Impl.le_maxKey_of_mem t.wf hc
+
+theorem maxKey_le [TransCmp cmp] {k he} :
+    (cmp (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  Impl.maxKey_le t.wf
+
+@[simp]
+theorem getKey?_maxKey [TransCmp cmp] {he} :
+    t.getKey? (t.maxKey he) = some (t.maxKey he) :=
+  Impl.getKey?_maxKey t.wf
+
+@[simp]
+theorem getKey_maxKey [TransCmp cmp] {he hc} :
+    t.getKey (t.maxKey he) hc = t.maxKey he :=
+  Impl.getKey_maxKey t.wf
+
+@[simp]
+theorem getKey!_maxKey [TransCmp cmp] [Inhabited α] {he} :
+    t.getKey! (t.maxKey he) = t.maxKey he :=
+  Impl.getKey!_maxKey t.wf
+
+@[simp]
+theorem getKeyD_maxKey [TransCmp cmp] {he fallback} :
+    t.getKeyD (t.maxKey he) fallback = t.maxKey he :=
+  Impl.getKeyD_maxKey t.wf
+
+@[simp]
+theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransCmp cmp] {k he} :
+    (t.erase k |>.maxKey he) =
+        t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
+      ¬ cmp k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
+  Impl.maxKey_erase_eq_iff_not_compare_eq_maxKey t.wf
+
+theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransCmp cmp] {k he} :
+    (hc : ¬ cmp k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
+    (t.erase k |>.maxKey he) =
+      t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
+  Impl.maxKey_erase_eq_of_not_compare_eq_maxKey t.wf
+
+theorem maxKey_erase_le_maxKey [TransCmp cmp] {k he} :
+    cmp (t.erase k |>.maxKey he)
+      (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
+  Impl.maxKey_erase_le_maxKey t.wf
+
+theorem maxKey_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).maxKey isEmpty_insertIfNew =
+      t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  Impl.maxKey_insertIfNew t.wf
+
+theorem maxKey_le_maxKey_insertIfNew [TransCmp cmp] {k v he} :
+    cmp (t.maxKey he)
+      (t.insertIfNew k v |>.maxKey isEmpty_insertIfNew) |>.isLE :=
+  Impl.maxKey_le_maxKey_insertIfNew t.wf
+
+theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
+    cmp k (t.insertIfNew k v |>.maxKey <| isEmpty_insertIfNew) |>.isLE :=
+  Impl.self_le_maxKey_insertIfNew t.wf
+
+theorem maxKey_eq_getLast_keys [TransCmp cmp] {he} :
+    t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
+  Impl.maxKey_eq_getLast_keys t.wf
+
+@[simp]
+theorem maxKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
+    (t.modify k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
+  Impl.maxKey_modify t.wf
+
+theorem maxKey_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
+    (t.alter k f).maxKey he = k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+  Impl.maxKey_alter_eq_self t.wf
+
+namespace Const
+
+variable {β : Type v} {t : DTreeMap α β cmp}
+
+theorem maxKey_modify [TransCmp cmp] {k f he} :
+    (modify t k f).maxKey he =
+      if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
+        k
+      else
+        (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) :=
+  Impl.Const.maxKey_modify t.wf
+
+@[simp]
+theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
+    (modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
+  Impl.Const.maxKey_modify_eq_maxKey t.wf
+
+@[simp]
+theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
+    cmp (modify t k f |>.maxKey he)
+      (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  Impl.Const.compare_maxKey_modify_eq t.wf
+
+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 :=
+  Impl.Const.maxKey_alter_eq_self t.wf
+
+end Const
+
 end Max
 
 end Std.DTreeMap
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index df01d778b0..6cd81fb2d0 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -5647,6 +5647,199 @@ theorem maxKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd 
 
 end Const
 
+/-- Given a proof that the list is nonempty, returns the largest key in an associative list. -/
+abbrev maxKey [Ord α] (xs : List ((a : α) × β a)) (h : xs.isEmpty = false) : α :=
+  letI : Ord α := .opposite inferInstance; minKey xs h
+
+theorem maxKey_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)}
+    {hl} (hd : DistinctKeys l) (hp : l.Perm l') :
+    maxKey l hl = maxKey l' (hp.isEmpty_eq ▸ hl) :=
+  letI : Ord α := .opposite inferInstance
+  minKey_of_perm hd hp
+
+theorem maxKey_eq_get_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} {he} :
+    maxKey l he = (maxKey? l |>.get (by simp [isSome_maxKey?_eq_not_isEmpty, he])) :=
+  rfl
+
+theorem maxKey?_eq_some_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} {he} :
+    maxKey? l = some (maxKey l he) :=
+  letI : Ord α := .opposite inferInstance
+  minKey?_eq_some_minKey
+
+theorem maxKey_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
+    maxKey l he = km ↔ getKey? km l = some km ∧ ∀ k, containsKey k l → (compare k km).isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_eq_iff_getKey?_eq_self_and_forall hd
+
+theorem maxKey_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    [LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
+    maxKey l he = km ↔ containsKey km l ∧ ∀ k, containsKey k l → (compare k km).isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_eq_some_iff_mem_and_forall hd
+
+theorem maxKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)}
+    (hd : DistinctKeys l) {k v} :
+    (insertEntry k v l |> maxKey <| isEmpty_insertEntry) =
+      ((maxKey? l).elim k fun k' => if compare k' k |>.isLE then k else k') :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntry hd
+
+theorem maxKey_le_maxKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v he} :
+    compare (maxKey l he) (insertEntry k v l |> maxKey <| isEmpty_insertEntry) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntry_le_minKey hd
+
+theorem self_le_maxKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
+    compare k (insertEntry k v l |> maxKey <| isEmpty_insertEntry) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntry_le_self hd
+
+theorem containsKey_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
+    containsKey (maxKey l he) l :=
+  letI : Ord α := .opposite inferInstance
+  containsKey_minKey hd
+
+theorem le_maxKey_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (hc : containsKey k l) :
+    compare k (maxKey l <| isEmpty_eq_false_iff_exists_containsKey.mpr ⟨k, hc⟩) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_le_of_containsKey hd hc
+
+theorem maxKey_le [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
+    (compare (maxKey l he) k).isLE ↔ (∀ k', containsKey k' l → (compare k' k).isLE) :=
+  letI : Ord α := .opposite inferInstance
+  le_minKey hd
+
+theorem getKey?_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
+    getKey? (maxKey l he) l = some (maxKey l he) :=
+  letI : Ord α := .opposite inferInstance
+  getKey?_minKey hd
+
+theorem getKey_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
+    getKey (maxKey l he) l (containsKey_maxKey hd) = maxKey l he :=
+  letI : Ord α := .opposite inferInstance
+  getKey_minKey hd
+
+theorem getKey!_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
+    getKey! (maxKey l he) l = maxKey l he :=
+  letI : Ord α := .opposite inferInstance
+  getKey!_minKey hd
+
+theorem getKeyD_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he fallback} :
+    getKeyD (maxKey l he) l fallback = maxKey l he :=
+  letI : Ord α := .opposite inferInstance
+  getKeyD_minKey hd
+
+theorem maxKey_eraseKey_eq_iff_beq_maxKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
+    (eraseKey k l |> maxKey <| he) =
+        maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) ↔
+      (k == (maxKey l <| isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he)) = false :=
+  letI : Ord α := .opposite inferInstance
+  minKey_eraseKey_eq_iff_beq_minKey_eq_false hd
+
+theorem maxKey_eraseKey_eq_of_beq_maxKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
+    (hc : (k == (maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he))) = false) →
+    (eraseKey k l |> maxKey <| he) =
+      maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) :=
+  letI : Ord α := .opposite inferInstance
+  minKey_eraseKey_eq_of_beq_minKey_eq_false hd
+
+theorem maxKey_eraseKey_le_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
+    compare (eraseKey k l |> maxKey <| he)
+      (maxKey l <| isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_le_minKey_erase hd
+
+theorem maxKey_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
+    (insertEntryIfNew k v l |> maxKey <| isEmpty_insertEntryIfNew) =
+      (maxKey? l).elim k fun k' => if compare k' k = .lt then k else k' :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntryIfNew hd
+
+theorem maxKey_le_maxKey_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v he} :
+    compare (maxKey l he)
+      (insertEntryIfNew k v l |> maxKey <| isEmpty_insertEntryIfNew) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntryIfNew_le_minKey hd
+
+theorem self_le_maxKey_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
+    compare k (insertEntryIfNew k v l  |> maxKey <| isEmpty_insertEntryIfNew) |>.isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_insertEntryIfNew_le_self hd
+
+theorem maxKey_eq_getLast_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l)
+    (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {he} :
+    maxKey l he = (keys l).getLast (by simp_all [keys_eq_map, List.isEmpty_eq_false_iff]) := by
+  simp only [List.getLast_eq_head_reverse, reverse_keys, maxKey_of_perm hd (List.reverse_perm l).symm]
+  letI : Ord α := .opposite inferInstance
+  exact minKey_eq_head_keys (List.pairwise_reverse.mpr ho)
+
+theorem maxKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
+    (modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he):=
+  letI : Ord α := .opposite inferInstance
+  minKey_modifyKey hd
+
+theorem maxKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f he} :
+    (alterKey k f l |> maxKey <| he) = k ↔
+      (f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_alterKey_eq_self hd
+
+namespace Const
+
+variable {β : Type v}
+
+theorem maxKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
+    (modifyKey k f l |> maxKey <| he) =
+      if (maxKey l <| isEmpty_modifyKey k f l ▸ he) == k then
+        k
+      else
+        (maxKey l <| isEmpty_modifyKey k f l ▸ he) :=
+  letI : Ord α := .opposite inferInstance
+  minKey_modifyKey hd
+
+theorem maxKey_modifyKey_eq_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
+    (modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he) :=
+  letI : Ord α := .opposite inferInstance
+  minKey_modifyKey_eq_minKey hd
+
+theorem maxKey_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
+    (modifyKey k f l |> maxKey <| he) == (maxKey l <| isEmpty_modifyKey k f l ▸ he) :=
+  letI : Ord α := .opposite inferInstance
+  minKey_modifyKey_beq hd
+
+theorem maxKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
+    (alterKey k f l |> maxKey <| he) = k ↔
+      (f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
+  letI : Ord α := .opposite inferInstance
+  minKey_alterKey_eq_self hd
+
+end Const
+
 end Max
 
 end Std.Internal.List
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index e83cd49918..b089408ef2 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -2010,13 +2010,13 @@ theorem getKeyD_minKey [TransCmp cmp] {he fallback} :
   DTreeMap.getKeyD_minKey
 
 @[simp]
-theorem minKey_erase_eq_iff_not_cmp_eq_minKey [TransCmp cmp] {k he} :
+theorem minKey_erase_eq_iff_not_compare_eq_minKey [TransCmp cmp] {k he} :
     (t.erase k |>.minKey he) =
         t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
       ¬ cmp k (t.minKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
   DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey
 
-theorem minKey_erase_eq_of_not_cmp_eq_minKey [TransCmp cmp] {k he} :
+theorem minKey_erase_eq_of_not_compare_eq_minKey [TransCmp cmp] {k he} :
     (hc : ¬ cmp k (t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
     (t.erase k |>.minKey he) =
       t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
@@ -2058,6 +2058,7 @@ theorem minKey_modify_eq_minKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (modify t k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
   DTreeMap.Const.minKey_modify_eq_minKey
 
+@[simp]
 theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
     cmp (modify t k f |>.minKey he)
       (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
@@ -2494,6 +2495,136 @@ theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} :
       (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Const.maxKey?_alter_eq_self
 
+theorem maxKey_eq_get_maxKey? [TransCmp cmp] {he} :
+    t.maxKey he = t.maxKey?.get (isSome_maxKey?_iff_isEmpty_eq_false.mpr he) :=
+  DTreeMap.maxKey_eq_get_maxKey?
+
+theorem maxKey?_eq_some_maxKey [TransCmp cmp] {he} :
+    t.maxKey? = some (t.maxKey he) :=
+  DTreeMap.maxKey?_eq_some_maxKey
+
+theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
+    t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  DTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall
+
+theorem maxKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
+    t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  DTreeMap.maxKey_eq_some_iff_mem_and_forall
+
+theorem maxKey_insert [TransCmp cmp] {k v} :
+    (t.insert k v).maxKey isEmpty_insert =
+      t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k' :=
+  DTreeMap.maxKey_insert
+
+theorem maxKey_le_maxKey_insert [TransCmp cmp] {k v he} :
+    cmp (t.maxKey he) (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
+  DTreeMap.maxKey_le_maxKey_insert
+
+theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
+    cmp k (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
+  DTreeMap.self_le_maxKey_insert
+
+theorem contains_maxKey [TransCmp cmp] {he} :
+    t.contains (t.maxKey he) :=
+  DTreeMap.contains_maxKey
+
+theorem maxKey_mem [TransCmp cmp] {he} :
+    t.maxKey he ∈ t :=
+  DTreeMap.maxKey_mem
+
+theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
+    cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  DTreeMap.le_maxKey_of_contains hc
+
+theorem le_maxKey_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
+    cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  DTreeMap.le_maxKey_of_mem hc
+
+theorem maxKey_le [TransCmp cmp] {k he} :
+    (cmp (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  DTreeMap.maxKey_le
+
+@[simp]
+theorem getKey?_maxKey [TransCmp cmp] {he} :
+    t.getKey? (t.maxKey he) = some (t.maxKey he) :=
+  DTreeMap.getKey?_maxKey
+
+@[simp]
+theorem getKey_maxKey [TransCmp cmp] {he hc} :
+    t.getKey (t.maxKey he) hc = t.maxKey he :=
+  DTreeMap.getKey_maxKey
+
+@[simp]
+theorem getKey!_maxKey [TransCmp cmp] [Inhabited α] {he} :
+    t.getKey! (t.maxKey he) = t.maxKey he :=
+  DTreeMap.getKey!_maxKey
+
+@[simp]
+theorem getKeyD_maxKey [TransCmp cmp] {he fallback} :
+    t.getKeyD (t.maxKey he) fallback = t.maxKey he :=
+  DTreeMap.getKeyD_maxKey
+
+@[simp]
+theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransCmp cmp] {k he} :
+    (t.erase k |>.maxKey he) =
+        t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
+      ¬ cmp k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
+  DTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey
+
+theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransCmp cmp] {k he} :
+    (hc : ¬ cmp k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
+    (t.erase k |>.maxKey he) =
+      t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
+  DTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey
+
+theorem maxKey_erase_le_maxKey [TransCmp cmp] {k he} :
+    cmp (t.erase k |>.maxKey he)
+      (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
+  DTreeMap.maxKey_erase_le_maxKey
+
+theorem maxKey_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).maxKey isEmpty_insertIfNew =
+      t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  DTreeMap.maxKey_insertIfNew
+
+theorem maxKey_le_maxKey_insertIfNew [TransCmp cmp] {k v he} :
+    cmp (t.maxKey he)
+      (t.insertIfNew k v |>.maxKey isEmpty_insertIfNew) |>.isLE :=
+  DTreeMap.maxKey_le_maxKey_insertIfNew (t := t.inner) (he := he)
+
+theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
+    cmp k (t.insertIfNew k v |>.maxKey <| isEmpty_insertIfNew) |>.isLE :=
+  DTreeMap.self_le_maxKey_insertIfNew
+
+theorem maxKey_eq_getLast_keys [TransCmp cmp] {he} :
+    t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
+  DTreeMap.maxKey_eq_getLast_keys
+
+theorem maxKey_modify [TransCmp cmp] {k f he} :
+    (modify t k f).maxKey he =
+      if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
+        k
+      else
+        (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) :=
+  DTreeMap.Const.maxKey_modify
+
+@[simp]
+theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
+    (modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
+  DTreeMap.Const.maxKey_modify_eq_maxKey
+
+@[simp]
+theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
+    cmp (modify t k f |>.maxKey he)
+      (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
+  DTreeMap.Const.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 :=
+  DTreeMap.Const.maxKey_alter_eq_self
+
+
 end Max
 
 end Std.TreeMap
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index 7bf36f36aa..b9b783cbb0 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -871,13 +871,13 @@ theorem getD_min [TransCmp cmp] {he fallback} :
   DTreeMap.getKeyD_minKey
 
 @[simp]
-theorem min_erase_eq_iff_not_cmp_eq_min [TransCmp cmp] {k he} :
+theorem min_erase_eq_iff_not_compare_eq_min [TransCmp cmp] {k he} :
     (t.erase k |>.min he) =
         t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
       ¬ cmp k (t.min <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
   DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey
 
-theorem min_erase_eq_of_not_cmp_eq_min [TransCmp cmp] {k he} :
+theorem min_erase_eq_of_not_compare_eq_min [TransCmp cmp] {k he} :
     (hc : ¬ cmp k (t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
     (t.erase k |>.min he) =
       t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
@@ -1198,6 +1198,102 @@ theorem max?_erase_le_max? [TransCmp cmp] {k km kme} :
     cmp kme km |>.isLE :=
   TreeMap.maxKey?_erase_le_maxKey?
 
+theorem max?_eq_getLast?_toList [TransCmp cmp] :
+    t.max? = t.toList.getLast? :=
+  TreeMap.maxKey?_eq_getLast?_keys
+
+theorem max_eq_get_max? [TransCmp cmp] {he} :
+    t.max he = t.max?.get (isSome_max?_iff_isEmpty_eq_false.mpr he) :=
+  TreeMap.maxKey_eq_get_maxKey?
+
+theorem max?_eq_some_max [TransCmp cmp] {he} :
+    t.max? = some (t.max he) :=
+  TreeMap.maxKey?_eq_some_maxKey
+
+theorem max_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
+    t.max he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  TreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall
+
+theorem max_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
+    t.max he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
+  TreeMap.maxKey_eq_some_iff_mem_and_forall
+
+theorem max_insert [TransCmp cmp] {k} :
+    (t.insert k).max isEmpty_insert =
+      t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
+  TreeMap.maxKey_insertIfNew
+
+theorem max_le_max_insert [TransCmp cmp] {k he} :
+    cmp (t.max he)
+      (t.insert k |>.max isEmpty_insert) |>.isLE :=
+  TreeMap.maxKey_le_maxKey_insertIfNew
+
+theorem self_le_max_insert [TransCmp cmp] {k} :
+    cmp k (t.insert k |>.max <| isEmpty_insert) |>.isLE :=
+  TreeMap.self_le_maxKey_insertIfNew
+
+theorem contains_max [TransCmp cmp] {he} :
+    t.contains (t.max he) :=
+  TreeMap.contains_maxKey
+
+theorem max_mem [TransCmp cmp] {he} :
+    t.max he ∈ t :=
+  TreeMap.maxKey_mem
+
+theorem le_max_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
+    cmp k (t.max <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  TreeMap.le_maxKey_of_contains hc
+
+theorem le_max_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
+    cmp k (t.max <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
+  TreeMap.le_maxKey_of_mem hc
+
+theorem max_le [TransCmp cmp] {k he} :
+    (cmp (t.max he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
+  TreeMap.maxKey_le
+
+@[simp]
+theorem get?_max [TransCmp cmp] {he} :
+    t.get? (t.max he) = some (t.max he) :=
+  TreeMap.getKey?_maxKey
+
+@[simp]
+theorem get_max [TransCmp cmp] {he hc} :
+    t.get (t.max he) hc = t.max he :=
+  TreeMap.getKey_maxKey
+
+@[simp]
+theorem get!_max [TransCmp cmp] [Inhabited α] {he} :
+    t.get! (t.max he) = t.max he :=
+  TreeMap.getKey!_maxKey
+
+@[simp]
+theorem getD_max [TransCmp cmp] {he fallback} :
+    t.getD (t.max he) fallback = t.max he :=
+  TreeMap.getKeyD_maxKey
+
+@[simp]
+theorem max_erase_eq_iff_not_compare_eq_max [TransCmp cmp] {k he} :
+    (t.erase k |>.max he) =
+        t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
+      ¬ cmp k (t.max <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
+  TreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey
+
+theorem max_erase_eq_of_not_compare_eq_max [TransCmp cmp] {k he} :
+    (hc : ¬ cmp k (t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
+    (t.erase k |>.max he) =
+      t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
+  TreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey
+
+theorem max_erase_le_max [TransCmp cmp] {k he} :
+    cmp (t.erase k |>.max he)
+      (t.max <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
+  TreeMap.maxKey_erase_le_maxKey
+
+theorem max_eq_getLast_toList [TransCmp cmp] {he} :
+    t.max he = t.toList.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
+  TreeMap.maxKey_eq_getLast_keys
+
 end Max
 
 end Std.TreeSet