diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index ea467ae6c5..ad0f46aba6 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -4227,6 +4227,14 @@ theorem minKey?_eq_none_iff [TransOrd α] (h : t.WF) :
     t.minKey? = none ↔ t.isEmpty := by
   simp_to_model using List.minKey?_eq_none_iff_isEmpty
 
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) {km} :
+    t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE := by
+  simp_to_model using List.minKey?_eq_some_iff_getKey?_eq_self_and_forall
+
+theorem minKey?_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.WF) {km} :
+    t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE := by
+  simp_to_model using List.minKey?_eq_some_iff_mem_and_forall
+
 theorem isNone_minKey?_eq_isEmpty [TransOrd α] (h : t.WF) :
     t.minKey?.isNone = t.isEmpty := by
   simp_to_model using List.isNone_minKey?_eq_isEmpty
@@ -4303,6 +4311,15 @@ theorem minKey?_le_of_mem [TransOrd α] (h : t.WF) {k km} :
     compare km k |>.isLE :=
   minKey?_le_of_contains h
 
+theorem le_minKey? [TransOrd α] {k} (h : t.WF) :
+    (∀ k', t.minKey? = some k' → (compare k k').isLE) ↔
+      (∀ k', k' ∈ t → (compare k k').isLE) := by
+  simp_to_model using List.le_minKey?
+
+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?
+
 @[simp]
 theorem minKey?_bind_getKey? [TransOrd α] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? := by
@@ -4353,6 +4370,99 @@ theorem minKey?_le_minKey?_erase! [TransOrd α] (h : t.WF) {k km kme} :
     compare km kme |>.isLE := by
   simpa only [erase_eq_erase!] using minKey?_le_minKey?_erase h
 
+theorem minKey?_insertIfNew [TransOrd α] (h : t.WF) {k v} :
+    (t.insertIfNew k v h.balanced).impl.minKey? =
+      t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
+  simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew
+
+theorem minKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v} :
+    (t.insertIfNew! k v).minKey? =
+      t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
+  simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew h
+
+theorem isSome_minKey?_insertIfNew [TransOrd α] (h : t.WF) {k v} :
+    (t.insertIfNew k v h.balanced).impl.minKey?.isSome := by
+  simp_to_model [insertIfNew] using List.isSome_minKey?_insertEntryIfNew
+
+theorem isSome_minKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v} :
+    (t.insertIfNew! k v).minKey?.isSome := by
+  simpa only [insertIfNew_eq_insertIfNew!] using isSome_minKey?_insertIfNew h
+
+theorem minKey?_insertIfNew_le_minKey? [TransOrd α] (h : t.WF) {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew k v h.balanced |>.impl.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    compare kmi km |>.isLE := by
+  simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew_le_minKey?
+
+theorem minKey?_insertIfNew!_le_minKey? [TransOrd α] (h : t.WF) {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew! k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew! h) = kmi) →
+    compare kmi km |>.isLE := by
+  simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_minKey? h
+
+theorem minKey?_insertIfNew_le_self [TransOrd α] (h : t.WF) {k v kmi} :
+    (hkmi : (t.insertIfNew k v h.balanced |>.impl.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    compare kmi k |>.isLE := by
+  simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew_le_self
+
+theorem minKey?_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v kmi} :
+    (hkmi : (t.insertIfNew! k v |>.minKey?.get <| isSome_minKey?_insertIfNew! h) = kmi) →
+    compare kmi k |>.isLE := by
+  simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_self h
+
+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
+
+theorem minKey?_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
+    (t.alter k f h.balanced).impl.minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
+  simp_to_model [alter] using List.minKey?_alterKey_eq_self
+
+theorem minKey?_alter!_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
+    (t.alter! k f).minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
+  simpa only [alter_eq_alter!] using minKey?_alter_eq_self h
+
+namespace Const
+
+variable {β : Type v} {t : Impl α β}
+
+theorem minKey?_modify [TransOrd α] (h : t.WF) {k f} :
+    (Const.modify k f t).minKey? = t.minKey?.map fun km => if compare km k = .eq then k else km := by
+  simp_to_model [Const.modify] using List.Const.minKey?_modifyKey
+
+theorem minKey?_modify_eq_minKey? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
+    (Const.modify k f t).minKey? = t.minKey? := by
+  simp_to_model [Const.modify] using List.Const.minKey?_modifyKey_of_lawfulEqOrd
+
+theorem isSome_minKey?_modify [TransOrd α] {k f}  (h : t.WF) :
+    (Const.modify k f t).minKey?.isSome = !t.isEmpty := by
+  simp_to_model [Const.modify] using List.Const.isSome_minKey?_modifyKey
+
+theorem isSome_minKey?_modify_eq_isSome [TransOrd α] (h : t.WF) {k f} :
+    (Const.modify k f t).minKey?.isSome = t.minKey?.isSome := by
+  simp_to_model [Const.modify] using List.Const.isSome_minKey?_modifyKey_eq_isSome
+
+theorem compare_minKey?_modify_eq [TransOrd α] (h : t.WF) {k f km kmm} :
+    (hkm : t.minKey? = some km) →
+    (hkmm : (Const.modify k f t |>.minKey? |>.get <|
+        (isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
+    compare kmm km = .eq := by
+  simp_to_model [Const.modify] using List.Const.minKey?_modifyKey_beq
+
+theorem minKey?_alter_eq_self [TransOrd α] (h : t.WF) {k f} :
+    (Const.alter k f t h.balanced).impl.minKey? = some k ↔
+      (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
+  simp_to_model [Const.alter] using List.Const.minKey?_alterKey_eq_self
+
+theorem minKey?_alter!_eq_self [TransOrd α] (h : t.WF) {k f} :
+    (Const.alter! k f t).minKey? = some k ↔
+      (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
+  simpa [alter_eq_alter!] using minKey?_alter_eq_self h
+
+end Const
+
 end Min
 
 end Std.DTreeMap.Internal.Impl
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index ac8db1a22d..d7392400c5 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -2779,6 +2779,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] :
     t.minKey? = none ↔ t.isEmpty :=
   Impl.minKey?_eq_none_iff t.wf
 
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} :
+    t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  Impl.minKey?_eq_some_iff_getKey?_eq_self_and_forall t.wf
+
+theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
+    t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  Impl.minKey?_eq_some_iff_mem_and_forall t.wf
+
 @[simp]
 theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] :
     t.minKey?.isNone = t.isEmpty :=
@@ -2837,6 +2845,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] {k km} :
     cmp km k |>.isLE :=
   Impl.minKey?_le_of_mem t.wf
 
+theorem le_minKey? [TransCmp cmp] {k} :
+    (∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
+      (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  Impl.le_minKey? t.wf
+
+theorem getKey?_minKey? [TransCmp cmp] {km} :
+    (hkm : t.minKey? = some km) → t.getKey? km = some km :=
+  Impl.getKey?_minKey? t.wf
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -2864,6 +2881,71 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] {k km kme} :
     cmp km kme |>.isLE :=
   Impl.minKey?_le_minKey?_erase t.wf
 
+theorem minKey?_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).minKey? =
+      t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  Impl.minKey?_insertIfNew t.wf
+
+theorem isSome_minKey?_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).minKey?.isSome :=
+  Impl.isSome_minKey?_insertIfNew t.wf
+
+theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew k v |>.minKey? |>.get isSome_minKey?_insertIfNew) = kmi) →
+    cmp kmi km |>.isLE :=
+  Impl.minKey?_insertIfNew_le_minKey? t.wf
+
+theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
+    (hkmi : (t.insertIfNew k v |>.minKey?.get isSome_minKey?_insertIfNew) = kmi) →
+    cmp kmi k |>.isLE :=
+  Impl.minKey?_insertIfNew_le_self t.wf
+
+@[simp]
+theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
+    (t.modify k f).minKey? = t.minKey? :=
+  Impl.minKey?_modify t.wf
+
+theorem minKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
+    (t.alter k f).minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  Impl.minKey?_alter_eq_self t.wf
+
+namespace Const
+
+variable {β : Type v} {t : DTreeMap α β cmp}
+
+theorem minKey?_modify [TransCmp cmp] {k f} :
+    (Const.modify t k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
+  Impl.Const.minKey?_modify t.wf
+
+@[simp]
+theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
+    (Const.modify t k f).minKey? = t.minKey? :=
+  Impl.Const.minKey?_modify_eq_minKey? t.wf
+
+theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
+    (Const.modify t k f).minKey?.isSome = !t.isEmpty :=
+  Impl.Const.isSome_minKey?_modify t.wf
+
+theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] {k f} :
+    (Const.modify t k f).minKey?.isSome = t.minKey?.isSome :=
+  Impl.Const.isSome_minKey?_modify_eq_isSome t.wf
+
+theorem compare_minKey?_modify_eq [TransCmp cmp] {k f km kmm} :
+    (hkm : t.minKey? = some km) →
+    (hkmm : (Const.modify t k f |>.minKey? |>.get <|
+        isSome_minKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) →
+    cmp kmm km = .eq :=
+  Impl.Const.compare_minKey?_modify_eq t.wf
+
+theorem minKey?_alter_eq_self [TransCmp cmp] {k f} :
+    (Const.alter t k f).minKey? = some k ↔
+      (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  Impl.Const.minKey?_alter_eq_self t.wf
+
+end Const
+
 end Min
 
 end Std.DTreeMap
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 3d79e00d6e..5d31c94fd9 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -2784,6 +2784,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] (h : t.WF) :
     t.minKey? = none ↔ t.isEmpty :=
   Impl.minKey?_eq_none_iff h
 
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
+    t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  Impl.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
+
+theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
+    t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  Impl.minKey?_eq_some_iff_mem_and_forall h
+
 @[simp]
 theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
     t.minKey?.isNone = t.isEmpty :=
@@ -2842,6 +2850,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
     cmp km k |>.isLE :=
   Impl.minKey?_le_of_mem h
 
+theorem le_minKey? [TransCmp cmp] {k} (h : t.WF) :
+    (∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
+      (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  Impl.le_minKey? h
+
+theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
+    (hkm : t.minKey? = some km) → t.getKey? km = some km :=
+  Impl.getKey?_minKey? h
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -2869,6 +2886,71 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
     cmp km kme |>.isLE :=
   Impl.minKey?_le_minKey?_erase! h
 
+theorem minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
+    (t.insertIfNew k v).minKey? =
+      t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  Impl.minKey?_insertIfNew! h
+
+theorem isSome_minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
+    (t.insertIfNew k v).minKey?.isSome :=
+  Impl.isSome_minKey?_insertIfNew! h
+
+theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] (h : t.WF) {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    cmp kmi km |>.isLE :=
+  Impl.minKey?_insertIfNew!_le_minKey? h
+
+theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
+    (hkmi : (t.insertIfNew k v |>.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    cmp kmi k |>.isLE :=
+  Impl.minKey?_insertIfNew!_le_self h
+
+@[simp]
+theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
+    (t.modify k f).minKey? = t.minKey? :=
+  Impl.minKey?_modify h
+
+theorem minKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
+    (t.alter k f).minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  Impl.minKey?_alter!_eq_self h
+
+namespace Const
+
+variable {β : Type v} {t : Raw α β cmp}
+
+theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
+    (Const.modify t k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
+  Impl.Const.minKey?_modify h
+
+@[simp]
+theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
+    (Const.modify t k f).minKey? = t.minKey? :=
+  Impl.Const.minKey?_modify_eq_minKey? h
+
+theorem isSome_minKey?_modify [TransCmp cmp] {k f}  (h : t.WF) :
+    (Const.modify t k f).minKey?.isSome = !t.isEmpty :=
+  Impl.Const.isSome_minKey?_modify h
+
+theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} :
+    (Const.modify t k f).minKey?.isSome = t.minKey?.isSome :=
+  Impl.Const.isSome_minKey?_modify_eq_isSome h
+
+theorem compare_minKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
+    (hkm : t.minKey? = some km) →
+    (hkmm : (Const.modify t k f |>.minKey? |>.get <|
+        (isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
+    cmp kmm km = .eq :=
+  Impl.Const.compare_minKey?_modify_eq h
+
+theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
+    (Const.alter t k f).minKey? = some k ↔
+      (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  Impl.Const.minKey?_alter!_eq_self h
+
+end Const
+
 end Min
 
 end Std.DTreeMap.Raw
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index c1c7e8ce48..92991e5d6f 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -696,6 +696,10 @@ theorem getKey_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
     {k k' : α} (h : k == k') {h'} {h''} : getKey k l h' = getKey k' l h'' := by
   simpa only [getKey?_eq_some_getKey, h', h'', Option.some.injEq] using getKey?_congr (l := l) h
 
+theorem getKey_eq_getEntry_fst [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
+    {h : containsKey a l} : getKey a l h = (getEntry a l h).fst := by
+  simp [getKey, getKey?_eq_getEntry?, Option.get_map, getEntry]
+
 /-- Internal implementation detail of the hash map -/
 def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
   (getKey? a l).getD fallback
@@ -3839,6 +3843,10 @@ theorem modifyKey_eq_alterKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β
   split <;> next h =>
     simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false]
 
+theorem DistinctKeys.modifyKey [BEq α] [LawfulBEq α] {a f} {l : List ((a : α) × β a)}
+    (hd : DistinctKeys l) : DistinctKeys (modifyKey a f l) := by
+  simpa [modifyKey_eq_alterKey] using hd.alterKey
+
 theorem modifyKey_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)}
     {k : α} {f : β k → β k} (hl : DistinctKeys l) (h : Perm l l') :
     Perm (modifyKey k f l) (modifyKey k f l') := by
@@ -4150,6 +4158,10 @@ theorem constModifyKey_eq_modifyKey {β : Type v} [BEq α] [LawfulBEq α] {k : 
   rw [modifyKey, Const.modifyKey, getValue?_eq_getValueCast?]
   cases getValueCast? k l <;> rfl
 
+theorem DistinctKeys.constModifyKey {β : Type v} [BEq α] [EquivBEq α] {a f} {l : List ((_ : α) × β)}
+    (hd : DistinctKeys l) : DistinctKeys (Const.modifyKey a f l) := by
+  simpa [Const.modifyKey_eq_alterKey] using hd.constAlterKey
+
 end Modify
 
 section Min
@@ -4265,8 +4277,8 @@ theorem minEntry?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
   · intro e e' he he' hee' he'e
     exact hd.eq_of_mem_of_beq he he' <| compare_eq_iff_beq.mp <| TransCmp.isLE_antisymm hee' he'e
 
-theorem minKey?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
-    {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
     minKey? l = some k ↔ getKey? k l = some k ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
   simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
   simp only [getKey?_eq_getEntry?, Option.map_eq_some', getEntry?_eq_some_iff hd]
@@ -4276,8 +4288,22 @@ theorem minKey?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k
   · rintro ⟨⟨_, ⟨_, hm⟩, rfl⟩, hcmp⟩
     exact ⟨_, ⟨hm, hcmp⟩, rfl⟩
 
-theorem minEntry?_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)}
-    (hl : DistinctKeys l) (hp : l.Perm l') :
+theorem minKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α]
+    [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
+    minKey? l = some k ↔ containsKey k l ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
+  simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
+  apply Iff.intro
+  · rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩
+    exact ⟨containsKey_of_mem hm, hcmp⟩
+  · rintro ⟨hc, hle⟩
+    have heq := beq_iff_eq.mp <| getKey_eq_getEntry_fst (α := α) ▸ getKey_beq hc
+    refine ⟨getEntry k l hc, ⟨mem_getEntry hc, ?_⟩, heq⟩
+    intro k' hk'
+    rw [heq]
+    exact hle _ hk'
+
+theorem minEntry?_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
     minEntry? l = minEntry? l' := by
   cases l
   case nil => simp_all only [List.nil_perm]
@@ -4430,19 +4456,24 @@ theorem isSome_minKey?_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEq
     minKey? l |>.isSome := by
   simpa [minKey?] using isSome_minEntry?_of_containsKey hc
 
+theorem getEntry?_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) {em} (hem : minEntry? l = some em) :
+    getEntry? em.1 l = some em := by
+  simp only [minEntry?_eq_some_iff _ hd] at hem
+  exact getEntry?_of_mem hd BEq.refl hem.1
+
 theorem minKey?_bind_getEntry? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
     (minKey? l |>.bind fun k => getEntry? k l) = minEntry? l := by
   rw [minKey?]
   cases h : minEntry? l
   · rfl
-  · simp only [Option.map_some', Option.some_bind, minEntry?_eq_some_iff _ hd] at h
-    exact getEntry?_of_mem hd BEq.refl h.1
+  · simp [getEntry?_minKey? hd h]
 
 theorem getKey?_minKey? [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} (hkm : minKey? l = some km) :
     getKey? km l = some km := by
-  simp_all [minKey?_eq_some_iff hd]
+  simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd]
 
 theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
@@ -4463,12 +4494,12 @@ theorem minKey?_eraseKey_eq_iff_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq
     minKey? (eraseKey k l) = minKey? l ↔ ∀ {km}, minKey? l = some km → (k == km) = false := by
   cases h : minKey? l
   · simp_all [minKey?_eq_none_iff_isEmpty]
-  · simp only [minKey?_eq_some_iff, getKey?_eraseKey, containsKey_eraseKey, compare_eq_iff_beq,
-      hd, hd.eraseKey] at ⊢ h
+  · simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall, getKey?_eraseKey,
+      containsKey_eraseKey, compare_eq_iff_beq, hd, hd.eraseKey] at ⊢ h
     simp_all
 
-theorem minKey?_eraseKey_eq_of_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
-    {l : List ((a : α) × β a)} (hd : DistinctKeys l)
+theorem minKey?_eraseKey_eq_of_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l)
     (hc : ∀ {km}, minKey? l = some km → (k == km) = false) :
     minKey? (eraseKey k l) = minKey? l := by
   rw [minKey?_eraseKey_eq_iff_beq_minKey?_eq_false hd |>.mpr]
@@ -4496,7 +4527,20 @@ theorem minKey?_le_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
     {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l)
     (hkm : (minKey? l |>.get <| isSome_minKey?_of_containsKey hc) = km) :
     compare km k |>.isLE := by
-  simpa only [← hkm] using minKey?_eq_some_iff hd |>.mp (by simp) |>.2 _ hc
+  simpa only [← hkm] using
+    minKey?_eq_some_iff_getKey?_eq_self_and_forall hd |>.mp (by simp) |>.2 _ hc
+
+theorem le_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)}
+    (hd : DistinctKeys l) :
+    (∀ k', minKey? l = some k' → (compare k k').isLE) ↔
+      (∀ k', containsKey k' l → (compare k k').isLE) := by
+  apply Iff.intro
+  · intro h k' hk'
+    have := isSome_minKey?_of_containsKey hk'
+    specialize h (minKey? l |>.get <| isSome_minKey?_of_containsKey hk') (by simp)
+    exact TransCmp.isLE_trans h <| minKey?_le_of_containsKey hd hk' rfl
+  · intro h k' hk'
+    exact h k' (containsKey_minKey? hd hk')
 
 theorem isSome_minKey?_of_isSome_minKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
     {l : List ((a : α) × β a)} (hs : eraseKey k l |> minKey? |>.isSome) :
@@ -4519,6 +4563,184 @@ theorem minKey?_le_minKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOr
   apply minKey?_le_of_containsKey hd _ hkm
   apply containsKey_minKey?_eraseKey hd hkme
 
+theorem minKey?_cons [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
+    minKey? (e :: l) = some (match minKey? l with
+    | none => e.1
+    | some w => if compare e.1 w |>.isLE then e.1 else w) := by
+  simp [minKey?, minEntry?_cons]
+  cases minEntry? l
+  · rfl
+  · simp [min_def, apply_ite Sigma.fst]
+
+theorem minEntry?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
+    minEntry? (insertEntryIfNew k v l) =
+      some (match minEntry? l with
+        | none => ⟨k, v⟩
+        | some e => if compare k e.1 = .lt then ⟨k, v⟩ else e) := by
+  simp [insertEntryIfNew]
+  cases hc : containsKey k l
+  · simp only [cond_false, minEntry?_cons, Option.some.injEq]
+    cases he : minEntry? l
+    · simp
+    · rename_i e
+      simp [min_def]
+      cases hcmp : compare k e.fst
+      · simp
+      · simp
+        rw [containsKey_congr <| compare_eq_iff_beq.mp hcmp] at hc
+        rw [containsKey_minKey? hd] at hc
+        · contradiction
+        · simp_all [minKey?]
+      · simp
+  · simp only [cond_true]
+    have := isSome_minEntry?_of_containsKey hc
+    cases h : minEntry? l
+    · simp_all
+    · simp
+      split
+      · have := minKey?_le_of_containsKey hd hc (by simp [minKey?, h]; rfl)
+        simp_all [← OrientedCmp.gt_iff_lt]
+      · rfl
+
+theorem minKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
+    minKey? (insertEntryIfNew k v l) =
+      some ((minKey? l).elim k fun k' => if compare k k' = .lt then k else k') := by
+  simp [minKey?, minEntry?_insertEntryIfNew hd]
+  cases minEntry? l <;> simp [apply_ite Sigma.fst]
+
+theorem isSome_minEntry?_insertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
+    minEntry? (insertEntryIfNew k v l) |>.isSome := by
+  simp [minEntry?_insertEntryIfNew hl]
+
+theorem isSome_minKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+    {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
+    minKey? (insertEntryIfNew k v l) |>.isSome := by
+  simp [minKey?_insertEntryIfNew  hl]
+
+theorem minKey?_insertEntryIfNew_le_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
+    {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi} (hkm : minKey? l = some km)
+    (hkmi : (insertEntryIfNew k v l |> minKey? |>.get <| isSome_minKey?_insertEntryIfNew hl) = kmi) :
+    compare kmi km |>.isLE := by
+  simp only [← hkmi, minKey?_insertEntryIfNew hl, hkm, Option.get_some, Option.elim_some]
+  split <;> simp [*]
+
+theorem minKey?_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α}
+    {v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l)
+    (hkmi : (insertEntryIfNew k v l |> minKey? |>.get <| isSome_minKey?_insertEntryIfNew hl) = kmi) :
+    compare kmi k |>.isLE := by
+  simp only [← hkmi, minKey?_insertEntryIfNew hl, Option.get_some]
+  cases minKey? l
+  · simp
+  · simp only [Option.elim_some]
+    cases hcmp : compare k _ <;> (try simp; done)
+    all_goals
+      rw [OrientedCmp.eq_swap (cmp := compare)]
+      simp_all
+
+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
+  cases hkm : minKey? l
+  · simp_all [minKey?_eq_none_iff_isEmpty, modifyKey]
+  · simp_all [minKey?_eq_some_iff_mem_and_forall, hd.modifyKey, containsKey_modifyKey]
+
+theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
+    {k f} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
+    minKey? (alterKey k f l) = some k ↔
+      (f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
+  simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.alterKey, getKey?_alterKey _ hd,
+    beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.not_isSome,
+    Option.isNone_iff_eq_none, reduceCtorEq, imp_false, ← Option.isSome_iff_ne_none,
+    containsKey_alterKey hd, beq_iff_eq, Bool.ite_eq_true_distrib, and_congr_right_iff]
+  intro hf
+  apply Iff.intro
+  · intro hk k' hk'
+    simpa [hk', hf] using hk k'
+  · intro hk k' hk'
+    simp only [hf, if_true_left] at hk'
+    by_cases hbeq : k == k'
+    · simp [compare_eq_iff_beq.mpr hbeq]
+    · exact hk k' (hk' hbeq)
+
+namespace Const
+
+variable {β : Type v}
+
+theorem minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
+    minKey? (modifyKey k f l) = (minKey? l).map fun km => if km == k then k else km := by
+  cases hkm : minKey? l
+  · simp_all [minKey?_eq_none_iff_isEmpty, modifyKey]
+  · simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall, hd.constModifyKey, getKey?_modifyKey]
+    cases h : _ == k
+    · simp_all [BEq.symm_false h, containsKey_modifyKey]
+    · simp_all [containsKey_congr (BEq.symm h), containsKey_eq_isSome_getKey?,
+        containsKey_modifyKey, getKey?_modifyKey]
+      intro k' hk'
+      cases hcmp : compare k k' <;> try rfl
+      replace hkm := hkm.2 k'
+      simp only [← compare_eq_iff_beq] at *
+      simp only [hcmp, reduceCtorEq, ↓reduceIte] at hk'
+      specialize hkm hk'
+      simp only [OrientedCmp.gt_iff_lt, Ordering.isLE_gt, Bool.false_eq_true] at *
+      have := TransCmp.lt_of_isLE_of_lt hkm hcmp
+      simp [this] at h
+
+theorem minKey?_modifyKey_of_lawfulEqOrd [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    [LawfulEqOrd α] {k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
+    minKey? (modifyKey k f l) = minKey? l := by
+  simp only [minKey?_modifyKey hd]
+  cases minKey? l
+  · rfl
+  · simp only [beq_iff_eq, Option.map_some', Option.some.injEq, ite_eq_right_iff]
+    exact Eq.symm
+
+theorem isSome_minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
+    {l : List ((_ : α) × β)} :
+    (modifyKey k f l |> minKey?).isSome = !l.isEmpty := by
+  simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
+
+theorem isSome_minKey?_modifyKey_eq_isSome [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
+    {l : List ((_ : α) × β)} :
+    (modifyKey k f l |> minKey?).isSome = (minKey? l).isSome := by
+  simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
+
+theorem minKey?_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f km kmm}
+    {l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : minKey? l = some km)
+    (hkmm : (modifyKey k f l |> minKey? |>.get <|
+        isSome_minKey?_modifyKey_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) :
+    kmm == km := by
+  simp only [minKey?_modifyKey hd, Option.get_map] at hkmm
+  simp only [Option.eq_some_iff_get_eq] at hkm
+  simp only [← hkmm, ← hkm.2]
+  split
+  · exact BEq.symm ‹_›
+  · exact BEq.refl
+
+theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
+    {k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
+    minKey? (alterKey k f l) = some k ↔
+      (f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
+  simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.constAlterKey, getKey?_alterKey _ hd,
+    ← compare_eq_iff_beq, compare_self, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true,
+    Option.not_isSome, Option.isNone_iff_eq_none, reduceCtorEq, imp_false,
+    ← Option.isSome_iff_ne_none, containsKey_alterKey hd, Bool.ite_eq_true_distrib,
+    and_congr_right_iff]
+  intro hf
+  apply Iff.intro
+  · intro hk k' hk'
+    simpa [hk', hf] using hk k'
+  · intro hk k' hk'
+    simp only [hf, if_true_left] at hk'
+    by_cases heq : compare k k' = .eq
+    · simp [heq]
+    · exact hk k' (hk' heq)
+
+end Const
+
 end Min
 
 end Std.Internal.List
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index ded6ee2405..afe6531703 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -1748,6 +1748,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] :
     t.minKey? = none ↔ t.isEmpty :=
   DTreeMap.minKey?_eq_none_iff
 
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} :
+    t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall
+
+theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
+    t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.minKey?_eq_some_iff_mem_and_forall
+
 @[simp]
 theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] :
     t.minKey?.isNone = t.isEmpty :=
@@ -1801,6 +1809,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] {k km} :
     cmp km k |>.isLE :=
   DTreeMap.minKey?_le_of_mem
 
+theorem le_minKey? [TransCmp cmp] {k} :
+    (∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
+      (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  DTreeMap.le_minKey?
+
+theorem getKey?_minKey? [TransCmp cmp] {km} :
+    (hkm : t.minKey? = some km) → t.getKey? km = some km :=
+  DTreeMap.getKey?_minKey?
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -1828,6 +1845,55 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] {k km kme} :
     cmp km kme |>.isLE :=
   DTreeMap.minKey?_le_minKey?_erase
 
+theorem minKey?_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).minKey? =
+      t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  DTreeMap.minKey?_insertIfNew
+
+theorem isSome_minKey?_insertIfNew [TransCmp cmp] {k v} :
+    (t.insertIfNew k v).minKey?.isSome :=
+  DTreeMap.isSome_minKey?_insertIfNew
+
+theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew k v |>.minKey? |>.get isSome_minKey?_insertIfNew) = kmi) →
+    cmp kmi km |>.isLE :=
+  DTreeMap.minKey?_insertIfNew_le_minKey?
+
+theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
+    (hkmi : (t.insertIfNew k v |>.minKey?.get isSome_minKey?_insertIfNew) = kmi) →
+    cmp kmi k |>.isLE :=
+  DTreeMap.minKey?_insertIfNew_le_self
+
+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
+
+@[simp]
+theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
+    (t.modify k f).minKey? = t.minKey? :=
+  DTreeMap.Const.minKey?_modify_eq_minKey?
+
+theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
+    (t.modify k f).minKey?.isSome = !t.isEmpty :=
+  DTreeMap.Const.isSome_minKey?_modify
+
+theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] {k f} :
+    (t.modify k f).minKey?.isSome = t.minKey?.isSome :=
+  DTreeMap.Const.isSome_minKey?_modify_eq_isSome
+
+theorem compare_minKey?_modify_eq [TransCmp cmp] {k f km kmm} :
+    (hkm : t.minKey? = some km) →
+    (hkmm : (t.modify k f |>.minKey? |>.get <|
+        isSome_minKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) →
+    cmp kmm km = .eq :=
+  DTreeMap.Const.compare_minKey?_modify_eq
+
+theorem minKey?_alter_eq_self [TransCmp cmp] {k f} :
+    (t.alter k f).minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  DTreeMap.Const.minKey?_alter_eq_self
+
 end Min
 
 end Std.TreeMap
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index 0795614482..e92f7d1eb5 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -1757,6 +1757,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] (h : t.WF) :
     t.minKey? = none ↔ t.isEmpty :=
   DTreeMap.Raw.minKey?_eq_none_iff h
 
+theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
+    t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
+
+theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
+    t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.Raw.minKey?_eq_some_iff_mem_and_forall h
+
 @[simp]
 theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
     t.minKey?.isNone = t.isEmpty :=
@@ -1810,6 +1818,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
     cmp km k |>.isLE :=
   DTreeMap.Raw.minKey?_le_of_mem h
 
+theorem le_minKey? [TransCmp cmp] {k} (h : t.WF) :
+    (∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
+      (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  DTreeMap.Raw.le_minKey? h
+
+theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
+    (hkm : t.minKey? = some km) → t.getKey? km = some km :=
+  DTreeMap.Raw.getKey?_minKey? h
+
 @[simp]
 theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
     t.minKey?.bind t.getKey? = t.minKey? :=
@@ -1837,6 +1854,55 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
     cmp km kme |>.isLE :=
   DTreeMap.Raw.minKey?_le_minKey?_erase h
 
+theorem minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
+    (t.insertIfNew k v).minKey? =
+      t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  DTreeMap.Raw.minKey?_insertIfNew h
+
+theorem isSome_minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
+    (t.insertIfNew k v).minKey?.isSome :=
+  DTreeMap.Raw.isSome_minKey?_insertIfNew h
+
+theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] (h : t.WF) {k v km kmi} :
+    (hkm : t.minKey? = some km) →
+    (hkmi : (t.insertIfNew k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    cmp kmi km |>.isLE :=
+  DTreeMap.Raw.minKey?_insertIfNew_le_minKey? h
+
+theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
+    (hkmi : (t.insertIfNew k v |>.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
+    cmp kmi k |>.isLE :=
+  DTreeMap.Raw.minKey?_insertIfNew_le_self 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
+
+@[simp]
+theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
+    (t.modify k f).minKey? = t.minKey? :=
+  DTreeMap.Raw.Const.minKey?_modify_eq_minKey? h
+
+theorem isSome_minKey?_modify [TransCmp cmp] {k f} (h : t.WF) :
+    (t.modify k f).minKey?.isSome = !t.isEmpty :=
+  DTreeMap.Raw.Const.isSome_minKey?_modify h
+
+theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} :
+    (t.modify k f).minKey?.isSome = t.minKey?.isSome :=
+  DTreeMap.Raw.Const.isSome_minKey?_modify_eq_isSome h
+
+theorem compare_minKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
+    (hkm : t.minKey? = some km) →
+    (hkmm : (t.modify k f |>.minKey? |>.get <|
+        (isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
+    cmp kmm km = .eq :=
+  DTreeMap.Raw.Const.compare_minKey?_modify_eq h
+
+theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
+    (t.alter k f).minKey? = some k ↔
+      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+  DTreeMap.Raw.Const.minKey?_alter_eq_self h
+
 end Min
 
 end Std.TreeMap.Raw
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index 0bc2847e35..ec2361ccf6 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -660,76 +660,112 @@ section Min
 @[simp]
 theorem min?_emptyc :
     (∅ : TreeSet α cmp).min? = none :=
-  DTreeMap.minKey?_emptyc
+  TreeMap.minKey?_emptyc
 
 theorem min?_of_isEmpty [TransCmp cmp] :
     (he : t.isEmpty) → t.min? = none :=
-  DTreeMap.minKey?_of_isEmpty
+  TreeMap.minKey?_of_isEmpty
 
 @[simp]
 theorem min?_eq_none_iff [TransCmp cmp] :
     t.min? = none ↔ t.isEmpty :=
-  DTreeMap.minKey?_eq_none_iff
+  TreeMap.minKey?_eq_none_iff
+
+theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} :
+    t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  TreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall
+
+theorem min?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
+    t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  TreeMap.minKey?_eq_some_iff_mem_and_forall
 
 @[simp]
 theorem isNone_min?_eq_isEmpty [TransCmp cmp] :
     t.min?.isNone = t.isEmpty :=
-  DTreeMap.isNone_minKey?_eq_isEmpty
+  TreeMap.isNone_minKey?_eq_isEmpty
 
 @[simp]
 theorem isSome_min?_eq_not_isEmpty [TransCmp cmp] :
     t.min?.isSome = !t.isEmpty :=
-  DTreeMap.isSome_minKey?_eq_not_isEmpty
+  TreeMap.isSome_minKey?_eq_not_isEmpty
+
+theorem min?_insert [TransCmp cmp] {k} :
+    (t.insert k).min? =
+      t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  TreeMap.minKey?_insertIfNew
+
+theorem isSome_min?_insert [TransCmp cmp] {k} :
+    (t.insert k).min?.isSome :=
+  TreeMap.isSome_minKey?_insertIfNew
+
+theorem min?_insert_le_min? [TransCmp cmp] {k km kmi} :
+    (hkm : t.min? = some km) →
+    (hkmi : (t.insert k |>.min? |>.get isSome_min?_insert) = kmi) →
+    cmp kmi km |>.isLE :=
+  TreeMap.minKey?_insertIfNew_le_minKey?
+
+theorem min?_insert_le_self [TransCmp cmp] {k kmi} :
+    (hkmi : (t.insert k |>.min?.get isSome_min?_insert) = kmi) →
+    cmp kmi k |>.isLE :=
+  TreeMap.minKey?_insertIfNew_le_self
 
 theorem contains_min? [TransCmp cmp] {km} :
     (hkm : t.min? = some km) →
     t.contains km :=
-  DTreeMap.contains_minKey?
+  TreeMap.contains_minKey?
 
 theorem isSome_min?_of_contains [TransCmp cmp] {k} :
     (hc : t.contains k) → t.min?.isSome :=
-  DTreeMap.isSome_minKey?_of_contains
+  TreeMap.isSome_minKey?_of_contains
 
 theorem isSome_min?_of_mem [TransCmp cmp] {k} :
     k ∈ t → t.min?.isSome :=
-  DTreeMap.isSome_minKey?_of_mem
+  TreeMap.isSome_minKey?_of_mem
 
 theorem min?_le_of_contains [TransCmp cmp] {k km} :
     (hc : t.contains k) → (hkm : (t.min?.get <| isSome_min?_of_contains hc) = km) →
     cmp km k |>.isLE :=
-  DTreeMap.minKey?_le_of_contains
+  TreeMap.minKey?_le_of_contains
 
 theorem min?_le_of_mem [TransCmp cmp] {k km} :
     (hc : k ∈ t) → (hkm : (t.min?.get <| isSome_min?_of_mem hc) = km) →
     cmp km k |>.isLE :=
-  DTreeMap.minKey?_le_of_mem
+  TreeMap.minKey?_le_of_mem
+
+theorem le_min? [TransCmp cmp] {k} :
+    (∀ k', t.min? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  TreeMap.le_minKey?
+
+theorem get?_min? [TransCmp cmp] {km} :
+    (hkm : t.min? = some km) → t.get? km = some km :=
+  DTreeMap.getKey?_minKey?
 
 @[simp]
 theorem min?_bind_get? [TransCmp cmp] :
     t.min?.bind t.get? = t.min? :=
-  DTreeMap.minKey?_bind_getKey?
+  TreeMap.minKey?_bind_getKey?
 
 theorem min?_erase_eq_iff_not_compare_eq_min? [TransCmp cmp] {k} :
     (t.erase k |>.min?) = t.min? ↔
       ∀ {km}, t.min? = some km → ¬ cmp k km = .eq :=
-  DTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey?
+  TreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey?
 
 theorem min?_erase_eq_of_not_compare_eq_min? [TransCmp cmp] {k} :
     (hc : ∀ {km}, t.min? = some km → ¬ cmp k km = .eq) →
     (t.erase k |>.min?) = t.min? :=
-  DTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey?
+  TreeMap.minKey?_erase_eq_of_not_compare_eq_minKey?
 
 theorem isSome_min?_of_isSome_min?_erase [TransCmp cmp] {k} :
     (hs : t.erase k |>.min?.isSome) →
     t.min?.isSome :=
-  DTreeMap.isSome_minKey?_of_isSome_minKey?_erase
+  TreeMap.isSome_minKey?_of_isSome_minKey?_erase
 
 theorem min?_le_min?_erase [TransCmp cmp] {k km kme} :
     (hkme : (t.erase k |>.min?) = some kme) →
     (hkm : (t.min?.get <|
       isSome_min?_of_isSome_min?_erase <| hkme ▸ Option.isSome_some) = km) →
     cmp km kme |>.isLE :=
-  DTreeMap.minKey?_le_minKey?_erase
+  TreeMap.minKey?_le_minKey?_erase
 
 end Min
 
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index 7c3bf36744..7d3a3cacbe 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -658,76 +658,112 @@ section Min
 @[simp]
 theorem min?_emptyc :
     (empty : Raw α cmp).min? = none :=
-  DTreeMap.Raw.minKey?_emptyc
+  TreeMap.Raw.minKey?_emptyc
 
 theorem min?_of_isEmpty [TransCmp cmp] (h : t.WF) :
     (he : t.isEmpty) → t.min? = none :=
-  DTreeMap.Raw.minKey?_of_isEmpty h
+  TreeMap.Raw.minKey?_of_isEmpty h
 
 @[simp]
 theorem min?_eq_none_iff [TransCmp cmp] (h : t.WF) :
     t.min? = none ↔ t.isEmpty :=
-  DTreeMap.Raw.minKey?_eq_none_iff h
+  TreeMap.Raw.minKey?_eq_none_iff h
+
+theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
+    t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
+
+theorem min?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
+    t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
+  DTreeMap.Raw.minKey?_eq_some_iff_mem_and_forall h
 
 @[simp]
 theorem isNone_min?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
     t.min?.isNone = t.isEmpty :=
-  DTreeMap.Raw.isNone_minKey?_eq_isEmpty h
+  TreeMap.Raw.isNone_minKey?_eq_isEmpty h
 
 @[simp]
 theorem isSome_min?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) :
     t.min?.isSome = !t.isEmpty :=
-  DTreeMap.Raw.isSome_minKey?_eq_not_isEmpty h
+  TreeMap.Raw.isSome_minKey?_eq_not_isEmpty h
+
+theorem min?_insert [TransCmp cmp] (h : t.WF) {k} :
+    (t.insert k).min? =
+      t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
+  TreeMap.Raw.minKey?_insertIfNew h
+
+theorem isSome_min?_insert [TransCmp cmp] (h : t.WF) {k} :
+    (t.insert k).min?.isSome :=
+  TreeMap.Raw.isSome_minKey?_insertIfNew h
+
+theorem min?_insert_le_min? [TransCmp cmp] (h : t.WF) {k km kmi} :
+    (hkm : t.min? = some km) →
+    (hkmi : (t.insert k |>.min? |>.get <| isSome_min?_insert h) = kmi) →
+    cmp kmi km |>.isLE :=
+  TreeMap.Raw.minKey?_insertIfNew_le_minKey? h
+
+theorem min?_insert_le_self [TransCmp cmp] (h : t.WF) {k kmi} :
+    (hkmi : (t.insert k |>.min?.get <| isSome_min?_insert h) = kmi) →
+    cmp kmi k |>.isLE :=
+  TreeMap.Raw.minKey?_insertIfNew_le_self h
 
 theorem contains_min? [TransCmp cmp] (h : t.WF) {km} :
     (hkm : t.min? = some km) →
     t.contains km :=
-  DTreeMap.Raw.contains_minKey? h
+  TreeMap.Raw.contains_minKey? h
 
 theorem isSome_min?_of_contains [TransCmp cmp] (h : t.WF) {k} :
     (hc : t.contains k) → t.min?.isSome :=
-  DTreeMap.Raw.isSome_minKey?_of_contains h
+  TreeMap.Raw.isSome_minKey?_of_contains h
 
 theorem isSome_min?_of_mem [TransCmp cmp] (h : t.WF) {k} :
     k ∈ t → t.min?.isSome :=
-  DTreeMap.Raw.isSome_minKey?_of_mem h
+  TreeMap.Raw.isSome_minKey?_of_mem h
 
 theorem min?_le_of_contains [TransCmp cmp] (h : t.WF) {k km} :
     (hc : t.contains k) → (hkm : (t.min?.get <| isSome_min?_of_contains h hc) = km) →
     cmp km k |>.isLE :=
-  DTreeMap.Raw.minKey?_le_of_contains h
+  TreeMap.Raw.minKey?_le_of_contains h
 
 theorem min?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
     (hc : k ∈ t) → (hkm : (t.min?.get <| isSome_min?_of_mem h hc) = km) →
     cmp km k |>.isLE :=
-  DTreeMap.Raw.minKey?_le_of_mem h
+  TreeMap.Raw.minKey?_le_of_mem h
+
+theorem le_min? [TransCmp cmp] {k} (h : t.WF) :
+    (∀ k', t.min? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
+  TreeMap.Raw.le_minKey? h
+
+theorem get?_min? [TransCmp cmp] (h : t.WF) {km} :
+    (hkm : t.min? = some km) → t.get? km = some km :=
+  TreeMap.Raw.getKey?_minKey? h
 
 @[simp]
 theorem min?_bind_get? [TransCmp cmp] (h : t.WF) :
     t.min?.bind t.get? = t.min? :=
-  DTreeMap.Raw.minKey?_bind_getKey? h
+  TreeMap.Raw.minKey?_bind_getKey? h
 
 theorem min?_erase_eq_iff_not_compare_eq_min? [TransCmp cmp] (h : t.WF) {k} :
     (t.erase k |>.min?) = t.min? ↔
       ∀ {km}, t.min? = some km → ¬ cmp k km = .eq :=
-  DTreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? h
+  TreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? h
 
 theorem min?_erase_eq_of_not_compare_eq_min? [TransCmp cmp] (h : t.WF) {k} :
     (hc : ∀ {km}, t.min? = some km → ¬ cmp k km = .eq) →
     (t.erase k |>.min?) = t.min? :=
-  DTreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? h
+  TreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? h
 
 theorem isSome_min?_of_isSome_min?_erase [TransCmp cmp] (h : t.WF) {k} :
     (hs : t.erase k |>.min?.isSome) →
     t.min?.isSome :=
-  DTreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase h
+  TreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase h
 
 theorem min?_le_min?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
     (hkme : (t.erase k |>.min?) = some kme) →
     (hkm : (t.min?.get <|
       isSome_min?_of_isSome_min?_erase h <| hkme ▸ Option.isSome_some) = km) →
     cmp km kme |>.isLE :=
-  DTreeMap.Raw.minKey?_le_minKey?_erase h
+  TreeMap.Raw.minKey?_le_minKey?_erase h
 
 end Min