From f3c507ec579c2bb2f6de64bddb0e1cbca5515b41 Mon Sep 17 00:00:00 2001
From: Paul Reichert <datokrat@users.noreply.github.com>
Date: Mon, 10 Mar 2025 15:35:24 +0100
Subject: [PATCH] feat: tree map lemmas for modify (#7419)

This PR provides lemmas about the tree map function `modify` and its
interactions with other functions for which lemmas already exist.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
---
 src/Std/Data/DTreeMap/Internal/Lemmas.lean    | 268 +++++++++++++++++-
 .../Data/DTreeMap/Internal/Operations.lean    |   4 +-
 src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean |  10 +
 src/Std/Data/DTreeMap/Lemmas.lean             | 264 +++++++++++++++++
 src/Std/Data/DTreeMap/Raw/Lemmas.lean         | 264 +++++++++++++++++
 src/Std/Data/TreeMap/Lemmas.lean              | 127 +++++++++
 src/Std/Data/TreeMap/Raw/Lemmas.lean          | 127 +++++++++
 7 files changed, 1061 insertions(+), 3 deletions(-)

diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index d1df38b891..45c0faa3d5 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -85,7 +85,9 @@ private def modifyMap : Std.HashMap Name Name :=
      (`alter, ``toListModel_alter),
      (`alter!, ``toListModel_alter!),
      (`Const.alter, ``Const.toListModel_alter),
-     (`Const.alter!, ``Const.toListModel_alter!)]
+     (`Const.alter!, ``Const.toListModel_alter!),
+     (`modify, ``toListModel_modify),
+     (`Const.modify, ``Const.toListModel_modify)]
 
 private def congrNames : MacroM (Array (TSyntax `term)) := do
   return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
@@ -3872,4 +3874,268 @@ end Const
 
 end Alter
 
+section Modify
+
+variable [TransOrd α]
+
+section Dependent
+
+variable [LawfulEqOrd α]
+
+@[simp]
+theorem isEmpty_modify (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).isEmpty = t.isEmpty := by
+  simp_to_model [modify] using List.isEmpty_modifyKey
+
+theorem contains_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).contains k' = t.contains k' := by
+  simp_to_model [modify] using List.containsKey_modifyKey
+
+theorem mem_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    k' ∈ t.modify k f ↔ k' ∈ t := by
+  simp [mem_iff_contains, contains_modify h]
+
+theorem size_modify (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).size = t.size := by
+  simp_to_model [modify] using List.length_modifyKey
+
+theorem get?_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).get? k' =
+      if h : compare k k' = .eq then
+        (cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) ((t.get? k).map f))
+      else
+        t.get? k' := by
+  simp_to_model [modify] using List.getValueCast?_modifyKey
+
+@[simp]
+theorem get?_modify_self (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).get? k = (t.get? k).map f := by
+  simp_to_model [modify] using List.getValueCast?_modifyKey_self
+
+theorem get_modify (h : t.WF) {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f} :
+    (t.modify k f).get k' hc =
+      if heq : compare k k' = .eq then
+        haveI h' : k ∈ t := by rwa [mem_modify h, ← compare_eq_iff_eq.mp heq] at hc
+        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| f (t.get k h')
+      else
+        haveI h' : k' ∈ t := by rwa [mem_modify h] at hc
+        t.get k' h' := by
+  simp_to_model [modify] using List.getValueCast_modifyKey
+
+@[simp]
+theorem get_modify_self (h : t.WF) {k : α} {f : β k → β k} {hc : k ∈ t.modify k f} :
+    haveI h' : k ∈ t := mem_modify h |>.mp hc
+    (t.modify k f).get k hc = f (t.get k h') := by
+  simp_to_model [modify] using List.getValueCast_modifyKey_self
+
+theorem get!_modify (h : t.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
+    (t.modify k f).get! k' =
+      if heq : compare k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+      else
+        t.get! k' := by
+  simp_to_model [modify] using List.getValueCast!_modifyKey
+
+@[simp]
+theorem get!_modify_self (h : t.WF) {k : α} [Inhabited (β k)] {f : β k → β k} :
+    (t.modify k f).get! k = ((t.get? k).map f).get! := by
+  simp_to_model [modify] using List.getValueCast!_modifyKey_self
+
+theorem getD_modify (h : t.WF) {k k' : α} {fallback : β k'} {f : β k → β k} :
+    (t.modify k f).getD k' fallback =
+      if heq : compare k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+      else
+        t.getD k' fallback := by
+  simp_to_model [modify] using List.getValueCastD_modifyKey
+
+@[simp]
+theorem getD_modify_self (h : t.WF) {k : α} {fallback : β k} {f : β k → β k} :
+    (t.modify k f).getD k fallback = ((t.get? k).map f).getD fallback := by
+  simp_to_model [modify] using List.getValueCastD_modifyKey_self
+
+theorem getKey?_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey? k' =
+      if compare k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' := by
+  simp_to_model [modify] using List.getKey?_modifyKey
+
+theorem getKey?_modify_self (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).getKey? k = if k ∈ t then some k else none := by
+  simp_to_model [modify] using List.getKey?_modifyKey_self
+
+theorem getKey!_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey! k' =
+      if compare k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' := by
+  simp_to_model [modify] using List.getKey!_modifyKey
+
+theorem getKey!_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β k → β k} :
+    (t.modify k f).getKey! k = if k ∈ t then k else default := by
+  simp_to_model [modify] using List.getKey!_modifyKey_self
+
+theorem getKey_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k}
+    {hc : k' ∈ t.modify k f} :
+    (t.modify k f).getKey k' hc =
+      if compare k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t.getKey k' h' := by
+  simp_to_model [modify] using List.getKey_modifyKey
+
+@[simp]
+theorem getKey_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β k → β k}
+    {hc : k ∈ t.modify k f} : (t.modify k f).getKey k hc = k := by
+  simp_to_model [modify] using List.getKey_modifyKey_self
+
+theorem getKeyD_modify (h : t.WF) {k k' fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k' fallback =
+      if compare k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback := by
+  simp_to_model [modify] using List.getKeyD_modifyKey
+
+theorem getKeyD_modify_self (h : t.WF) [Inhabited α] {k fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback := by
+  simp_to_model [modify] using List.getKeyD_modifyKey_self
+
+end Dependent
+
+namespace Const
+
+variable {β : Type v} {t : Impl α β}
+
+@[simp]
+theorem isEmpty_modify (h : t.WF) {k : α} {f : β → β} :
+    (modify k f t).isEmpty = t.isEmpty := by
+  simp_to_model [Const.modify] using List.Const.isEmpty_modifyKey
+
+theorem contains_modify (h : t.WF) {k k' : α} {f : β → β} :
+    (modify k f t).contains k' = t.contains k' := by
+  simp_to_model [Const.modify] using List.Const.containsKey_modifyKey
+
+theorem mem_modify (h : t.WF) {k k' : α} {f : β → β} :
+    k' ∈ modify k f t ↔ k' ∈ t := by
+  simp [mem_iff_contains, contains_modify h]
+
+theorem size_modify (h : t.WF) {k : α} {f : β → β} :
+    (modify k f t).size = t.size := by
+  simp_to_model [Const.modify] using List.Const.length_modifyKey
+
+theorem get?_modify (h : t.WF) {k k' : α} {f : β → β} :
+    get? (modify k f t) k' =
+      if compare k k' = .eq then
+        (get? t k).map f
+      else
+        get? t k' := by
+  simp_to_model [Const.modify] using List.Const.getValue?_modifyKey
+
+@[simp]
+theorem get?_modify_self (h : t.WF) {k : α} {f : β → β} :
+    get? (modify k f t) k = (get? t k).map f := by
+  simp_to_model [Const.modify] using List.Const.getValue?_modifyKey_self
+
+theorem get_modify (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ modify k f t} :
+    get (modify k f t) k' hc =
+      if heq : compare k k' = .eq then
+        haveI h' : k ∈ t := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
+        f (get t k h')
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        get t k' h' := by
+  simp_to_model [Const.modify] using List.Const.getValue_modifyKey
+
+@[simp]
+theorem get_modify_self (h : t.WF) {k : α} {f : β → β} {hc : k ∈ modify k f t} :
+    haveI h' : k ∈ t := mem_modify h |>.mp hc
+    get (modify k f t) k hc = f (get t k h') := by
+  simp_to_model [Const.modify] using List.Const.getValue_modifyKey_self
+
+theorem get!_modify (h : t.WF) {k k' : α} [hi : Inhabited β] {f : β → β} :
+    get! (modify k f t) k' =
+      if compare k k' = .eq then
+        get? t k |>.map f |>.get!
+      else
+        get! t k' := by
+  simp_to_model [Const.modify] using List.Const.getValue!_modifyKey
+
+@[simp]
+theorem get!_modify_self (h : t.WF) {k : α} [Inhabited β] {f : β → β} :
+    get! (modify k f t) k = ((get? t k).map f).get! := by
+  simp_to_model [Const.modify] using List.Const.getValue!_modifyKey_self
+
+theorem getD_modify (h : t.WF) {k k' : α} {fallback : β} {f : β → β} :
+    getD (modify k f t) k' fallback =
+      if compare k k' = .eq then
+        get? t k |>.map f |>.getD fallback
+      else
+        getD t k' fallback := by
+  simp_to_model [Const.modify] using List.Const.getValueD_modifyKey
+
+@[simp]
+theorem getD_modify_self (h : t.WF) {k : α} {fallback : β} {f : β → β} :
+    getD (modify k f t) k fallback = ((get? t k).map f).getD fallback := by
+  simp_to_model [Const.modify] using List.Const.getValueD_modifyKey_self
+
+theorem getKey?_modify (h : t.WF) {k k' : α} {f : β → β} :
+    (modify k f t).getKey? k' =
+      if compare k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' := by
+  simp_to_model [Const.modify] using List.Const.getKey?_modifyKey
+
+theorem getKey?_modify_self (h : t.WF) {k : α} {f : β → β} :
+    (modify k f t).getKey? k = if k ∈ t then some k else none := by
+  simp_to_model [Const.modify] using List.Const.getKey?_modifyKey_self
+
+theorem getKey!_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} :
+    (modify k f t).getKey! k' =
+      if compare k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' := by
+  simp_to_model [Const.modify] using List.Const.getKey!_modifyKey
+
+theorem getKey!_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β → β} :
+    (modify k f t).getKey! k = if k ∈ t then k else default := by
+  simp_to_model [Const.modify] using List.Const.getKey!_modifyKey_self
+
+theorem getKey_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β → β}
+    {hc : k' ∈ modify k f t} :
+    (modify k f t).getKey k' hc =
+      if compare k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t.getKey k' h' := by
+  simp_to_model [Const.modify] using List.Const.getKey_modifyKey
+
+@[simp]
+theorem getKey_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β → β}
+    {hc : k ∈ modify k f t} : (modify k f t).getKey k hc = k := by
+  simp_to_model [Const.modify] using List.Const.getKey_modifyKey_self
+
+theorem getKeyD_modify (h : t.WF) {k k' fallback : α} {f : β → β} :
+    (modify k f t).getKeyD k' fallback =
+      if compare k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback := by
+  simp_to_model [Const.modify] using List.Const.getKeyD_modifyKey
+
+theorem getKeyD_modify_self (h : t.WF) [Inhabited α] {k fallback : α} {f : β → β} :
+    (modify k f t).getKeyD k fallback = if k ∈ t then k else fallback := by
+  simp_to_model [Const.modify] using List.Const.getKeyD_modifyKey_self
+
+end Const
+
+end Modify
+
 end Std.DTreeMap.Internal.Impl
diff --git a/src/Std/Data/DTreeMap/Internal/Operations.lean b/src/Std/Data/DTreeMap/Internal/Operations.lean
index b6ca274752..412d2fa069 100644
--- a/src/Std/Data/DTreeMap/Internal/Operations.lean
+++ b/src/Std/Data/DTreeMap/Internal/Operations.lean
@@ -784,7 +784,7 @@ def modify [Ord α] [LawfulEqOrd α] (k : α) (f : β k → β k) (t : Impl α 
     | .eq => .inner sz k (f <| cast (congrArg β <| compare_eq_iff_eq.mp h).symm v') l r
 
 @[Std.Internal.tree_tac]
-theorem size_modify [Ord α] [LawfulEqOrd α] {k f} {t : Impl α β} :
+theorem aux_size_modify [Ord α] [LawfulEqOrd α] {k f} {t : Impl α β} :
     (t.modify k f).size = t.size := by
   unfold modify
   split <;> (try split) <;> rfl
@@ -891,7 +891,7 @@ def modify [Ord α] (k : α) (f : β → β) (t : Impl α β) :
     | .eq => .inner sz k (f v') l r
 
 @[Std.Internal.tree_tac]
-theorem size_modify [Ord α] {k f} {t : Impl α β} :
+theorem aux_size_modify [Ord α] {k f} {t : Impl α β} :
     (modify k f t).size = t.size := by
   unfold modify
   split <;> (try split) <;> rfl
diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index c0e5648733..b563c6b8a8 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -1116,6 +1116,11 @@ theorem ordered_modify [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β}
     (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered :=
   modify_eq_alter htb ▸ ordered_alter htb hto
 
+theorem toListModel_modify [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a f}
+    (htb : t.Balanced) (hto : t.Ordered) :
+    List.Perm (modify a f t).toListModel (modifyKey a f t.toListModel) := by
+  simpa only [modify_eq_alter htb, modifyKey_eq_alterKey] using toListModel_alter htb hto
+
 /-!
 ### mergeWith
 -/
@@ -1365,6 +1370,11 @@ theorem ordered_modify [Ord α] [TransOrd α] {t : Impl α β} {a f}
     (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered :=
   modify_eq_alter htb ▸ ordered_alter htb hto
 
+theorem toListModel_modify [Ord α] [TransOrd α] {t : Impl α β} {a f}
+    (htb : t.Balanced) (hto : t.Ordered) :
+    List.Perm (modify a f t).toListModel (Const.modifyKey a f t.toListModel) := by
+  simpa only [modify_eq_alter htb, Const.modifyKey_eq_alterKey] using toListModel_alter htb hto
+
 /-!
 ### mergeWith
 -/
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index 53892c1411..3b55061a7d 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -2443,4 +2443,268 @@ end Const
 
 end Alter
 
+section Modify
+
+variable [TransCmp cmp]
+
+section Dependent
+
+variable [LawfulEqCmp cmp]
+
+@[simp]
+theorem isEmpty_modify {k : α} {f : β k → β k} :
+    (t.modify k f).isEmpty = t.isEmpty :=
+  Impl.isEmpty_modify t.wf
+
+theorem contains_modify {k k' : α} {f : β k → β k} :
+    (t.modify k f).contains k' = t.contains k' :=
+  Impl.contains_modify t.wf
+
+theorem mem_modify {k k' : α} {f : β k → β k} :
+    k' ∈ t.modify k f ↔ k' ∈ t :=
+  Impl.mem_modify t.wf
+
+theorem size_modify {k : α} {f : β k → β k} :
+    (t.modify k f).size = t.size :=
+  Impl.size_modify t.wf
+
+theorem get?_modify {k k' : α} {f : β k → β k} :
+    (t.modify k f).get? k' =
+      if h : cmp k k' = .eq then
+        (cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) ((t.get? k).map f))
+      else
+        t.get? k' :=
+  Impl.get?_modify t.wf
+
+@[simp]
+theorem get?_modify_self {k : α} {f : β k → β k} :
+    (t.modify k f).get? k = (t.get? k).map f :=
+  Impl.get?_modify_self t.wf
+
+theorem get_modify {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f} :
+    (t.modify k f).get k' hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr heq |>.mpr <| mem_modify.mp hc
+        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| f (t.get k h')
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        t.get k' h' :=
+  Impl.get_modify t.wf
+
+@[simp]
+theorem get_modify_self {k : α} {f : β k → β k} {hc : k ∈ t.modify k f} :
+    haveI h' : k ∈ t := mem_modify.mp hc
+    (t.modify k f).get k hc = f (t.get k h') :=
+  Impl.get_modify_self t.wf
+
+theorem get!_modify {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
+    (t.modify k f).get! k' =
+      if heq : cmp k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+      else
+        t.get! k' :=
+  Impl.get!_modify t.wf
+
+@[simp]
+theorem get!_modify_self {k : α} [Inhabited (β k)] {f : β k → β k} :
+    (t.modify k f).get! k = ((t.get? k).map f).get! :=
+  Impl.get!_modify_self t.wf
+
+theorem getD_modify {k k' : α} {fallback : β k'} {f : β k → β k} :
+    (t.modify k f).getD k' fallback =
+      if heq : cmp k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+      else
+        t.getD k' fallback :=
+  Impl.getD_modify t.wf
+
+@[simp]
+theorem getD_modify_self {k : α} {fallback : β k} {f : β k → β k} :
+    (t.modify k f).getD k fallback = ((t.get? k).map f).getD fallback :=
+  Impl.getD_modify_self t.wf
+
+theorem getKey?_modify {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  Impl.getKey?_modify t.wf
+
+theorem getKey?_modify_self {k : α} {f : β k → β k} :
+    (t.modify k f).getKey? k = if k ∈ t then some k else none :=
+  Impl.getKey?_modify_self t.wf
+
+theorem getKey!_modify [Inhabited α] {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  Impl.getKey!_modify t.wf
+
+theorem getKey!_modify_self [Inhabited α] {k : α} {f : β k → β k} :
+    (t.modify k f).getKey! k = if k ∈ t then k else default :=
+  Impl.getKey!_modify_self t.wf
+
+theorem getKey_modify [Inhabited α] {k k' : α} {f : β k → β k}
+    {hc : k' ∈ t.modify k f} :
+    (t.modify k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        t.getKey k' h' :=
+  Impl.getKey_modify t.wf
+
+@[simp]
+theorem getKey_modify_self [Inhabited α] {k : α} {f : β k → β k}
+    {hc : k ∈ t.modify k f} : (t.modify k f).getKey k hc = k :=
+  Impl.getKey_modify_self t.wf
+
+theorem getKeyD_modify {k k' fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  Impl.getKeyD_modify t.wf
+
+theorem getKeyD_modify_self [Inhabited α] {k fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  Impl.getKeyD_modify_self t.wf
+
+end Dependent
+
+namespace Const
+
+variable {β : Type v} {t : DTreeMap α β cmp}
+
+@[simp]
+theorem isEmpty_modify {k : α} {f : β → β} :
+    (modify t k f).isEmpty = t.isEmpty :=
+  Impl.Const.isEmpty_modify t.wf
+
+theorem contains_modify {k k' : α} {f : β → β} :
+    (modify t k f).contains k' = t.contains k' :=
+  Impl.Const.contains_modify t.wf
+
+theorem mem_modify {k k' : α} {f : β → β} :
+    k' ∈ modify t k f ↔ k' ∈ t :=
+  Impl.Const.mem_modify t.wf
+
+theorem size_modify {k : α} {f : β → β} :
+    (modify t k f).size = t.size :=
+  Impl.Const.size_modify t.wf
+
+theorem get?_modify {k k' : α} {f : β → β} :
+    get? (modify t k f) k' =
+      if cmp k k' = .eq then
+        (get? t k).map f
+      else
+        get? t k' :=
+  Impl.Const.get?_modify t.wf
+
+@[simp]
+theorem get?_modify_self {k : α} {f : β → β} :
+    get? (modify t k f) k = (get? t k).map f :=
+  Impl.Const.get?_modify_self t.wf
+
+theorem get_modify {k k' : α} {f : β → β} {hc : k' ∈ modify t k f} :
+    get (modify t k f) k' hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr heq |>.mpr <| mem_modify.mp hc
+        f (get t k h')
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        get t k' h' :=
+  Impl.Const.get_modify t.wf
+
+@[simp]
+theorem get_modify_self {k : α} {f : β → β} {hc : k ∈ modify t k f} :
+    haveI h' : k ∈ t := mem_modify.mp hc
+    get (modify t k f) k hc = f (get t k h') :=
+  Impl.Const.get_modify_self t.wf
+
+theorem get!_modify {k k' : α} [hi : Inhabited β] {f : β → β} :
+    get! (modify t k f) k' =
+      if cmp k k' = .eq then
+        get? t k |>.map f |>.get!
+      else
+        get! t k' :=
+  Impl.Const.get!_modify t.wf
+
+@[simp]
+theorem get!_modify_self {k : α} [Inhabited β] {f : β → β} :
+    get! (modify t k f) k = ((get? t k).map f).get! :=
+  Impl.Const.get!_modify_self t.wf
+
+theorem getD_modify {k k' : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k' fallback =
+      if cmp k k' = .eq then
+        get? t k |>.map f |>.getD fallback
+      else
+        getD t k' fallback :=
+  Impl.Const.getD_modify t.wf
+
+@[simp]
+theorem getD_modify_self {k : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k fallback = ((get? t k).map f).getD fallback :=
+  Impl.Const.getD_modify_self t.wf
+
+theorem getKey?_modify {k k' : α} {f : β → β} :
+    (modify t k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  Impl.Const.getKey?_modify t.wf
+
+theorem getKey?_modify_self {k : α} {f : β → β} :
+    (modify t k f).getKey? k = if k ∈ t then some k else none :=
+  Impl.Const.getKey?_modify_self t.wf
+
+theorem getKey!_modify [Inhabited α] {k k' : α} {f : β → β} :
+    (modify t k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  Impl.Const.getKey!_modify t.wf
+
+theorem getKey!_modify_self [Inhabited α] {k : α} {f : β → β} :
+    (modify t k f).getKey! k = if k ∈ t then k else default :=
+  Impl.Const.getKey!_modify_self t.wf
+
+theorem getKey_modify [Inhabited α] {k k' : α} {f : β → β}
+    {hc : k' ∈ modify t k f} :
+    (modify t k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        t.getKey k' h' :=
+  Impl.Const.getKey_modify t.wf
+
+@[simp]
+theorem getKey_modify_self [Inhabited α] {k : α} {f : β → β}
+    {hc : k ∈ modify t k f} : (modify t k f).getKey k hc = k :=
+  Impl.Const.getKey_modify_self t.wf
+
+theorem getKeyD_modify {k k' fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  Impl.Const.getKeyD_modify t.wf
+
+theorem getKeyD_modify_self [Inhabited α] {k fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  Impl.Const.getKeyD_modify_self t.wf
+
+end Const
+
+end Modify
+
 end Std.DTreeMap
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 01ebfd90d6..148814e553 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -2446,4 +2446,268 @@ end Const
 
 end Alter
 
+section Modify
+
+variable [TransCmp cmp]
+
+section Dependent
+
+variable [LawfulEqCmp cmp]
+
+@[simp]
+theorem isEmpty_modify (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).isEmpty = t.isEmpty :=
+  Impl.isEmpty_modify h
+
+theorem contains_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).contains k' = t.contains k' :=
+  Impl.contains_modify h
+
+theorem mem_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    k' ∈ t.modify k f ↔ k' ∈ t :=
+  Impl.mem_modify h
+
+theorem size_modify (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).size = t.size :=
+  Impl.size_modify h
+
+theorem get?_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).get? k' =
+      if h : cmp k k' = .eq then
+        (cast (congrArg (Option ∘ β) (compare_eq_iff_eq.mp h)) ((t.get? k).map f))
+      else
+        t.get? k' :=
+  Impl.get?_modify h
+
+@[simp]
+theorem get?_modify_self (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).get? k = (t.get? k).map f :=
+  Impl.get?_modify_self h
+
+theorem get_modify (h : t.WF) {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f} :
+    (t.modify k f).get k' hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
+        cast (congrArg β (compare_eq_iff_eq.mp heq)) <| f (t.get k h')
+      else
+        haveI h' : k' ∈ t := (mem_modify h).mp hc
+        t.get k' h' :=
+  Impl.get_modify h
+
+@[simp]
+theorem get_modify_self (h : t.WF) {k : α} {f : β k → β k} {hc : k ∈ t.modify k f} :
+    haveI h' : k ∈ t := mem_modify h |>.mp hc
+    (t.modify k f).get k hc = f (t.get k h') :=
+  Impl.get_modify_self h
+
+theorem get!_modify (h : t.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
+    (t.modify k f).get! k' =
+      if heq : cmp k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β (compare_eq_iff_eq.mp heq))) |>.get!
+      else
+        t.get! k' :=
+  Impl.get!_modify h
+
+@[simp]
+theorem get!_modify_self (h : t.WF) {k : α} [Inhabited (β k)] {f : β k → β k} :
+    (t.modify k f).get! k = ((t.get? k).map f).get! :=
+  Impl.get!_modify_self h
+
+theorem getD_modify (h : t.WF) {k k' : α} {fallback : β k'} {f : β k → β k} :
+    (t.modify k f).getD k' fallback =
+      if heq : cmp k k' = .eq then
+        t.get? k |>.map f |>.map (cast (congrArg β <| compare_eq_iff_eq.mp heq)) |>.getD fallback
+      else
+        t.getD k' fallback :=
+  Impl.getD_modify h
+
+@[simp]
+theorem getD_modify_self (h : t.WF) {k : α} {fallback : β k} {f : β k → β k} :
+    (t.modify k f).getD k fallback = ((t.get? k).map f).getD fallback :=
+  Impl.getD_modify_self h
+
+theorem getKey?_modify (h : t.WF) {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  Impl.getKey?_modify h
+
+theorem getKey?_modify_self (h : t.WF) {k : α} {f : β k → β k} :
+    (t.modify k f).getKey? k = if k ∈ t then some k else none :=
+  Impl.getKey?_modify_self h
+
+theorem getKey!_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k} :
+    (t.modify k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  Impl.getKey!_modify h
+
+theorem getKey!_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β k → β k} :
+    (t.modify k f).getKey! k = if k ∈ t then k else default :=
+  Impl.getKey!_modify_self h
+
+theorem getKey_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k}
+    {hc : k' ∈ t.modify k f} :
+    (t.modify k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t.getKey k' h' :=
+  Impl.getKey_modify h
+
+@[simp]
+theorem getKey_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β k → β k}
+    {hc : k ∈ t.modify k f} : (t.modify k f).getKey k hc = k :=
+  Impl.getKey_modify_self h
+
+theorem getKeyD_modify (h : t.WF) {k k' fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  Impl.getKeyD_modify h
+
+theorem getKeyD_modify_self (h : t.WF) [Inhabited α] {k fallback : α} {f : β k → β k} :
+    (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  Impl.getKeyD_modify_self h
+
+end Dependent
+
+namespace Const
+
+variable {β : Type v} {t : Raw α β cmp}
+
+@[simp]
+theorem isEmpty_modify (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).isEmpty = t.isEmpty :=
+  Impl.Const.isEmpty_modify h
+
+theorem contains_modify (h : t.WF) {k k' : α} {f : β → β} :
+    (modify t k f).contains k' = t.contains k' :=
+  Impl.Const.contains_modify h
+
+theorem mem_modify (h : t.WF) {k k' : α} {f : β → β} :
+    k' ∈ modify t k f ↔ k' ∈ t :=
+  Impl.Const.mem_modify h
+
+theorem size_modify (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).size = t.size :=
+  Impl.Const.size_modify h
+
+theorem get?_modify (h : t.WF) {k k' : α} {f : β → β} :
+    get? (modify t k f) k' =
+      if cmp k k' = .eq then
+        (get? t k).map f
+      else
+        get? t k' :=
+  Impl.Const.get?_modify h
+
+@[simp]
+theorem get?_modify_self (h : t.WF) {k : α} {f : β → β} :
+    get? (modify t k f) k = (get? t k).map f :=
+  Impl.Const.get?_modify_self h
+
+theorem get_modify (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ modify t k f} :
+    get (modify t k f) k' hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
+        f (get t k h')
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        get t k' h' :=
+  Impl.Const.get_modify h
+
+@[simp]
+theorem get_modify_self (h : t.WF) {k : α} {f : β → β} {hc : k ∈ modify t k f} :
+    haveI h' : k ∈ t := mem_modify h |>.mp hc
+    get (modify t k f) k hc = f (get t k h') :=
+  Impl.Const.get_modify_self h
+
+theorem get!_modify (h : t.WF) {k k' : α} [hi : Inhabited β] {f : β → β} :
+    get! (modify t k f) k' =
+      if cmp k k' = .eq then
+        get? t k |>.map f |>.get!
+      else
+        get! t k' :=
+  Impl.Const.get!_modify h
+
+@[simp]
+theorem get!_modify_self (h : t.WF) {k : α} [Inhabited β] {f : β → β} :
+    get! (modify t k f) k = ((get? t k).map f).get! :=
+  Impl.Const.get!_modify_self h
+
+theorem getD_modify (h : t.WF) {k k' : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k' fallback =
+      if cmp k k' = .eq then
+        get? t k |>.map f |>.getD fallback
+      else
+        getD t k' fallback :=
+  Impl.Const.getD_modify h
+
+@[simp]
+theorem getD_modify_self (h : t.WF) {k : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k fallback = ((get? t k).map f).getD fallback :=
+  Impl.Const.getD_modify_self h
+
+theorem getKey?_modify (h : t.WF) {k k' : α} {f : β → β} :
+    (modify t k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  Impl.Const.getKey?_modify h
+
+theorem getKey?_modify_self (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).getKey? k = if k ∈ t then some k else none :=
+  Impl.Const.getKey?_modify_self h
+
+theorem getKey!_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} :
+    (modify t k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  Impl.Const.getKey!_modify h
+
+theorem getKey!_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β → β} :
+    (modify t k f).getKey! k = if k ∈ t then k else default :=
+  Impl.Const.getKey!_modify_self h
+
+theorem getKey_modify (h : t.WF) [Inhabited α] {k k' : α} {f : β → β}
+    {hc : k' ∈ modify t k f} :
+    (modify t k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t.getKey k' h' :=
+  Impl.Const.getKey_modify h
+
+@[simp]
+theorem getKey_modify_self (h : t.WF) [Inhabited α] {k : α} {f : β → β}
+    {hc : k ∈ modify t k f} : (modify t k f).getKey k hc = k :=
+  Impl.Const.getKey_modify_self h
+
+theorem getKeyD_modify (h : t.WF) {k k' fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  Impl.Const.getKeyD_modify h
+
+theorem getKeyD_modify_self (h : t.WF) [Inhabited α] {k fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  Impl.Const.getKeyD_modify_self h
+
+end Const
+
+end Modify
+
 end Std.DTreeMap.Raw
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index cded9c85d5..e57b8b7baf 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -1549,4 +1549,131 @@ theorem getKeyD_alter_self [TransCmp cmp] [Inhabited α] {k : α} {fallback : α
 
 end Alter
 
+section Modify
+
+@[simp]
+theorem isEmpty_modify [TransCmp cmp] {k : α} {f : β → β} :
+    (modify t k f).isEmpty = t.isEmpty :=
+  DTreeMap.Const.isEmpty_modify
+
+theorem contains_modify [TransCmp cmp] {k k' : α} {f : β → β} :
+    (modify t k f).contains k' = t.contains k' :=
+  DTreeMap.Const.contains_modify
+
+theorem mem_modify [TransCmp cmp] {k k' : α} {f : β → β} :
+    k' ∈ modify t k f ↔ k' ∈ t :=
+  DTreeMap.Const.mem_modify
+
+theorem size_modify [TransCmp cmp] {k : α} {f : β → β} :
+    (modify t k f).size = t.size :=
+  DTreeMap.Const.size_modify
+
+theorem getElem?_modify [TransCmp cmp] {k k' : α} {f : β → β} :
+    (modify t k f)[k']? =
+      if cmp k k' = .eq then
+        t[k]?.map f
+      else
+        t[k']? :=
+  DTreeMap.Const.get?_modify
+
+@[simp]
+theorem getElem?_modify_self [TransCmp cmp] {k : α} {f : β → β} :
+    (modify t k f)[k]? = t[k]?.map f :=
+  DTreeMap.Const.get?_modify_self
+
+theorem getElem_modify [TransCmp cmp] {k k' : α} {f : β → β} {hc : k' ∈ modify t k f} :
+    (modify t k f)[k']'hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr heq |>.mpr <| mem_modify.mp hc
+        f (t[k]'h')
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        t[k']'h' :=
+  DTreeMap.Const.get_modify
+
+@[simp]
+theorem getElem_modify_self [TransCmp cmp] {k : α} {f : β → β} {hc : k ∈ modify t k f} :
+    haveI h' : k ∈ t := mem_modify.mp hc
+    (modify t k f)[k]'hc = f (t[k]'h') :=
+  DTreeMap.Const.get_modify_self
+
+theorem getElem!_modify [TransCmp cmp] {k k' : α} [hi : Inhabited β] {f : β → β} :
+    (modify t k f)[k']! =
+      if cmp k k' = .eq then
+        t[k]? |>.map f |>.get!
+      else
+        t[k']! :=
+  DTreeMap.Const.get!_modify
+
+@[simp]
+theorem getElem!_modify_self [TransCmp cmp] {k : α} [Inhabited β] {f : β → β} :
+    (modify t k f)[k]! = (t[k]?.map f).get! :=
+  DTreeMap.Const.get!_modify_self
+
+theorem getD_modify [TransCmp cmp] {k k' : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k' fallback =
+      if cmp k k' = .eq then
+        t[k]?.map f |>.getD fallback
+      else
+        getD t k' fallback :=
+  DTreeMap.Const.getD_modify
+
+@[simp]
+theorem getD_modify_self [TransCmp cmp] {k : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k fallback = (t[k]?.map f).getD fallback :=
+  DTreeMap.Const.getD_modify_self
+
+theorem getKey?_modify [TransCmp cmp] {k k' : α} {f : β → β} :
+    (modify t k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  DTreeMap.Const.getKey?_modify
+
+theorem getKey?_modify_self [TransCmp cmp] {k : α} {f : β → β} :
+    (modify t k f).getKey? k = if k ∈ t then some k else none :=
+  DTreeMap.Const.getKey?_modify_self
+
+theorem getKey!_modify [TransCmp cmp] [Inhabited α] {k k' : α} {f : β → β} :
+    (modify t k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  DTreeMap.Const.getKey!_modify
+
+theorem getKey!_modify_self [TransCmp cmp] [Inhabited α] {k : α} {f : β → β} :
+    (modify t k f).getKey! k = if k ∈ t then k else default :=
+  DTreeMap.Const.getKey!_modify_self
+
+theorem getKey_modify [TransCmp cmp] [Inhabited α] {k k' : α} {f : β → β}
+    {hc : k' ∈ modify t k f} :
+    (modify t k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify.mp hc
+        t.getKey k' h' :=
+  DTreeMap.Const.getKey_modify
+
+@[simp]
+theorem getKey_modify_self [TransCmp cmp] [Inhabited α] {k : α} {f : β → β}
+    {hc : k ∈ modify t k f} : (modify t k f).getKey k hc = k :=
+  DTreeMap.Const.getKey_modify_self
+
+theorem getKeyD_modify [TransCmp cmp] {k k' fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  DTreeMap.Const.getKeyD_modify
+
+theorem getKeyD_modify_self [TransCmp cmp] [Inhabited α] {k fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  DTreeMap.Const.getKeyD_modify_self
+
+end Modify
+
 end Std.TreeMap
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index e4072a9f98..2d9b9c2dbd 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -1557,4 +1557,131 @@ theorem getKeyD_alter_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {fa
 
 end Alter
 
+section Modify
+
+@[simp]
+theorem isEmpty_modify [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).isEmpty = t.isEmpty :=
+  DTreeMap.Raw.Const.isEmpty_modify h
+
+theorem contains_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} :
+    (modify t k f).contains k' = t.contains k' :=
+  DTreeMap.Raw.Const.contains_modify h
+
+theorem mem_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} :
+    k' ∈ modify t k f ↔ k' ∈ t :=
+  DTreeMap.Raw.Const.mem_modify h
+
+theorem size_modify [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).size = t.size :=
+  DTreeMap.Raw.Const.size_modify h
+
+theorem getElem?_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} :
+    (modify t k f)[k']? =
+      if cmp k k' = .eq then
+        t[k]?.map f
+      else
+        t[k']? :=
+  DTreeMap.Raw.Const.get?_modify h
+
+@[simp]
+theorem getElem?_modify_self [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f)[k]? = t[k]?.map f :=
+  DTreeMap.Raw.Const.get?_modify_self h
+
+theorem getElem_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ modify t k f} :
+    (modify t k f)[k']'hc =
+      if heq : cmp k k' = .eq then
+        haveI h' : k ∈ t := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
+        f (t[k]'h')
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t[k']'h' :=
+  DTreeMap.Raw.Const.get_modify h
+
+@[simp]
+theorem getElem_modify_self [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {hc : k ∈ modify t k f} :
+    haveI h' : k ∈ t := mem_modify h |>.mp hc
+    (modify t k f)[k]'hc = f (t[k]'h') :=
+  DTreeMap.Raw.Const.get_modify_self h
+
+theorem getElem!_modify [TransCmp cmp] (h : t.WF) {k k' : α} [hi : Inhabited β] {f : β → β} :
+    (modify t k f)[k']! =
+      if cmp k k' = .eq then
+        t[k]? |>.map f |>.get!
+      else
+        t[k']! :=
+  DTreeMap.Raw.Const.get!_modify h
+
+@[simp]
+theorem getElem!_modify_self [TransCmp cmp] (h : t.WF) {k : α} [Inhabited β] {f : β → β} :
+    (modify t k f)[k]! = (t[k]?.map f).get! :=
+  DTreeMap.Raw.Const.get!_modify_self h
+
+theorem getD_modify [TransCmp cmp] (h : t.WF) {k k' : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k' fallback =
+      if cmp k k' = .eq then
+        t[k]?.map f |>.getD fallback
+      else
+        getD t k' fallback :=
+  DTreeMap.Raw.Const.getD_modify h
+
+@[simp]
+theorem getD_modify_self [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} {f : β → β} :
+    getD (modify t k f) k fallback = (t[k]?.map f).getD fallback :=
+  DTreeMap.Raw.Const.getD_modify_self h
+
+theorem getKey?_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} :
+    (modify t k f).getKey? k' =
+      if cmp k k' = .eq then
+        if k ∈ t then some k else none
+      else
+        t.getKey? k' :=
+  DTreeMap.Raw.Const.getKey?_modify h
+
+theorem getKey?_modify_self [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} :
+    (modify t k f).getKey? k = if k ∈ t then some k else none :=
+  DTreeMap.Raw.Const.getKey?_modify_self h
+
+theorem getKey!_modify [TransCmp cmp] (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} :
+    (modify t k f).getKey! k' =
+      if cmp k k' = .eq then
+        if k ∈ t then k else default
+      else
+        t.getKey! k' :=
+  DTreeMap.Raw.Const.getKey!_modify h
+
+theorem getKey!_modify_self [TransCmp cmp] (h : t.WF) [Inhabited α] {k : α} {f : β → β} :
+    (modify t k f).getKey! k = if k ∈ t then k else default :=
+  DTreeMap.Raw.Const.getKey!_modify_self h
+
+theorem getKey_modify [TransCmp cmp] (h : t.WF) [Inhabited α] {k k' : α} {f : β → β}
+    {hc : k' ∈ modify t k f} :
+    (modify t k f).getKey k' hc =
+      if cmp k k' = .eq then
+        k
+      else
+        haveI h' : k' ∈ t := mem_modify h |>.mp hc
+        t.getKey k' h' :=
+  DTreeMap.Raw.Const.getKey_modify h
+
+@[simp]
+theorem getKey_modify_self [TransCmp cmp] (h : t.WF) [Inhabited α] {k : α} {f : β → β}
+    {hc : k ∈ modify t k f} : (modify t k f).getKey k hc = k :=
+  DTreeMap.Raw.Const.getKey_modify_self h
+
+theorem getKeyD_modify [TransCmp cmp] (h : t.WF) {k k' fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k' fallback =
+      if cmp k k' = .eq then
+        if k ∈ t then k else fallback
+      else
+        t.getKeyD k' fallback :=
+  DTreeMap.Raw.Const.getKeyD_modify h
+
+theorem getKeyD_modify_self [TransCmp cmp] (h : t.WF) [Inhabited α] {k fallback : α} {f : β → β} :
+    (modify t k f).getKeyD k fallback = if k ∈ t then k else fallback :=
+  DTreeMap.Raw.Const.getKeyD_modify_self h
+
+end Modify
+
 end Std.TreeMap.Raw