diff --git a/src/Std/Data/DTreeMap/Internal/Cell.lean b/src/Std/Data/DTreeMap/Internal/Cell.lean
index 3ffd990507..8e2477d6a2 100644
--- a/src/Std/Data/DTreeMap/Internal/Cell.lean
+++ b/src/Std/Data/DTreeMap/Internal/Cell.lean
@@ -97,6 +97,16 @@ theorem get?_empty [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} :
     (Cell.empty : Cell α β (compare k)).get? = none :=
   rfl
 
+/-- Internal implementation detail of the tree map -/
+def getKey? [Ord α] {k : α} (c : Cell α β (compare k)) : Option α :=
+  match c.inner with
+  | none => none
+  | some p => some p.1
+
+@[simp]
+theorem getKey?_empty [Ord α] {k : α} : (Cell.empty : Cell α β (compare k)).getKey? = none :=
+  rfl
+
 /-- Internal implementation detail of the tree map -/
 def alter [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α}
     (f : Option (β k) → Option (β k)) (c : Cell α β (compare k)) :
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index a7c94c6c9c..8c4bb37bea 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -49,22 +49,17 @@ open Lean
 
 theorem compare_eq_eq_iff_beq {k a : α} : compare k a = .eq ↔ k == a := beq_iff_eq.symm
 
-theorem dif_compare {γ} [LawfulEqOrd α] {k a : α} {f : compare k a = .eq → γ} {g : ¬ compare k a = .eq → γ} :
-    (if h : compare k a = .eq then f h else g h) =
-      (if h : k == a then f (eq_of_beq h) else g (h ∘ beq_of_eq)) := by
-  split
-  · exact Eq.symm <| dif_pos (beq_of_eq ‹_› :)
-  · exact Eq.symm <| dif_neg (‹_› ∘ eq_of_beq :)
-
 private def helperLemmaNames : Array Name :=
-  #[``dif_compare, ``compare_eq_eq_iff_beq]
+  #[``compare_eq_eq_iff_beq]
 
 private def queryNames : Array Name :=
   #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length,
     ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?,
     ``get_eq_getValueCast, ``Const.get_eq_getValue,
     ``get!_eq_getValueCast!, ``Const.get!_eq_getValue!,
-    ``getD_eq_getValueCastD, ``Const.getD_eq_getValueD]
+    ``getD_eq_getValueCastD, ``Const.getD_eq_getValueD,
+    ``getKey?_eq_getKey?, ``getKey_eq_getKey,
+    ``getKey!_eq_getKey!, ``getKeyD_eq_getKeyD]
 
 private def modifyMap : Std.HashMap Name Name :=
   .ofList
@@ -124,14 +119,6 @@ theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq
     k ∈ t ↔ k' ∈ t := by
   simp [mem_iff_contains, contains_congr h hab]
 
-theorem isEmpty_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
-    (t.insertIfNew k v h.balanced).impl.isEmpty = false := by
-  simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew
-
-theorem isEmpty_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
-    (t.insertIfNew! k v).isEmpty = false := by
-  simp_to_model [insertIfNew!] using List.isEmpty_insertEntryIfNew
-
 theorem contains_empty {a : α} : (empty : Impl α β).contains a = false := by
   simp [contains, empty]
 
@@ -353,6 +340,14 @@ theorem containsThenInsertIfNew!_snd [TransOrd α] (h : t.WF) {k : α} {v : β k
   rw [containsThenInsertIfNew!_snd_eq_containsThenInsertIfNew_snd _ h.balanced, containsThenInsertIfNew_snd h,
     insertIfNew_eq_insertIfNew!]
 
+theorem isEmpty_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.isEmpty = false := by
+  simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew
+
+theorem isEmpty_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew! k v).isEmpty = false := by
+  simp_to_model [insertIfNew!] using List.isEmpty_insertEntryIfNew
+
 theorem contains_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
     (t.insertIfNew k v h.balanced).impl.contains a = (k == a || t.contains a) := by
   simp_to_model [insertIfNew] using List.containsKey_insertEntryIfNew
@@ -947,4 +942,449 @@ theorem getD_congr [TransOrd α] (h : t.WF) {a b : α} {fallback : β}
 
 end Const
 
+theorem getKey?_empty {a : α} : (empty : Impl α β).getKey? a = none := by
+  simp [empty, getKey?]
+
+theorem getKey?_of_isEmpty [TransOrd α] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey? a = none := by
+  simp_to_model; empty
+
+theorem getKey?_insert [TransOrd α] (h : t.WF) {a k : α} {v : β k} :
+    (t.insert k v h.balanced).impl.getKey? a = if compare k a = .eq then some k else t.getKey? a := by
+  simp_to_model [insert] using List.getKey?_insertEntry
+
+theorem getKey?_insert! [TransOrd α] (h : t.WF) {a k : α} {v : β k} :
+    (t.insert! k v).getKey? a = if compare k a = .eq then some k else t.getKey? a := by
+  simp_to_model [insert!] using List.getKey?_insertEntry
+
+theorem getKey?_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v h.balanced).impl.getKey? k = some k := by
+  simp_to_model [insert] using List.getKey?_insertEntry_self
+
+theorem getKey?_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert! k v).getKey? k = some k := by
+  simp_to_model [insert!] using List.getKey?_insertEntry_self
+
+theorem contains_eq_isSome_getKey? [TransOrd α] (h : t.WF) {a : α} :
+    t.contains a = (t.getKey? a).isSome := by
+  simp_to_model using List.containsKey_eq_isSome_getKey?
+
+theorem mem_iff_isSome_getKey? [TransOrd α] (h : t.WF) {a : α} :
+    a ∈ t ↔ (t.getKey? a).isSome := by
+  simpa [mem_iff_contains] using contains_eq_isSome_getKey? h
+
+theorem getKey?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey? a = none := by
+  simp_to_model using List.getKey?_eq_none
+
+theorem getKey?_eq_none [TransOrd α] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey? a = none := by
+  simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false h
+
+theorem getKey?_erase [TransOrd α] (h : t.WF) {k a : α} :
+    (t.erase k h.balanced).impl.getKey? a = if compare k a = .eq then none else t.getKey? a := by
+  simp_to_model [erase] using List.getKey?_eraseKey
+
+theorem getKey?_erase! [TransOrd α] (h : t.WF) {k a : α} :
+    (t.erase! k).getKey? a = if compare k a = .eq then none else t.getKey? a := by
+  simp_to_model [erase!] using List.getKey?_eraseKey
+
+theorem getKey?_erase_self [TransOrd α] (h : t.WF) {k : α} :
+    (t.erase k h.balanced).impl.getKey? k = none := by
+  simp_to_model [erase] using List.getKey?_eraseKey_self
+
+theorem getKey?_erase!_self [TransOrd α] (h : t.WF) {k : α} :
+    (t.erase! k).getKey? k = none := by
+  simp_to_model [erase!] using List.getKey?_eraseKey_self
+
+theorem getKey_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insert k v h.balanced).impl.getKey a h₁ =
+      if h₂ : compare k a = .eq then
+        k
+      else
+        t.getKey a (contains_of_contains_insert h h₁ h₂) := by
+  simp_to_model [insert] using List.getKey_insertEntry
+
+theorem getKey_insert! [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insert! k v).getKey a h₁ =
+      if h₂ : compare k a = .eq then
+        k
+      else
+        t.getKey a (contains_of_contains_insert! h h₁ h₂) := by
+  simp_to_model [insert!] using List.getKey_insertEntry
+
+theorem getKey_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v h.balanced).impl.getKey k (contains_insert_self h) = k := by
+  simp_to_model [insert] using List.getKey_insertEntry_self
+
+theorem getKey_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert! k v).getKey k (contains_insert!_self h) = k := by
+  simp_to_model [insert!] using List.getKey_insertEntry_self
+
+@[simp]
+theorem getKey_erase [TransOrd α] (h : t.WF) {k a : α} {h'} :
+    (t.erase k h.balanced).impl.getKey a h' = t.getKey a (contains_of_contains_erase h h') := by
+  simp_to_model [erase] using List.getKey_eraseKey
+
+@[simp]
+theorem getKey_erase! [TransOrd α] (h : t.WF) {k a : α} {h'} :
+    (t.erase! k).getKey a h' = t.getKey a (contains_of_contains_erase! h h') := by
+  simp_to_model [erase!] using List.getKey_eraseKey
+
+theorem getKey?_eq_some_getKey [TransOrd α] (h : t.WF) {a : α} {h'} :
+    t.getKey? a = some (t.getKey a h') := by
+  simp_to_model using List.getKey?_eq_some_getKey
+
+theorem getKey!_empty {a : α} [Inhabited α] :
+    (empty : Impl α β).getKey! a = default := by
+  simp only [empty, getKey!]; rfl
+
+theorem getKey!_of_isEmpty [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey! a = default := by
+  simp_to_model; empty;
+
+theorem getKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β k} :
+    (t.insert k v h.balanced).impl.getKey! a = if compare k a = .eq then k else t.getKey! a := by
+  simp_to_model [insert] using List.getKey!_insertEntry
+
+theorem getKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β k} :
+    (t.insert! k v).getKey! a = if compare k a = .eq then k else t.getKey! a := by
+  simp_to_model [insert!] using List.getKey!_insertEntry
+
+theorem getKey!_insert_self [TransOrd α] [Inhabited α] (h : t.WF) {a : α}
+    {b : β a} : (t.insert a b h.balanced).impl.getKey! a = a := by
+  simp_to_model [insert] using List.getKey!_insertEntry_self
+
+theorem getKey!_insert!_self [TransOrd α] [Inhabited α] (h : t.WF) {a : α}
+    {b : β a} : (t.insert! a b).getKey! a = a := by
+  simp_to_model [insert!] using List.getKey!_insertEntry_self
+
+theorem getKey!_eq_default_of_contains_eq_false [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey! a = default := by
+  simp_to_model using List.getKey!_eq_default
+
+theorem getKey!_eq_default [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey! a = default := by
+  simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false h
+
+theorem getKey!_erase [TransOrd α] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.erase k h.balanced).impl.getKey! a = if compare k a = .eq then default else t.getKey! a := by
+  simp_to_model [erase] using List.getKey!_eraseKey
+
+theorem getKey!_erase! [TransOrd α] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.erase! k).getKey! a = if compare k a = .eq then default else t.getKey! a := by
+  simp_to_model [erase!] using List.getKey!_eraseKey
+
+theorem getKey!_erase_self [TransOrd α] [Inhabited α] (h : t.WF) {k : α} :
+    (t.erase k h.balanced).impl.getKey! k = default := by
+  simp_to_model [erase] using List.getKey!_eraseKey_self
+
+theorem getKey!_erase!_self [TransOrd α] [Inhabited α] (h : t.WF) {k : α} :
+    (t.erase! k).getKey! k = default := by
+  simp_to_model [erase!] using List.getKey!_eraseKey_self
+
+theorem getKey?_eq_some_getKey!_of_contains [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = true → t.getKey? a = some (t.getKey! a) := by
+  simp_to_model using List.getKey?_eq_some_getKey!
+
+theorem getKey?_eq_some_getKey! [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    a ∈ t → t.getKey? a = some (t.getKey! a) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains h
+
+theorem getKey!_eq_get!_getKey? [TransOrd α] [Inhabited α] (h : t.WF) {a : α} :
+    t.getKey! a = (t.getKey? a).get! := by
+  simp_to_model using List.getKey!_eq_getKey?
+
+theorem getKey_eq_getKey! [TransOrd α] [Inhabited α] (h : t.WF) {a : α} {h} :
+    t.getKey a h = t.getKey! a := by
+  simp_to_model using List.getKey_eq_getKey!
+
+theorem getKeyD_empty {a : α} {fallback : α} :
+    (empty : Impl α β).getKeyD a fallback = fallback := by
+  simp [getKeyD, empty]
+
+theorem getKeyD_of_isEmpty [TransOrd α] (h : t.WF) {a fallback : α} :
+    t.isEmpty = true → t.getKeyD a fallback = fallback := by
+  simp_to_model; empty
+
+theorem getKeyD_insert [TransOrd α] (h : t.WF) {k a fallback : α} {v : β k} :
+    (t.insert k v h.balanced).impl.getKeyD a fallback =
+      if compare k a = .eq then k else t.getKeyD a fallback := by
+  simp_to_model [insert] using List.getKeyD_insertEntry
+
+theorem getKeyD_insert! [TransOrd α] (h : t.WF) {k a fallback : α} {v : β k} :
+    (t.insert! k v).getKeyD a fallback =
+      if compare k a = .eq then k else t.getKeyD a fallback := by
+  simp_to_model [insert!] using List.getKeyD_insertEntry
+
+theorem getKeyD_insert_self [TransOrd α] (h : t.WF) {a fallback : α}
+    {b : β a} :
+    (t.insert a b h.balanced).impl.getKeyD a fallback = a := by
+  simp_to_model [insert] using List.getKeyD_insertEntry_self
+
+theorem getKeyD_insert!_self [TransOrd α] (h : t.WF) {a fallback : α}
+    {b : β a} :
+    (t.insert! a b).getKeyD a fallback = a := by
+  simp_to_model [insert!] using List.getKeyD_insertEntry_self
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [TransOrd α] (h : t.WF) {a fallback : α} :
+    t.contains a = false → t.getKeyD a fallback = fallback := by
+  simp_to_model using List.getKeyD_eq_fallback
+
+theorem getKeyD_eq_fallback [TransOrd α] (h : t.WF) {a fallback : α} :
+    ¬ a ∈ t → t.getKeyD a fallback = fallback := by
+  simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false h
+
+theorem getKeyD_erase [TransOrd α] (h : t.WF) {k a fallback : α} :
+    (t.erase k h.balanced).impl.getKeyD a fallback =
+      if compare k a = .eq then fallback else t.getKeyD a fallback := by
+  simp_to_model [erase] using List.getKeyD_eraseKey
+
+theorem getKeyD_erase! [TransOrd α] (h : t.WF) {k a fallback : α} :
+    (t.erase! k).getKeyD a fallback =
+      if compare k a = .eq then fallback else t.getKeyD a fallback := by
+  simp_to_model [erase!] using List.getKeyD_eraseKey
+
+theorem getKeyD_erase_self [TransOrd α] (h : t.WF) {k fallback : α} :
+    (t.erase k h.balanced).impl.getKeyD k fallback = fallback := by
+  simp_to_model [erase] using List.getKeyD_eraseKey_self
+
+theorem getKeyD_erase!_self [TransOrd α] (h : t.WF) {k fallback : α} :
+    (t.erase! k).getKeyD k fallback = fallback := by
+  simp_to_model [erase!] using List.getKeyD_eraseKey_self
+
+theorem getKey?_eq_some_getKeyD_of_contains [TransOrd α] (h : t.WF) {a fallback : α} :
+    t.contains a = true → t.getKey? a = some (t.getKeyD a fallback) := by
+  simp_to_model using List.getKey?_eq_some_getKeyD
+
+theorem getKey?_eq_some_getKeyD [TransOrd α] (h : t.WF) {a fallback : α} :
+    a ∈ t → t.getKey? a = some (t.getKeyD a fallback) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains h
+
+theorem getKeyD_eq_getD_getKey? [TransOrd α] (h : t.WF) {a fallback : α} :
+    t.getKeyD a fallback = (t.getKey? a).getD fallback := by
+  simp_to_model using List.getKeyD_eq_getKey?
+
+theorem getKey_eq_getKeyD [TransOrd α] (h : t.WF) {a fallback : α} {h} :
+    t.getKey a h = t.getKeyD a fallback := by
+  simp_to_model using List.getKey_eq_getKeyD
+
+theorem getKey!_eq_getKeyD_default [TransOrd α] [Inhabited α] (h : t.WF)
+    {a : α} :
+    t.getKey! a = t.getKeyD a default := by
+  simp_to_model using List.getKey!_eq_getKeyD_default
+
+/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insertIfNew' [TransOrd α] (h : t.WF) {k a : α}
+    {v : β k} :
+    a ∈ (t.insertIfNew k v h.balanced).impl →
+      ¬ (compare k a = .eq ∧ ¬ k ∈ t) → a ∈ t := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew'
+
+/-- This is a restatement of `contains_of_contains_insertIfNew!` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew!`. -/
+theorem mem_of_mem_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α}
+    {v : β k} :
+    a ∈ (t.insertIfNew! k v) → ¬ (compare k a = .eq ∧ ¬ k ∈ t) → a ∈ t := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.containsKey_of_containsKey_insertEntryIfNew'
+
+theorem get?_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.get? a =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+      else
+        t.get? a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValueCast?_insertEntryIfNew
+
+theorem get?_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew! k v).get? a =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+      else
+        t.get? a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValueCast?_insertEntryIfNew
+
+theorem get_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v h.balanced).impl.get a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+      else
+        t.get a (mem_of_mem_insertIfNew' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValueCast_insertEntryIfNew
+
+theorem get_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew! k v).get a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+      else
+        t.get a (mem_of_mem_insertIfNew!' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValueCast_insertEntryIfNew
+
+theorem get!_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.get! a =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.get! a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValueCast!_insertEntryIfNew
+
+theorem get!_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
+    (t.insertIfNew! k v).get! a =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.get! a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValueCast!_insertEntryIfNew
+
+theorem getD_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.getD a fallback =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.getD a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValueCastD_insertEntryIfNew
+
+theorem getD_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
+    (t.insertIfNew! k v).getD a fallback =
+      if h : compare k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.getD a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValueCastD_insertEntryIfNew
+
+namespace Const
+
+variable {β : Type v} {t : Impl α β}
+
+theorem get?_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β} :
+    get? (t.insertIfNew k v h.balanced).impl a =
+      if compare k a = .eq ∧ ¬ k ∈ t then
+        some v
+      else
+        get? t a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValue?_insertEntryIfNew
+
+theorem get?_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} :
+    get? (t.insertIfNew! k v) a =
+      if compare k a = .eq ∧ ¬ k ∈ t then
+        some v
+      else
+        get? t a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValue?_insertEntryIfNew
+
+theorem get_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} :
+    get (t.insertIfNew k v h.balanced).impl a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then
+        v
+      else
+        get t a (mem_of_mem_insertIfNew' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValue_insertEntryIfNew
+
+theorem get_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} :
+    get (t.insertIfNew! k v) a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then
+        v
+      else
+        get t a (mem_of_mem_insertIfNew!' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValue_insertEntryIfNew
+
+theorem get!_insertIfNew [TransOrd α] [Inhabited β] (h : t.WF) {k a : α}
+    {v : β} :
+    get! (t.insertIfNew k v h.balanced).impl a =
+      if compare k a = .eq ∧ ¬ k ∈ t then v else get! t a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValue!_insertEntryIfNew
+
+theorem get!_insertIfNew! [TransOrd α] [Inhabited β] (h : t.WF) {k a : α}
+    {v : β} :
+    get! (t.insertIfNew! k v) a =
+      if compare k a = .eq ∧ ¬ k ∈ t then v else get! t a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValue!_insertEntryIfNew
+
+theorem getD_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} :
+    getD (t.insertIfNew k v h.balanced).impl a fallback =
+      if compare k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getValueD_insertEntryIfNew
+
+theorem getD_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} :
+    getD (t.insertIfNew! k v) a fallback =
+      if compare k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getValueD_insertEntryIfNew
+
+end Const
+
+theorem getKey?_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.getKey? a =
+      if compare k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getKey?_insertEntryIfNew
+
+theorem getKey?_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew! k v).getKey? a =
+      if compare k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getKey?_insertEntryIfNew
+
+theorem getKey_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v h.balanced).impl.getKey a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getKey_insertEntryIfNew
+
+theorem getKey_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew! k v).getKey a h₁ =
+      if h₂ : compare k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew!' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getKey_insertEntryIfNew
+
+theorem getKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.getKey! a =
+      if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getKey!_insertEntryIfNew
+
+theorem getKey!_insertIfNew! [TransOrd α] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β k} :
+    (t.insertIfNew! k v).getKey! a =
+      if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getKey!_insertEntryIfNew
+
+theorem getKeyD_insertIfNew [TransOrd α] (h : t.WF) {k a fallback : α}
+    {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.getKeyD a fallback =
+      if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew] using List.getKeyD_insertEntryIfNew
+
+theorem getKeyD_insertIfNew! [TransOrd α] (h : t.WF) {k a fallback : α}
+    {v : β k} :
+    (t.insertIfNew! k v).getKeyD a fallback =
+      if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_model [insertIfNew!] using List.getKeyD_insertEntryIfNew
+
 end Std.DTreeMap.Internal.Impl
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index c30f44e7a8..756a71f181 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -234,6 +234,34 @@ Internal implementation detail of the tree map
 def getDₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) : β k :=
   get?ₘ l k |>.getD fallback
 
+/--
+Model implementation of the `getKey?` function.
+Internal implementation detail of the tree map
+-/
+def getKey?ₘ [Ord α] (l : Impl α β) (k : α) : Option α :=
+  applyCell k l fun c _ => c.getKey?
+
+/--
+Model implementation of the `getKey` function.
+Internal implementation detail of the tree map
+-/
+def getKeyₘ [Ord α] (l : Impl α β) (k : α) (h : (getKey?ₘ l k).isSome) : α :=
+  getKey?ₘ l k |>.get h
+
+/--
+Model implementation of the `getKey!` function.
+Internal implementation detail of the tree map
+-/
+def getKey!ₘ [Ord α] (l : Impl α β) (k : α) [Inhabited α] : α :=
+  getKey?ₘ l k |>.get!
+
+/--
+Model implementation of the `getKeyD` function.
+Internal implementation detail of the tree map
+-/
+def getKeyDₘ [Ord α] (k : α) (l : Impl α β) (fallback : α) : α :=
+  getKey?ₘ l k |>.getD fallback
+
 /--
 Model implementation of the `insert` function.
 Internal implementation detail of the tree map
@@ -375,6 +403,45 @@ theorem getD_eq_getDₘ [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l :
     all_goals simp_all [Cell.get?, Cell.ofEq]
   · simp only [getD, applyCell, Cell.get?_empty, Option.getD_none]
 
+theorem getKey?_eq_getKey?ₘ [Ord α] (k : α) (l : Impl α β) :
+    l.getKey? k = l.getKey?ₘ k := by
+  simp only [getKey?ₘ]
+  induction l
+  · simp only [applyCell, getKey?]
+    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
+    all_goals simp_all [Cell.getKey?, Cell.ofEq]
+  · simp [getKey?, applyCell]
+
+theorem getKey_eq_getKey? [Ord α] (k : α) (l : Impl α β) {h} :
+    l.getKey k h = l.getKey? k := by
+  induction l
+  · simp only [applyCell, getKey, getKey?]
+    split <;> rename_i ihl ihr hcmp <;> simp_all
+  · contradiction
+
+theorem getKey_eq_getKeyₘ [Ord α] (k : α) (l : Impl α β) {h} (h') :
+    l.getKey k h = l.getKeyₘ k h' := by
+  apply Option.some.inj
+  simp [getKey_eq_getKey?, getKey?_eq_getKey?ₘ, getKeyₘ]
+
+theorem getKey!_eq_getKey!ₘ [Ord α] (k : α) [Inhabited α] (l : Impl α β) :
+    l.getKey! k = l.getKey!ₘ k := by
+  simp only [getKey!ₘ, getKey?ₘ]
+  induction l
+  · simp only [applyCell, getKey!]
+    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
+    all_goals simp_all [Cell.getKey?, Cell.ofEq]
+  · simp only [getKey!, applyCell, Cell.getKey?_empty, Option.get!_none]; rfl
+
+theorem getKeyD_eq_getKeyDₘ [Ord α] (k : α) (l : Impl α β)
+    (fallback : α) : l.getKeyD k fallback = l.getKeyDₘ k fallback := by
+  simp only [getKeyDₘ, getKey?ₘ]
+  induction l
+  · simp only [applyCell, getKeyD]
+    split <;> rename_i hcmp₁ <;> split <;> rename_i hcmp₂ <;> try (simp [hcmp₁] at hcmp₂; done)
+    all_goals simp_all [Cell.getKey?, Cell.ofEq]
+  · simp only [getKeyD, applyCell, Cell.getKey?_empty, Option.getD_none]
+
 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/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
index 7f1ca1c4a7..9bcd0370c1 100644
--- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
@@ -610,6 +610,71 @@ theorem getD_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
     t.getD k fallback = getValueCastD k t.toListModel fallback := by
   rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hto]
 
+/-!
+### `getKey?`
+-/
+
+theorem getKey?ₘ_eq_getKey? [Ord α] [TransOrd α] {k : α} {t : Impl α β}
+    (hto : t.Ordered) : t.getKey?ₘ k = List.getKey? k t.toListModel := by
+  rw [getKey?ₘ, applyCell_eq_apply_toListModel hto (fun l _ => List.getKey? k l)]
+  · rintro ⟨(_|p), hp⟩ -
+    · simp [Cell.getKey?]
+    · simp only [Cell.getKey?, Option.toList_some, List.getKey?, beq_eq,
+        compare_eq_iff_eq, Option.some_eq_dite_none_right, exists_prop, and_true]
+      simp [OrientedCmp.eq_symm (hp p rfl)]
+  · exact fun l₁ l₂ h => List.getKey?_of_perm
+  · exact fun l₁ l₂ h => List.getKey?_append_of_containsKey_eq_false
+
+theorem getKey?_eq_getKey? [Ord α] [TransOrd α] {k : α} {t : Impl α β}
+    (hto : t.Ordered) : t.getKey? k = List.getKey? k t.toListModel := by
+  rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hto]
+
+/-!
+### `getKey`
+-/
+
+theorem contains_eq_isSome_getKey?ₘ [Ord α] [TransOrd α] {k : α} {t : Impl α β}
+    (hto : t.Ordered) : contains k t = (t.getKey?ₘ k).isSome := by
+  rw [getKey?ₘ_eq_getKey? hto, contains_eq_containsKey hto, containsKey_eq_isSome_getKey?]
+
+theorem getKeyₘ_eq_getKey [Ord α] [TransOrd α] {k : α} {t : Impl α β} (h) {h'}
+    (hto : t.Ordered) : t.getKeyₘ k h' = List.getKey k t.toListModel h := by
+  simp only [getKeyₘ]
+  revert h'
+  rw [getKey?ₘ_eq_getKey? hto]
+  simp [getKey?_eq_some_getKey ‹_›]
+
+theorem getKey_eq_getKey [Ord α] [TransOrd α] {k : α} {t : Impl α β} {h}
+    (hto : t.Ordered): t.getKey k h = List.getKey k t.toListModel (contains_eq_containsKey hto ▸ h) := by
+  rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey _ hto]
+  exact contains_eq_isSome_getKey?ₘ hto ▸ h
+
+/-!
+### `getKey!`
+-/
+
+theorem getKey!ₘ_eq_getKey! [Ord α] [TransOrd α] {k : α} [Inhabited α]
+    {t : Impl α β} (hto : t.Ordered) : t.getKey!ₘ k = List.getKey! k t.toListModel := by
+  simp [getKey!ₘ, getKey?ₘ_eq_getKey? hto, getKey!_eq_getKey?]
+
+theorem getKey!_eq_getKey! [Ord α] [TransOrd α] {k : α} [Inhabited α]
+    {t : Impl α β} (hto : t.Ordered) : t.getKey! k = List.getKey! k t.toListModel := by
+  rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hto]
+
+/-!
+### `getKeyD`
+-/
+
+theorem getKeyDₘ_eq_getKeyD [Ord α] [TransOrd α] {k : α}
+    {t : Impl α β} {fallback : α} (hto : t.Ordered) :
+    t.getKeyDₘ k fallback = List.getKeyD k t.toListModel fallback := by
+  simp [getKeyDₘ, getKey?ₘ_eq_getKey? hto, getKeyD_eq_getKey?]
+
+theorem getKeyD_eq_getKeyD [Ord α] [TransOrd α] {k : α}
+    {t : Impl α β} {fallback : α} (hto : t.Ordered) :
+    t.getKeyD k fallback = List.getKeyD k t.toListModel fallback := by
+  rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hto]
+
 namespace Const
 
 variable {β : Type v}
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index d4d0a623a7..53e2d3b79e 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -48,11 +48,6 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
 theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
   Impl.mem_congr t.wf hab
 
-@[simp]
-theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
-    (t.insertIfNew k v).isEmpty = false :=
-  Impl.isEmpty_insertIfNew t.wf
-
 @[simp]
 theorem contains_emptyc {k : α} : (∅ : DTreeMap α β cmp).contains k = false :=
   Impl.contains_empty
@@ -200,44 +195,6 @@ theorem containsThenInsertIfNew_snd [TransCmp cmp] {k : α} {v : β k} :
     (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v :=
   ext <| Impl.containsThenInsertIfNew_snd t.wf
 
-@[simp]
-theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
-    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
-  Impl.contains_insertIfNew t.wf
-
-@[simp]
-theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
-    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
-  Impl.mem_insertIfNew t.wf
-
-theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} :
-    (t.insertIfNew k v).contains k :=
-  Impl.contains_insertIfNew_self t.wf
-
-theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} :
-    k ∈ t.insertIfNew k v :=
-  Impl.mem_insertIfNew_self t.wf
-
-theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
-    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
-  Impl.contains_of_contains_insertIfNew t.wf
-
-theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
-    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
-  Impl.contains_of_contains_insertIfNew t.wf
-
-theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
-    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
-  Impl.size_insertIfNew t.wf
-
-theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
-    t.size ≤ (t.insertIfNew k v).size :=
-  Impl.size_le_size_insertIfNew t.wf
-
-theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} :
-    (t.insertIfNew k v).size ≤ t.size + 1 :=
-  Impl.size_insertIfNew_le t.wf
-
 @[simp]
 theorem get?_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (∅ : DTreeMap α β cmp).get? a = none :=
@@ -640,4 +597,303 @@ theorem getD_congr [TransCmp cmp] {a b : α} {fallback : β} (hab : cmp a b = .e
 
 end Const
 
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : DTreeMap α β cmp).getKey? a = none :=
+  Impl.getKey?_empty
+
+theorem getKey?_of_isEmpty [TransCmp cmp] {a : α} :
+    t.isEmpty = true → t.getKey? a = none :=
+  Impl.getKey?_of_isEmpty t.wf
+
+theorem getKey?_insert [TransCmp cmp] {a k : α} {v : β k} :
+    (t.insert k v).getKey? a = if cmp k a = .eq then some k else t.getKey? a :=
+  Impl.getKey?_insert t.wf
+
+@[simp]
+theorem getKey?_insert_self [TransCmp cmp] {k : α} {v : β k} :
+    (t.insert k v).getKey? k = some k :=
+  Impl.getKey?_insert_self t.wf
+
+theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
+    t.contains a = (t.getKey? a).isSome :=
+  Impl.contains_eq_isSome_getKey? t.wf
+
+theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
+    a ∈ t ↔ (t.getKey? a).isSome :=
+  Impl.mem_iff_isSome_getKey? t.wf
+
+theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
+    t.contains a = false → t.getKey? a = none :=
+  Impl.getKey?_eq_none_of_contains_eq_false t.wf
+
+theorem getKey?_eq_none [TransCmp cmp] {a : α} :
+    ¬ a ∈ t → t.getKey? a = none :=
+  Impl.getKey?_eq_none t.wf
+
+theorem getKey?_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).getKey? a = if cmp k a = .eq then none else t.getKey? a :=
+  Impl.getKey?_erase t.wf
+
+@[simp]
+theorem getKey?_erase_self [TransCmp cmp] {k : α} :
+    (t.erase k).getKey? k = none :=
+  Impl.getKey?_erase_self t.wf
+
+theorem getKey_insert [TransCmp cmp] {k a : α} {v : β k} {h₁} :
+    (t.insert k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq then
+        k
+      else
+        t.getKey a (mem_of_mem_insert h₁ h₂) :=
+  Impl.getKey_insert t.wf
+
+@[simp]
+theorem getKey_insert_self [TransCmp cmp] {k : α} {v : β k} :
+    (t.insert k v).getKey k mem_insert_self = k :=
+  Impl.getKey_insert_self t.wf
+
+@[simp]
+theorem getKey_erase [TransCmp cmp] {k a : α} {h'} :
+    (t.erase k).getKey a h' = t.getKey a (mem_of_mem_erase h') :=
+  Impl.getKey_erase t.wf
+
+theorem getKey?_eq_some_getKey [TransCmp cmp] {a : α} {h'} :
+    t.getKey? a = some (t.getKey a h') :=
+  Impl.getKey?_eq_some_getKey t.wf
+
+@[simp]
+theorem getKey!_emptyc {a : α} [Inhabited α] :
+    (∅ : DTreeMap α β cmp).getKey! a = default :=
+  Impl.getKey!_empty
+
+theorem getKey!_of_isEmpty [TransCmp cmp] [Inhabited α] {a : α} :
+    t.isEmpty = true → t.getKey! a = default :=
+  Impl.getKey!_of_isEmpty t.wf
+
+theorem getKey!_insert [TransCmp cmp] [Inhabited α] {k a : α}
+    {v : β k} : (t.insert k v).getKey! a = if cmp k a = .eq then k else t.getKey! a :=
+  Impl.getKey!_insert t.wf
+
+@[simp]
+theorem getKey!_insert_self [TransCmp cmp] [Inhabited α] {a : α}
+    {b : β a} : (t.insert a b).getKey! a = a :=
+  Impl.getKey!_insert_self t.wf
+
+theorem getKey!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = false → t.getKey! a = default :=
+  Impl.getKey!_eq_default_of_contains_eq_false t.wf
+
+theorem getKey!_eq_default [TransCmp cmp] [Inhabited α] {a : α} :
+    ¬ a ∈ t → t.getKey! a = default :=
+  Impl.getKey!_eq_default t.wf
+
+theorem getKey!_erase [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.erase k).getKey! a = if cmp k a = .eq then default else t.getKey! a :=
+  Impl.getKey!_erase t.wf
+
+@[simp]
+theorem getKey!_erase_self [TransCmp cmp] [Inhabited α] {k : α} :
+    (t.erase k).getKey! k = default :=
+  Impl.getKey!_erase_self t.wf
+
+theorem getKey?_eq_some_getKey!_of_contains [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = true → t.getKey? a = some (t.getKey! a) :=
+  Impl.getKey?_eq_some_getKey!_of_contains t.wf
+
+theorem getKey?_eq_some_getKey! [TransCmp cmp] [Inhabited α] {a : α} :
+    a ∈ t → t.getKey? a = some (t.getKey! a) :=
+  Impl.getKey?_eq_some_getKey! t.wf
+
+theorem getKey!_eq_get!_getKey? [TransCmp cmp] [Inhabited α] {a : α} :
+    t.getKey! a = (t.getKey? a).get! :=
+  Impl.getKey!_eq_get!_getKey? t.wf
+
+theorem getKey_eq_getKey! [TransCmp cmp] [Inhabited α] {a : α} {h} :
+    t.getKey a h = t.getKey! a :=
+  Impl.getKey_eq_getKey! t.wf
+
+@[simp]
+theorem getKeyD_emptyc {a : α} {fallback : α} :
+    (∅ : DTreeMap α β cmp).getKeyD a fallback = fallback :=
+  Impl.getKeyD_empty
+
+theorem getKeyD_of_isEmpty [TransCmp cmp] {a fallback : α} :
+    t.isEmpty = true → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_of_isEmpty t.wf
+
+theorem getKeyD_insert [TransCmp cmp] {k a fallback : α} {v : β k} :
+    (t.insert k v).getKeyD a fallback =
+      if cmp k a = .eq then k else t.getKeyD a fallback :=
+  Impl.getKeyD_insert t.wf
+
+@[simp]
+theorem getKeyD_insert_self [TransCmp cmp] {a fallback : α} {b : β a} :
+    (t.insert a b).getKeyD a fallback = a :=
+  Impl.getKeyD_insert_self t.wf
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a fallback : α} :
+    t.contains a = false → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_eq_fallback_of_contains_eq_false t.wf
+
+theorem getKeyD_eq_fallback [TransCmp cmp] {a fallback : α} :
+    ¬ a ∈ t → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_eq_fallback t.wf
+
+theorem getKeyD_erase [TransCmp cmp] {k a fallback : α} :
+    (t.erase k).getKeyD a fallback =
+      if cmp k a = .eq then fallback else t.getKeyD a fallback :=
+  Impl.getKeyD_erase t.wf
+
+@[simp]
+theorem getKeyD_erase_self [TransCmp cmp] {k fallback : α} :
+    (t.erase k).getKeyD k fallback = fallback :=
+  Impl.getKeyD_erase_self t.wf
+
+theorem getKey?_eq_some_getKeyD_of_contains [TransCmp cmp] {a fallback : α} :
+    t.contains a = true → t.getKey? a = some (t.getKeyD a fallback) :=
+  Impl.getKey?_eq_some_getKeyD_of_contains t.wf
+
+theorem getKey?_eq_some_getKeyD [TransCmp cmp] {a fallback : α} :
+  a ∈ t → t.getKey? a = some (t.getKeyD a fallback) :=
+  Impl.getKey?_eq_some_getKeyD t.wf
+
+theorem getKeyD_eq_getD_getKey? [TransCmp cmp] {a fallback : α} :
+    t.getKeyD a fallback = (t.getKey? a).getD fallback :=
+  Impl.getKeyD_eq_getD_getKey? t.wf
+
+theorem getKey_eq_getKeyD [TransCmp cmp] {a fallback : α} {h} :
+    t.getKey a h = t.getKeyD a fallback :=
+  Impl.getKey_eq_getKeyD t.wf
+
+theorem getKey!_eq_getKeyD_default [TransCmp cmp] [Inhabited α] {a : α} :
+    t.getKey! a = t.getKeyD a default :=
+  Impl.getKey!_eq_getKeyD_default t.wf
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).isEmpty = false :=
+  Impl.isEmpty_insertIfNew t.wf
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
+    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
+  Impl.contains_insertIfNew t.wf
+
+@[simp]
+theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
+  Impl.mem_insertIfNew t.wf
+
+theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).contains k :=
+  Impl.contains_insertIfNew_self t.wf
+
+theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β k} :
+    k ∈ t.insertIfNew k v :=
+  Impl.mem_insertIfNew_self t.wf
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
+    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
+  Impl.contains_of_contains_insertIfNew t.wf
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
+  Impl.contains_of_contains_insertIfNew t.wf
+
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} :
+    a ∈ (t.insertIfNew k v) → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  Impl.mem_of_mem_insertIfNew' t.wf
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
+  Impl.size_insertIfNew t.wf
+
+theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
+    t.size ≤ (t.insertIfNew k v).size :=
+  Impl.size_le_size_insertIfNew t.wf
+
+theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).size ≤ t.size + 1 :=
+  Impl.size_insertIfNew_le t.wf
+
+theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} :
+    (t.insertIfNew k v).get? a =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+      else
+        t.get? a :=
+  Impl.get?_insertIfNew t.wf
+
+theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v).get a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+      else
+        t.get a (mem_of_mem_insertIfNew' h₁ h₂) :=
+  Impl.get_insertIfNew t.wf
+
+theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
+    (t.insertIfNew k v).get! a =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.get! a :=
+  Impl.get!_insertIfNew t.wf
+
+theorem getD_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
+    (t.insertIfNew k v).getD a fallback =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.getD a fallback :=
+  Impl.getD_insertIfNew t.wf
+
+namespace Const
+
+variable {β : Type v} {t : DTreeMap α β cmp}
+
+theorem get?_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    get? (t.insertIfNew k v) a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some v else get? t a :=
+  Impl.Const.get?_insertIfNew t.wf
+
+theorem get_insertIfNew [TransCmp cmp] {k a : α} {v : β} {h₁} :
+    get (t.insertIfNew k v) a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then v else get t a (mem_of_mem_insertIfNew' h₁ h₂) :=
+  Impl.Const.get_insertIfNew t.wf
+
+theorem get!_insertIfNew [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
+    get! (t.insertIfNew k v) a = if cmp k a = .eq ∧ ¬ k ∈ t then v else get! t a :=
+  Impl.Const.get!_insertIfNew t.wf
+
+theorem getD_insertIfNew [TransCmp cmp] {k a : α} {fallback v : β} :
+    getD (t.insertIfNew k v) a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback :=
+  Impl.Const.getD_insertIfNew t.wf
+
+end Const
+
+theorem getKey?_insertIfNew [TransCmp cmp] {k a : α} {v : β k} :
+    (t.insertIfNew k v).getKey? a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a :=
+  Impl.getKey?_insertIfNew t.wf
+
+theorem getKey_insertIfNew [TransCmp cmp] {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew' h₁ h₂) :=
+  Impl.getKey_insertIfNew t.wf
+
+theorem getKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k a : α} {v : β k} :
+    (t.insertIfNew k v).getKey! a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a :=
+  Impl.getKey!_insertIfNew t.wf
+
+theorem getKeyD_insertIfNew [TransCmp cmp] {k a fallback : α} {v : β k} :
+    (t.insertIfNew k v).getKeyD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback :=
+  Impl.getKeyD_insertIfNew t.wf
+
 end Std.DTreeMap
diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean
index 6529b35f2b..9f67aeb022 100644
--- a/src/Std/Data/DTreeMap/RawLemmas.lean
+++ b/src/Std/Data/DTreeMap/RawLemmas.lean
@@ -48,11 +48,6 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .
 theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
   Impl.mem_congr h hab
 
-@[simp]
-theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    (t.insertIfNew k v).isEmpty = false :=
-  Impl.isEmpty_insertIfNew! h
-
 @[simp]
 theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false :=
   Impl.contains_empty
@@ -200,44 +195,6 @@ theorem containsThenInsertIfNew_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β k
     (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v :=
   ext <| Impl.containsThenInsertIfNew!_snd h
 
-@[simp]
-theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
-    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
-  Impl.contains_insertIfNew! h
-
-@[simp]
-theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
-    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
-  Impl.mem_insertIfNew! h
-
-theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    (t.insertIfNew k v).contains k :=
-  Impl.contains_insertIfNew!_self h
-
-theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    k ∈ t.insertIfNew k v :=
-  Impl.mem_insertIfNew!_self h
-
-theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
-    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
-  Impl.contains_of_contains_insertIfNew! h
-
-theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
-    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
-  Impl.contains_of_contains_insertIfNew! h
-
-theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β k} :
-    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
-  Impl.size_insertIfNew! h
-
-theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    t.size ≤ (t.insertIfNew k v).size :=
-  Impl.size_le_size_insertIfNew! h
-
-theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
-    (t.insertIfNew k v).size ≤ t.size + 1 :=
-  Impl.size_insertIfNew!_le h
-
 @[simp]
 theorem get?_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (∅ : DTreeMap α β cmp).get? a = none :=
@@ -642,4 +599,308 @@ theorem getD_congr [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β} (hab : c
 
 end Const
 
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : DTreeMap α β cmp).getKey? a = none :=
+  Impl.getKey?_empty
+
+theorem getKey?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey? a = none :=
+  Impl.getKey?_of_isEmpty h
+
+theorem getKey?_insert [TransCmp cmp] (h : t.WF) {a k : α} {v : β k} :
+    (t.insert k v).getKey? a = if cmp k a = .eq then some k else t.getKey? a :=
+  Impl.getKey?_insert! h
+
+@[simp]
+theorem getKey?_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v).getKey? k = some k :=
+  Impl.getKey?_insert!_self h
+
+theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = (t.getKey? a).isSome :=
+  Impl.contains_eq_isSome_getKey? h
+
+theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
+    a ∈ t ↔ (t.getKey? a).isSome :=
+  Impl.mem_iff_isSome_getKey? h
+
+theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey? a = none :=
+  Impl.getKey?_eq_none_of_contains_eq_false h
+
+theorem getKey?_eq_none [TransCmp cmp] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey? a = none :=
+  Impl.getKey?_eq_none h
+
+theorem getKey?_erase [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.erase k).getKey? a = if cmp k a = .eq then none else t.getKey? a :=
+  Impl.getKey?_erase! h
+
+@[simp]
+theorem getKey?_erase_self [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.erase k).getKey? k = none :=
+  Impl.getKey?_erase!_self h
+
+theorem getKey_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insert k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq then
+        k
+      else
+        t.getKey a (mem_of_mem_insert h h₁ h₂) :=
+  Impl.getKey_insert! h
+
+@[simp]
+theorem getKey_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v).getKey k (mem_insert_self h) = k :=
+  Impl.getKey_insert!_self h
+
+@[simp]
+theorem getKey_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
+    (t.erase k).getKey a h' = t.getKey a (mem_of_mem_erase h h') :=
+  Impl.getKey_erase! h
+
+theorem getKey?_eq_some_getKey [TransCmp cmp] (h : t.WF) {a : α} {h'} :
+    t.getKey? a = some (t.getKey a h') :=
+  Impl.getKey?_eq_some_getKey h
+
+@[simp]
+theorem getKey!_emptyc {a : α} [Inhabited α] :
+    (∅ : DTreeMap α β cmp).getKey! a = default :=
+  Impl.getKey!_empty
+
+theorem getKey!_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey! a = default :=
+  Impl.getKey!_of_isEmpty h
+
+theorem getKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insert k v).getKey! a = if cmp k a = .eq then k else t.getKey! a :=
+  Impl.getKey!_insert! h
+
+@[simp]
+theorem getKey!_insert_self [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {b : β a} :
+    (t.insert a b).getKey! a = a :=
+  Impl.getKey!_insert!_self h
+
+theorem getKey!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey! a = default :=
+  Impl.getKey!_eq_default_of_contains_eq_false h
+
+theorem getKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey! a = default :=
+  Impl.getKey!_eq_default h
+
+theorem getKey!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.erase k).getKey! a = if cmp k a = .eq then default else t.getKey! a :=
+  Impl.getKey!_erase! h
+
+@[simp]
+theorem getKey!_erase_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
+    (t.erase k).getKey! k = default :=
+  Impl.getKey!_erase!_self h
+
+theorem getKey?_eq_some_getKey!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = true → t.getKey? a = some (t.getKey! a) :=
+  Impl.getKey?_eq_some_getKey!_of_contains h
+
+theorem getKey?_eq_some_getKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    a ∈ t → t.getKey? a = some (t.getKey! a) :=
+  Impl.getKey?_eq_some_getKey! h
+
+theorem getKey!_eq_get!_getKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.getKey! a = (t.getKey? a).get! :=
+  Impl.getKey!_eq_get!_getKey? h
+
+theorem getKey_eq_getKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {h'} :
+    t.getKey a h' = t.getKey! a :=
+  Impl.getKey_eq_getKey! h
+
+@[simp]
+theorem getKeyD_emptyc {a : α} {fallback : α} :
+    (∅ : DTreeMap α β cmp).getKeyD a fallback = fallback :=
+  Impl.getKeyD_empty
+
+theorem getKeyD_of_isEmpty [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.isEmpty = true → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_of_isEmpty h
+
+theorem getKeyD_insert [TransCmp cmp] (h : t.WF) {k a fallback : α} {v : β k} :
+    (t.insert k v).getKeyD a fallback = if cmp k a = .eq then k else t.getKeyD a fallback :=
+  Impl.getKeyD_insert! h
+
+@[simp]
+theorem getKeyD_insert_self [TransCmp cmp] (h : t.WF) {a fallback : α} {b : β a} :
+    (t.insert a b).getKeyD a fallback = a :=
+  Impl.getKeyD_insert!_self h
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = false → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_eq_fallback_of_contains_eq_false h
+
+theorem getKeyD_eq_fallback [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    ¬ a ∈ t → t.getKeyD a fallback = fallback :=
+  Impl.getKeyD_eq_fallback h
+
+theorem getKeyD_erase [TransCmp cmp] (h : t.WF) {k a fallback : α} :
+    (t.erase k).getKeyD a fallback =
+      if cmp k a = .eq then fallback else t.getKeyD a fallback :=
+  Impl.getKeyD_erase! h
+
+@[simp]
+theorem getKeyD_erase_self [TransCmp cmp] (h : t.WF) {k fallback : α} :
+    (t.erase k).getKeyD k fallback = fallback :=
+  Impl.getKeyD_erase!_self h
+
+theorem getKey?_eq_some_getKeyD_of_contains [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = true → t.getKey? a = some (t.getKeyD a fallback) :=
+  Impl.getKey?_eq_some_getKeyD_of_contains h
+
+theorem getKey?_eq_some_getKeyD [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    a ∈ t → t.getKey? a = some (t.getKeyD a fallback) :=
+  Impl.getKey?_eq_some_getKeyD h
+
+theorem getKeyD_eq_getD_getKey? [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.getKeyD a fallback = (t.getKey? a).getD fallback :=
+  Impl.getKeyD_eq_getD_getKey? h
+
+theorem getKey_eq_getKeyD [TransCmp cmp] (h : t.WF) {a fallback : α} {h'} :
+    t.getKey a h' = t.getKeyD a fallback :=
+  Impl.getKey_eq_getKeyD h
+
+theorem getKey!_eq_getKeyD_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.getKey! a = t.getKeyD a default :=
+  Impl.getKey!_eq_getKeyD_default h
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).isEmpty = false :=
+  Impl.isEmpty_insertIfNew! h
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
+  Impl.contains_insertIfNew! h
+
+@[simp]
+theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
+  Impl.mem_insertIfNew! h
+
+theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).contains k :=
+  Impl.contains_insertIfNew!_self h
+
+theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    k ∈ t.insertIfNew k v :=
+  Impl.mem_insertIfNew!_self h
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
+  Impl.contains_of_contains_insertIfNew! h
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
+  Impl.contains_of_contains_insertIfNew! h
+
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  Impl.mem_of_mem_insertIfNew!' h
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β k} :
+    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
+  Impl.size_insertIfNew! h
+
+theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insertIfNew k v).size :=
+  Impl.size_le_size_insertIfNew! h
+
+theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).size ≤ t.size + 1 :=
+  Impl.size_insertIfNew!_le h
+
+theorem get?_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v).get? a =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v)
+      else
+        t.get? a :=
+  Impl.get?_insertIfNew! h
+
+theorem get_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v).get a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v
+      else
+        t.get a (mem_of_mem_insertIfNew' h h₁ h₂) :=
+  Impl.get_insertIfNew! h
+
+theorem get!_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
+    (t.insertIfNew k v).get! a =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.get! a :=
+  Impl.get!_insertIfNew! h
+
+theorem getD_insertIfNew [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
+    (t.insertIfNew k v).getD a fallback =
+      if h : cmp k a = .eq ∧ ¬ k ∈ t then
+        cast (congrArg β (compare_eq_iff_eq.mp h.1)) v
+      else
+        t.getD a fallback :=
+  Impl.getD_insertIfNew! h
+
+namespace Const
+
+variable {β : Type v} {t : Raw α β cmp}
+
+theorem get?_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    get? (t.insertIfNew k v) a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some v else get? t a :=
+  Impl.Const.get?_insertIfNew! h
+
+theorem get_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
+    get (t.insertIfNew k v) a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
+        v
+      else
+        get t a (mem_of_mem_insertIfNew' h h₁ h₂) :=
+  Impl.Const.get_insertIfNew! h
+
+theorem get!_insertIfNew [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
+    get! (t.insertIfNew k v) a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then v else get! t a :=
+  Impl.Const.get!_insertIfNew! h
+
+theorem getD_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} :
+    getD (t.insertIfNew k v) a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback :=
+  Impl.Const.getD_insertIfNew! h
+
+end Const
+
+theorem getKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v).getKey? a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a :=
+  Impl.getKey?_insertIfNew! h
+
+theorem getKey_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
+    (t.insertIfNew k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) :=
+  Impl.getKey_insertIfNew! h
+
+theorem getKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β k} :
+    (t.insertIfNew k v).getKey! a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a :=
+  Impl.getKey!_insertIfNew! h
+
+theorem getKeyD_insertIfNew [TransCmp cmp] (h : t.WF) {k a fallback : α}
+    {v : β k} :
+    (t.insertIfNew k v).getKeyD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback :=
+  Impl.getKeyD_insertIfNew! h
+
 end Std.DTreeMap.Raw
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index 02fd360597..8d7a40077d 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -45,11 +45,6 @@ theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
 theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
   DTreeMap.mem_congr hab
 
-@[simp]
-theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} :
-    (t.insertIfNew k v).isEmpty = false :=
-  DTreeMap.isEmpty_insertIfNew
-
 @[simp]
 theorem contains_emptyc {k : α} : (∅ : TreeMap α β cmp).contains k = false :=
   DTreeMap.contains_emptyc
@@ -197,46 +192,6 @@ theorem containsThenInsertIfNew_snd [TransCmp cmp] {k : α} {v : β} :
     (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v :=
   ext <| DTreeMap.containsThenInsertIfNew_snd
 
-@[simp]
-theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
-    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
-  DTreeMap.contains_insertIfNew
-
-@[simp]
-theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
-    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
-  DTreeMap.mem_insertIfNew
-
-@[simp]
-theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} :
-    (t.insertIfNew k v).contains k :=
-  DTreeMap.contains_insertIfNew_self
-
-@[simp]
-theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β} :
-    k ∈ t.insertIfNew k v :=
-  DTreeMap.mem_insertIfNew_self
-
-theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
-    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
-  DTreeMap.contains_of_contains_insertIfNew
-
-theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
-    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
-  DTreeMap.contains_of_contains_insertIfNew
-
-theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β} :
-    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
-  DTreeMap.size_insertIfNew
-
-theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β} :
-    t.size ≤ (t.insertIfNew k v).size :=
-  DTreeMap.size_le_size_insertIfNew
-
-theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} :
-    (t.insertIfNew k v).size ≤ t.size + 1 :=
-  DTreeMap.size_insertIfNew_le
-
 @[simp] theorem get_eq_getElem {a : α} {h} : get t a h = t[a]'h := rfl
 @[simp] theorem get?_eq_getElem? {a : α} : get? t a = t[a]? := rfl
 @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! t a = t[a]! := rfl
@@ -429,4 +384,265 @@ theorem getD_congr [TransCmp cmp] {a b : α} {fallback : β}
     (hab : cmp a b = .eq) : getD t a fallback = getD t b fallback :=
   DTreeMap.Const.getD_congr hab
 
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : TreeMap α β cmp).getKey? a = none :=
+  DTreeMap.getKey?_emptyc
+
+theorem getKey?_of_isEmpty [TransCmp cmp] {a : α} :
+    t.isEmpty = true → t.getKey? a = none :=
+  DTreeMap.getKey?_of_isEmpty
+
+theorem getKey?_insert [TransCmp cmp] {a k : α} {v : β} :
+    (t.insert k v).getKey? a = if cmp k a = .eq then some k else t.getKey? a :=
+  DTreeMap.getKey?_insert
+
+@[simp]
+theorem getKey?_insert_self [TransCmp cmp] {k : α} {v : β} :
+    (t.insert k v).getKey? k = some k :=
+  DTreeMap.getKey?_insert_self
+
+theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
+    t.contains a = (t.getKey? a).isSome :=
+  DTreeMap.contains_eq_isSome_getKey?
+
+theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
+    a ∈ t ↔ (t.getKey? a).isSome :=
+  DTreeMap.mem_iff_isSome_getKey?
+
+theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
+    t.contains a = false → t.getKey? a = none :=
+  DTreeMap.getKey?_eq_none_of_contains_eq_false
+
+theorem getKey?_eq_none [TransCmp cmp] {a : α} :
+    ¬ a ∈ t → t.getKey? a = none :=
+  DTreeMap.getKey?_eq_none
+
+theorem getKey?_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).getKey? a = if cmp k a = .eq then none else t.getKey? a :=
+  DTreeMap.getKey?_erase
+
+@[simp]
+theorem getKey?_erase_self [TransCmp cmp] {k : α} :
+    (t.erase k).getKey? k = none :=
+  DTreeMap.getKey?_erase_self
+
+theorem getKey_insert [TransCmp cmp] {k a : α} {v : β} {h₁} :
+    (t.insert k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq then k else t.getKey a (mem_of_mem_insert h₁ h₂) :=
+  DTreeMap.getKey_insert
+
+@[simp]
+theorem getKey_insert_self [TransCmp cmp] {k : α} {v : β} :
+    (t.insert k v).getKey k mem_insert_self = k :=
+  DTreeMap.getKey_insert_self
+
+@[simp]
+theorem getKey_erase [TransCmp cmp] {k a : α} {h'} :
+    (t.erase k).getKey a h' = t.getKey a (mem_of_mem_erase h') :=
+  DTreeMap.getKey_erase
+
+theorem getKey?_eq_some_getKey [TransCmp cmp] {a : α} {h'} :
+    t.getKey? a = some (t.getKey a h') :=
+  DTreeMap.getKey?_eq_some_getKey
+
+@[simp]
+theorem getKey!_emptyc {a : α} [Inhabited α] :
+    (∅ : TreeMap α β cmp).getKey! a = default :=
+  DTreeMap.getKey!_emptyc
+
+theorem getKey!_of_isEmpty [TransCmp cmp] [Inhabited α] {a : α} :
+    t.isEmpty = true → t.getKey! a = default :=
+  DTreeMap.getKey!_of_isEmpty
+
+theorem getKey!_insert [TransCmp cmp] [Inhabited α] {k a : α}
+    {v : β} : (t.insert k v).getKey! a = if cmp k a = .eq then k else t.getKey! a :=
+  DTreeMap.getKey!_insert
+
+@[simp]
+theorem getKey!_insert_self [TransCmp cmp] [Inhabited α] {a : α}
+    {b : β} : (t.insert a b).getKey! a = a :=
+  DTreeMap.getKey!_insert_self
+
+theorem getKey!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = false → t.getKey! a = default :=
+  DTreeMap.getKey!_eq_default_of_contains_eq_false
+
+theorem getKey!_eq_default [TransCmp cmp] [Inhabited α] {a : α} :
+    ¬ a ∈ t → t.getKey! a = default :=
+  DTreeMap.getKey!_eq_default
+
+theorem getKey!_erase [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.erase k).getKey! a = if cmp k a = .eq then default else t.getKey! a :=
+  DTreeMap.getKey!_erase
+
+@[simp]
+theorem getKey!_erase_self [TransCmp cmp] [Inhabited α] {k : α} :
+    (t.erase k).getKey! k = default :=
+  DTreeMap.getKey!_erase_self
+
+theorem getKey?_eq_some_getKey!_of_contains [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = true → t.getKey? a = some (t.getKey! a) :=
+  DTreeMap.getKey?_eq_some_getKey!_of_contains
+
+theorem getKey?_eq_some_getKey! [TransCmp cmp] [Inhabited α] {a : α} :
+    a ∈ t → t.getKey? a = some (t.getKey! a) :=
+  DTreeMap.getKey?_eq_some_getKey!
+
+theorem getKey!_eq_get!_getKey? [TransCmp cmp] [Inhabited α] {a : α} :
+    t.getKey! a = (t.getKey? a).get! :=
+  DTreeMap.getKey!_eq_get!_getKey?
+
+theorem getKey_eq_getKey! [TransCmp cmp] [Inhabited α] {a : α} {h} :
+    t.getKey a h = t.getKey! a :=
+  DTreeMap.getKey_eq_getKey!
+
+@[simp]
+theorem getKeyD_emptyc {a : α} {fallback : α} :
+    (∅ : TreeMap α β cmp).getKeyD a fallback = fallback :=
+  DTreeMap.getKeyD_emptyc
+
+theorem getKeyD_of_isEmpty [TransCmp cmp] {a fallback : α} :
+    t.isEmpty = true → t.getKeyD a fallback = fallback :=
+  DTreeMap.getKeyD_of_isEmpty
+
+theorem getKeyD_insert [TransCmp cmp] {k a fallback : α} {v : β} :
+    (t.insert k v).getKeyD a fallback = if cmp k a = .eq then k else t.getKeyD a fallback :=
+  DTreeMap.getKeyD_insert
+
+@[simp]
+theorem getKeyD_insert_self [TransCmp cmp] {a fallback : α} {b : β} :
+    (t.insert a b).getKeyD a fallback = a :=
+  DTreeMap.getKeyD_insert_self
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a fallback : α} :
+    t.contains a = false → t.getKeyD a fallback = fallback :=
+  DTreeMap.getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getKeyD_eq_fallback [TransCmp cmp] {a fallback : α} :
+    ¬ a ∈ t → t.getKeyD a fallback = fallback :=
+  DTreeMap.getKeyD_eq_fallback
+
+theorem getKeyD_erase [TransCmp cmp] {k a fallback : α} :
+    (t.erase k).getKeyD a fallback =
+      if cmp k a = .eq then fallback else t.getKeyD a fallback :=
+  DTreeMap.getKeyD_erase
+
+@[simp]
+theorem getKeyD_erase_self [TransCmp cmp] {k fallback : α} :
+    (t.erase k).getKeyD k fallback = fallback :=
+  DTreeMap.getKeyD_erase_self
+
+theorem getKey?_eq_some_getKeyD_of_contains [TransCmp cmp] {a fallback : α} :
+    t.contains a = true → t.getKey? a = some (t.getKeyD a fallback) :=
+  DTreeMap.getKey?_eq_some_getKeyD_of_contains
+
+theorem getKey?_eq_some_getKeyD [TransCmp cmp] {a fallback : α} :
+  a ∈ t → t.getKey? a = some (t.getKeyD a fallback) :=
+  DTreeMap.getKey?_eq_some_getKeyD
+
+theorem getKeyD_eq_getD_getKey? [TransCmp cmp] {a fallback : α} :
+    t.getKeyD a fallback = (t.getKey? a).getD fallback :=
+  DTreeMap.getKeyD_eq_getD_getKey?
+
+theorem getKey_eq_getKeyD [TransCmp cmp] {a fallback : α} {h} :
+    t.getKey a h = t.getKeyD a fallback :=
+  DTreeMap.getKey_eq_getKeyD
+
+theorem getKey!_eq_getKeyD_default [TransCmp cmp] [Inhabited α] {a : α} :
+    t.getKey! a = t.getKeyD a default :=
+  DTreeMap.getKey!_eq_getKeyD_default
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).isEmpty = false :=
+  DTreeMap.isEmpty_insertIfNew
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
+  DTreeMap.contains_insertIfNew
+
+@[simp]
+theorem mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
+  DTreeMap.mem_insertIfNew
+
+@[simp]
+theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).contains k :=
+  DTreeMap.contains_insertIfNew_self
+
+@[simp]
+theorem mem_insertIfNew_self [TransCmp cmp] {k : α} {v : β} :
+    k ∈ t.insertIfNew k v :=
+  DTreeMap.mem_insertIfNew_self
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
+  DTreeMap.contains_of_contains_insertIfNew
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
+  DTreeMap.contains_of_contains_insertIfNew
+
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insertIfNew' [TransCmp cmp] {k a : α} {v : β} :
+    a ∈ (t.insertIfNew k v) → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  DTreeMap.mem_of_mem_insertIfNew'
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
+  DTreeMap.size_insertIfNew
+
+theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} {v : β} :
+    t.size ≤ (t.insertIfNew k v).size :=
+  DTreeMap.size_le_size_insertIfNew
+
+theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).size ≤ t.size + 1 :=
+  DTreeMap.size_insertIfNew_le
+
+theorem getElem?_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    (t.insertIfNew k v)[a]? =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some v else t[a]? :=
+  DTreeMap.Const.get?_insertIfNew
+
+theorem getElem_insertIfNew [TransCmp cmp] {k a : α} {v : β} {h₁} :
+    (t.insertIfNew k v)[a]'h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then v else t[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
+  DTreeMap.Const.get_insertIfNew
+
+theorem getElem!_insertIfNew [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
+    (t.insertIfNew k v)[a]! = if cmp k a = .eq ∧ ¬ k ∈ t then v else t[a]! :=
+  DTreeMap.Const.get!_insertIfNew
+
+theorem getD_insertIfNew [TransCmp cmp] {k a : α} {fallback v : β} :
+    getD (t.insertIfNew k v) a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback :=
+  DTreeMap.Const.getD_insertIfNew
+
+theorem getKey?_insertIfNew [TransCmp cmp] {k a : α} {v : β} :
+    (t.insertIfNew k v).getKey? a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a :=
+  DTreeMap.getKey?_insertIfNew
+
+theorem getKey_insertIfNew [TransCmp cmp] {k a : α} {v : β} {h₁} :
+    (t.insertIfNew k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew' h₁ h₂) :=
+  DTreeMap.getKey_insertIfNew
+
+theorem getKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k a : α}
+    {v : β} :
+    (t.insertIfNew k v).getKey! a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a :=
+  DTreeMap.getKey!_insertIfNew
+
+theorem getKeyD_insertIfNew [TransCmp cmp] {k a fallback : α}
+    {v : β} :
+    (t.insertIfNew k v).getKeyD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback :=
+  DTreeMap.getKeyD_insertIfNew
+
 end Std.TreeMap
diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean
index f5c2a5d32c..b8951eb19c 100644
--- a/src/Std/Data/TreeMap/RawLemmas.lean
+++ b/src/Std/Data/TreeMap/RawLemmas.lean
@@ -45,11 +45,6 @@ theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .
 theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
   DTreeMap.Raw.mem_congr h hab
 
-@[simp]
-theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    (t.insertIfNew k v).isEmpty = false :=
-  DTreeMap.Raw.isEmpty_insertIfNew h
-
 @[simp]
 theorem contains_emptyc {k : α} : (∅ : Raw α β cmp).contains k = false :=
   DTreeMap.Raw.contains_emptyc
@@ -197,44 +192,6 @@ theorem containsThenInsertIfNew_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β}
     (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v :=
   ext <| DTreeMap.Raw.containsThenInsertIfNew_snd h
 
-@[simp]
-theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
-    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
-  DTreeMap.Raw.contains_insertIfNew h
-
-@[simp]
-theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
-    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
-  DTreeMap.Raw.mem_insertIfNew h
-
-theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    (t.insertIfNew k v).contains k :=
-  DTreeMap.Raw.contains_insertIfNew_self h
-
-theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    k ∈ t.insertIfNew k v :=
-  DTreeMap.Raw.mem_insertIfNew_self h
-
-theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
-    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
-  DTreeMap.Raw.contains_of_contains_insertIfNew h
-
-theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
-    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
-  DTreeMap.Raw.contains_of_contains_insertIfNew h
-
-theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β} :
-    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
-  DTreeMap.Raw.size_insertIfNew h
-
-theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    t.size ≤ (t.insertIfNew k v).size :=
-  DTreeMap.Raw.size_le_size_insertIfNew h
-
-theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    (t.insertIfNew k v).size ≤ t.size + 1 :=
-  DTreeMap.Raw.size_insertIfNew_le h
-
 @[simp] theorem get_eq_getElem {a : α} {h} : get t a h = t[a]'h := rfl
 @[simp] theorem get?_eq_getElem? {a : α} : get? t a = t[a]? := rfl
 @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! t a = t[a]! := rfl
@@ -427,4 +384,271 @@ theorem getD_congr [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β}
     (hab : cmp a b = .eq) : getD t a fallback = getD t b fallback :=
   DTreeMap.Raw.Const.getD_congr h hab
 
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : Raw α β cmp).getKey? a = none :=
+  DTreeMap.Raw.getKey?_emptyc
+
+theorem getKey?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey? a = none :=
+  DTreeMap.Raw.getKey?_of_isEmpty h
+
+theorem getKey?_insert [TransCmp cmp] (h : t.WF) {a k : α} {v : β} :
+    (t.insert k v).getKey? a = if cmp k a = .eq then some k else t.getKey? a :=
+  DTreeMap.Raw.getKey?_insert h
+
+@[simp]
+theorem getKey?_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).getKey? k = some k :=
+  DTreeMap.Raw.getKey?_insert_self h
+
+theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = (t.getKey? a).isSome :=
+  DTreeMap.Raw.contains_eq_isSome_getKey? h
+
+theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
+    a ∈ t ↔ (t.getKey? a).isSome :=
+  DTreeMap.Raw.mem_iff_isSome_getKey? h
+
+theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey? a = none :=
+  DTreeMap.Raw.getKey?_eq_none_of_contains_eq_false h
+
+theorem getKey?_eq_none [TransCmp cmp] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey? a = none :=
+  DTreeMap.Raw.getKey?_eq_none h
+
+theorem getKey?_erase [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.erase k).getKey? a = if cmp k a = .eq then none else t.getKey? a :=
+  DTreeMap.Raw.getKey?_erase h
+
+@[simp]
+theorem getKey?_erase_self [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.erase k).getKey? k = none :=
+  DTreeMap.Raw.getKey?_erase_self h
+
+theorem getKey_insert [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
+    (t.insert k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq then k else t.getKey a (mem_of_mem_insert h h₁ h₂) :=
+  DTreeMap.Raw.getKey_insert h
+
+@[simp]
+theorem getKey_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).getKey k (mem_insert_self h) = k :=
+  DTreeMap.Raw.getKey_insert_self h
+
+@[simp]
+theorem getKey_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
+    (t.erase k).getKey a h' = t.getKey a (mem_of_mem_erase h h') :=
+  DTreeMap.Raw.getKey_erase h
+
+theorem getKey?_eq_some_getKey [TransCmp cmp] (h : t.WF) {a : α} {h'} :
+    t.getKey? a = some (t.getKey a h') :=
+  DTreeMap.Raw.getKey?_eq_some_getKey h
+
+@[simp]
+theorem getKey!_emptyc {a : α} [Inhabited α] :
+    (∅ : Raw α β cmp).getKey! a = default :=
+  DTreeMap.Raw.getKey!_emptyc
+
+theorem getKey!_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.getKey! a = default :=
+  DTreeMap.Raw.getKey!_of_isEmpty h
+
+theorem getKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β} : (t.insert k v).getKey! a = if cmp k a = .eq then k else t.getKey! a :=
+  DTreeMap.Raw.getKey!_insert h
+
+@[simp]
+theorem getKey!_insert_self [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α}
+    {b : β} : (t.insert a b).getKey! a = a :=
+  DTreeMap.Raw.getKey!_insert_self h
+
+theorem getKey!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = false → t.getKey! a = default :=
+  DTreeMap.Raw.getKey!_eq_default_of_contains_eq_false h
+
+theorem getKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.getKey! a = default :=
+  DTreeMap.Raw.getKey!_eq_default h
+
+theorem getKey!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.erase k).getKey! a = if cmp k a = .eq then default else t.getKey! a :=
+  DTreeMap.Raw.getKey!_erase h
+
+@[simp]
+theorem getKey!_erase_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
+    (t.erase k).getKey! k = default :=
+  DTreeMap.Raw.getKey!_erase_self h
+
+theorem getKey?_eq_some_getKey!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = true → t.getKey? a = some (t.getKey! a) :=
+  DTreeMap.Raw.getKey?_eq_some_getKey!_of_contains h
+
+theorem getKey?_eq_some_getKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    a ∈ t → t.getKey? a = some (t.getKey! a) :=
+  DTreeMap.Raw.getKey?_eq_some_getKey! h
+
+theorem getKey!_eq_get!_getKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.getKey! a = (t.getKey? a).get! :=
+  DTreeMap.Raw.getKey!_eq_get!_getKey? h
+
+theorem getKey_eq_getKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {h'} :
+    t.getKey a h' = t.getKey! a :=
+  DTreeMap.Raw.getKey_eq_getKey! h
+
+@[simp]
+theorem getKeyD_emptyc {a : α} {fallback : α} :
+    (∅ : Raw α β cmp).getKeyD a fallback = fallback :=
+  DTreeMap.Raw.getKeyD_emptyc
+
+theorem getKeyD_of_isEmpty [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.isEmpty = true → t.getKeyD a fallback = fallback :=
+  DTreeMap.Raw.getKeyD_of_isEmpty h
+
+theorem getKeyD_insert [TransCmp cmp] (h : t.WF) {k a fallback : α} {v : β} :
+    (t.insert k v).getKeyD a fallback =
+      if cmp k a = .eq then k else t.getKeyD a fallback :=
+  DTreeMap.Raw.getKeyD_insert h
+
+@[simp]
+theorem getKeyD_insert_self [TransCmp cmp] (h : t.WF) {a fallback : α} {b : β} :
+    (t.insert a b).getKeyD a fallback = a :=
+  DTreeMap.Raw.getKeyD_insert_self h
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = false → t.getKeyD a fallback = fallback :=
+  DTreeMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h
+
+theorem getKeyD_eq_fallback [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    ¬ a ∈ t → t.getKeyD a fallback = fallback :=
+  DTreeMap.Raw.getKeyD_eq_fallback h
+
+theorem getKeyD_erase [TransCmp cmp] (h : t.WF) {k a fallback : α} :
+    (t.erase k).getKeyD a fallback =
+      if cmp k a = .eq then fallback else t.getKeyD a fallback :=
+  DTreeMap.Raw.getKeyD_erase h
+
+@[simp]
+theorem getKeyD_erase_self [TransCmp cmp] (h : t.WF) {k fallback : α} :
+    (t.erase k).getKeyD k fallback = fallback :=
+  DTreeMap.Raw.getKeyD_erase_self h
+
+theorem getKey?_eq_some_getKeyD_of_contains [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = true → t.getKey? a = some (t.getKeyD a fallback) :=
+  DTreeMap.Raw.getKey?_eq_some_getKeyD_of_contains h
+
+theorem getKey?_eq_some_getKeyD [TransCmp cmp] (h : t.WF) {a fallback : α} :
+  a ∈ t → t.getKey? a = some (t.getKeyD a fallback) :=
+  DTreeMap.Raw.getKey?_eq_some_getKeyD h
+
+theorem getKeyD_eq_getD_getKey? [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.getKeyD a fallback = (t.getKey? a).getD fallback :=
+  DTreeMap.Raw.getKeyD_eq_getD_getKey? h
+
+theorem getKey_eq_getKeyD [TransCmp cmp] (h : t.WF) {a fallback : α} {h'} :
+    t.getKey a h' = t.getKeyD a fallback :=
+  DTreeMap.Raw.getKey_eq_getKeyD h
+
+theorem getKey!_eq_getKeyD_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.getKey! a = t.getKeyD a default :=
+  DTreeMap.Raw.getKey!_eq_getKeyD_default h
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insertIfNew k v).isEmpty = false :=
+  DTreeMap.Raw.isEmpty_insertIfNew h
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a = (cmp k a == .eq || t.contains a) :=
+  DTreeMap.Raw.contains_insertIfNew h
+
+@[simp]
+theorem mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    a ∈ t.insertIfNew k v ↔ cmp k a = .eq ∨ a ∈ t :=
+  DTreeMap.Raw.mem_insertIfNew h
+
+theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insertIfNew k v).contains k :=
+  DTreeMap.Raw.contains_insertIfNew_self h
+
+theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    k ∈ t.insertIfNew k v :=
+  DTreeMap.Raw.mem_insertIfNew_self h
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a → cmp k a ≠ .eq → t.contains a :=
+  DTreeMap.Raw.contains_of_contains_insertIfNew h
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    a ∈ t.insertIfNew k v → cmp k a ≠ .eq → a ∈ t :=
+  DTreeMap.Raw.contains_of_contains_insertIfNew h
+
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
+proof obligation in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α}
+    {v : β} :
+    a ∈ (t.insertIfNew k v) → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  DTreeMap.Raw.mem_of_mem_insertIfNew' h
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) {v : β} :
+    (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1 :=
+  DTreeMap.Raw.size_insertIfNew h
+
+theorem size_le_size_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    t.size ≤ (t.insertIfNew k v).size :=
+  DTreeMap.Raw.size_le_size_insertIfNew h
+
+theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insertIfNew k v).size ≤ t.size + 1 :=
+  DTreeMap.Raw.size_insertIfNew_le h
+
+theorem getElem?_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v)[a]? =
+      if cmp k a = .eq ∧ ¬ k ∈ t then
+        some v
+      else
+        t[a]? :=
+  DTreeMap.Raw.Const.get?_insertIfNew h
+
+theorem getElem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
+    (t.insertIfNew k v)[a]'h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then
+        v
+      else
+        t[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
+  DTreeMap.Raw.Const.get_insertIfNew h
+
+theorem getElem!_insertIfNew [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v)[a]! = if cmp k a = .eq ∧ ¬ k ∈ t then v else t[a]! :=
+  DTreeMap.Raw.Const.get!_insertIfNew h
+
+theorem getD_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} :
+    getD (t.insertIfNew k v) a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback :=
+  DTreeMap.Raw.Const.getD_insertIfNew h
+
+theorem getKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v).getKey? a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a :=
+  DTreeMap.Raw.getKey?_insertIfNew h
+
+theorem getKey_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁} :
+    (t.insertIfNew k v).getKey a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) :=
+  DTreeMap.Raw.getKey_insertIfNew h
+
+theorem getKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α}
+    {v : β} :
+    (t.insertIfNew k v).getKey! a =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a :=
+  DTreeMap.Raw.getKey!_insertIfNew h
+
+theorem getKeyD_insertIfNew [TransCmp cmp] (h : t.WF) {k a fallback : α}
+    {v : β} :
+    (t.insertIfNew k v).getKeyD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback :=
+  DTreeMap.Raw.getKeyD_insertIfNew h
+
 end Std.TreeMap.Raw
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index ceac92f4a1..5c4927b7c4 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -112,6 +112,12 @@ theorem mem_of_mem_insert [TransCmp cmp] {k a : α} :
     a ∈ t.insert k → cmp k a ≠ .eq → a ∈ t :=
   TreeMap.mem_of_mem_insertIfNew
 
+/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
+proof obligation in the statement of `get_insert`. -/
+theorem mem_of_mem_insert' [TransCmp cmp] {k a : α} :
+    a ∈ t.insert k → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  TreeMap.mem_of_mem_insertIfNew'
+
 @[simp]
 theorem size_emptyc : (∅ : TreeSet α cmp).size = 0 :=
   TreeMap.size_emptyc
@@ -172,6 +178,152 @@ theorem size_le_size_erase [TransCmp cmp] {k : α} :
     t.size ≤ (t.erase k).size + 1 :=
   TreeMap.size_le_size_erase
 
+@[simp]
+theorem get?_emptyc {a : α} : (∅ : TreeSet α cmp).get? a = none :=
+  TreeMap.getKey?_emptyc
+
+theorem get?_of_isEmpty [TransCmp cmp] {a : α} :
+    t.isEmpty = true → t.get? a = none :=
+  TreeMap.getKey?_of_isEmpty
+
+theorem get?_insert [TransCmp cmp] {k a : α} :
+    (t.insert k).get? a = if cmp k a = .eq ∧ ¬k ∈ t then some k else t.get? a :=
+  TreeMap.getKey?_insertIfNew
+
+theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
+    t.contains a = (t.get? a).isSome :=
+  TreeMap.contains_eq_isSome_getKey?
+
+theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
+    t.contains a = false → t.get? a = none :=
+  TreeMap.getKey?_eq_none_of_contains_eq_false
+
+theorem get?_eq_none [TransCmp cmp] {a : α} :
+    ¬ a ∈ t → t.get? a = none :=
+  TreeMap.getKey?_eq_none
+
+theorem get?_erase [TransCmp cmp] {k a : α} :
+    (t.erase k).get? a = if cmp k a = .eq then none else t.get? a :=
+  TreeMap.getKey?_erase
+
+@[simp]
+theorem get?_erase_self [TransCmp cmp] {k : α} :
+    (t.erase k).get? k = none :=
+  TreeMap.getKey?_erase_self
+
+theorem get_insert [TransCmp cmp] {k a : α} {h₁} :
+    (t.insert k).get a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.get a (mem_of_mem_insert' h₁ h₂) :=
+  TreeMap.getKey_insertIfNew
+
+@[simp]
+theorem get_erase [TransCmp cmp] {k a : α} {h'} :
+    (t.erase k).get a h' = t.get a (mem_of_mem_erase h') :=
+  TreeMap.getKey_erase
+
+theorem get?_eq_some_get [TransCmp cmp] {a : α} {h'} :
+    t.get? a = some (t.get a h') :=
+  TreeMap.getKey?_eq_some_getKey
+
+@[simp]
+theorem get!_emptyc {a : α} [Inhabited α] :
+    (∅ : TreeSet α cmp).get! a = default :=
+  TreeMap.getKey!_emptyc
+
+theorem get!_of_isEmpty [TransCmp cmp] [Inhabited α] {a : α} :
+    t.isEmpty = true → t.get! a = default :=
+  TreeMap.getKey!_of_isEmpty
+
+theorem get!_insert [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.insert k).get! a = if cmp k a = .eq ∧ ¬ k ∈ t then k else t.get! a :=
+  TreeMap.getKey!_insertIfNew
+
+theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = false → t.get! a = default :=
+  TreeMap.getKey!_eq_default_of_contains_eq_false
+
+theorem get!_eq_default [TransCmp cmp] [Inhabited α] {a : α} :
+    ¬ a ∈ t → t.get! a = default :=
+  TreeMap.getKey!_eq_default
+
+theorem get!_erase [TransCmp cmp] [Inhabited α] {k a : α} :
+    (t.erase k).get! a = if cmp k a = .eq then default else t.get! a :=
+  TreeMap.getKey!_erase
+
+@[simp]
+theorem get!_erase_self [TransCmp cmp] [Inhabited α] {k : α} :
+    (t.erase k).get! k = default :=
+  TreeMap.getKey!_erase_self
+
+theorem get?_eq_some_get!_of_contains [TransCmp cmp] [Inhabited α] {a : α} :
+    t.contains a = true → t.get? a = some (t.get! a) :=
+  TreeMap.getKey?_eq_some_getKey!_of_contains
+
+theorem get?_eq_some_get! [TransCmp cmp] [Inhabited α] {a : α} :
+    a ∈ t → t.get? a = some (t.get! a) :=
+  TreeMap.getKey?_eq_some_getKey!
+
+theorem get!_eq_get!_get? [TransCmp cmp] [Inhabited α] {a : α} :
+    t.get! a = (t.get? a).get! :=
+  TreeMap.getKey!_eq_get!_getKey?
+
+theorem get_eq_get! [TransCmp cmp] [Inhabited α] {a : α} {h} :
+    t.get a h = t.get! a :=
+  TreeMap.getKey_eq_getKey!
+
+@[simp]
+theorem getD_emptyc {a : α} {fallback : α} :
+    (∅ : TreeSet α cmp).getD a fallback = fallback :=
+  TreeMap.getKeyD_emptyc
+
+theorem getD_of_isEmpty [TransCmp cmp] {a fallback : α} :
+    t.isEmpty = true → t.getD a fallback = fallback :=
+  TreeMap.getKeyD_of_isEmpty
+
+theorem getD_insert [TransCmp cmp] {k a fallback : α} :
+    (t.insert k).getD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getD a fallback :=
+  TreeMap.getKeyD_insertIfNew
+
+theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] {a fallback : α} :
+    t.contains a = false → t.getD a fallback = fallback :=
+  TreeMap.getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getD_eq_fallback [TransCmp cmp] {a fallback : α} :
+    ¬ a ∈ t → t.getD a fallback = fallback :=
+  TreeMap.getKeyD_eq_fallback
+
+theorem getD_erase [TransCmp cmp] {k a fallback : α} :
+    (t.erase k).getD a fallback =
+      if cmp k a = .eq then fallback else t.getD a fallback :=
+  TreeMap.getKeyD_erase
+
+@[simp]
+theorem getD_erase_self [TransCmp cmp] {k fallback : α} :
+    (t.erase k).getD k fallback = fallback :=
+  TreeMap.getKeyD_erase_self
+
+theorem get?_eq_some_getD_of_contains [TransCmp cmp] {a fallback : α} :
+    t.contains a = true → t.get? a = some (t.getD a fallback) :=
+  TreeMap.getKey?_eq_some_getKeyD_of_contains
+
+theorem get?_eq_some_getD [TransCmp cmp] {a fallback : α} :
+    a ∈ t → t.get? a = some (t.getD a fallback) :=
+  TreeMap.getKey?_eq_some_getKeyD
+
+theorem getD_eq_getD_get? [TransCmp cmp] {a fallback : α} :
+    t.getD a fallback = (t.get? a).getD fallback :=
+  TreeMap.getKeyD_eq_getD_getKey?
+
+theorem get_eq_getD [TransCmp cmp] {a fallback : α} {h} :
+    t.get a h = t.getD a fallback :=
+  TreeMap.getKey_eq_getKeyD
+
+theorem get!_eq_getD_default [TransCmp cmp] [Inhabited α] {a : α} :
+    t.get! a = t.getD a default :=
+  TreeMap.getKey!_eq_getKeyD_default
+
 @[simp]
 theorem containsThenInsert_fst [TransCmp cmp] {k : α} :
     (t.containsThenInsert k).1 = t.contains k :=
diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean
index 37e00af8d1..b888a88f98 100644
--- a/src/Std/Data/TreeSet/RawLemmas.lean
+++ b/src/Std/Data/TreeSet/RawLemmas.lean
@@ -112,6 +112,12 @@ theorem mem_of_mem_insert [TransCmp cmp] (h : t.WF) {k a : α} :
     a ∈ t.insert k → cmp k a ≠ .eq → a ∈ t :=
   TreeMap.Raw.mem_of_mem_insertIfNew h
 
+/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
+proof obligation in the statement of `get_insert`. -/
+theorem mem_of_mem_insert' [TransCmp cmp] (h : t.WF) {k a : α} :
+    a ∈ t.insert k → ¬ (cmp k a = .eq ∧ ¬ k ∈ t) → a ∈ t :=
+  TreeMap.Raw.mem_of_mem_insertIfNew' h
+
 @[simp]
 theorem size_emptyc : (∅ : Raw α cmp).size = 0 :=
   TreeMap.Raw.size_emptyc
@@ -172,6 +178,152 @@ theorem size_le_size_erase [TransCmp cmp] (h : t.WF) {k : α} :
     t.size ≤ (t.erase k).size + 1 :=
   TreeMap.Raw.size_le_size_erase h
 
+@[simp]
+theorem get?_emptyc {a : α} : (∅ : TreeSet α cmp).get? a = none :=
+  TreeMap.Raw.getKey?_emptyc
+
+theorem get?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.get? a = none :=
+  TreeMap.Raw.getKey?_of_isEmpty h
+
+theorem get?_insert [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.insert k).get? a = if cmp k a = .eq ∧ ¬k ∈ t then some k else t.get? a :=
+  TreeMap.Raw.getKey?_insertIfNew h
+
+theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = (t.get? a).isSome :=
+  TreeMap.Raw.contains_eq_isSome_getKey? h
+
+theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
+    t.contains a = false → t.get? a = none :=
+  TreeMap.Raw.getKey?_eq_none_of_contains_eq_false h
+
+theorem get?_eq_none [TransCmp cmp] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.get? a = none :=
+  TreeMap.Raw.getKey?_eq_none h
+
+theorem get?_erase [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.erase k).get? a = if cmp k a = .eq then none else t.get? a :=
+  TreeMap.Raw.getKey?_erase h
+
+@[simp]
+theorem get?_erase_self [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.erase k).get? k = none :=
+  TreeMap.Raw.getKey?_erase_self h
+
+theorem get_insert [TransCmp cmp] (h : t.WF) {k a : α} {h₁} :
+    (t.insert k).get a h₁ =
+      if h₂ : cmp k a = .eq ∧ ¬ k ∈ t then k
+      else t.get a (mem_of_mem_insert' h h₁ h₂) :=
+  TreeMap.Raw.getKey_insertIfNew h
+
+@[simp]
+theorem get_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
+    (t.erase k).get a h' = t.get a (mem_of_mem_erase h h') :=
+  TreeMap.Raw.getKey_erase h
+
+theorem get?_eq_some_get [TransCmp cmp] (h : t.WF) {a : α} {h'} :
+    t.get? a = some (t.get a h') :=
+  TreeMap.Raw.getKey?_eq_some_getKey h
+
+@[simp]
+theorem get!_emptyc {a : α} [Inhabited α] :
+    (∅ : TreeSet α cmp).get! a = default :=
+  TreeMap.Raw.getKey!_emptyc
+
+theorem get!_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.isEmpty = true → t.get! a = default :=
+  TreeMap.Raw.getKey!_of_isEmpty h
+
+theorem get!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.insert k).get! a = if cmp k a = .eq ∧ ¬ k ∈ t then k else t.get! a :=
+  TreeMap.Raw.getKey!_insertIfNew h
+
+theorem get!_eq_default_of_contains_eq_false [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = false → t.get! a = default :=
+  TreeMap.Raw.getKey!_eq_default_of_contains_eq_false h
+
+theorem get!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    ¬ a ∈ t → t.get! a = default :=
+  TreeMap.Raw.getKey!_eq_default h
+
+theorem get!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
+    (t.erase k).get! a = if cmp k a = .eq then default else t.get! a :=
+  TreeMap.Raw.getKey!_erase h
+
+@[simp]
+theorem get!_erase_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
+    (t.erase k).get! k = default :=
+  TreeMap.Raw.getKey!_erase_self h
+
+theorem get?_eq_some_get!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.contains a = true → t.get? a = some (t.get! a) :=
+  TreeMap.Raw.getKey?_eq_some_getKey!_of_contains h
+
+theorem get?_eq_some_get! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    a ∈ t → t.get? a = some (t.get! a) :=
+  TreeMap.Raw.getKey?_eq_some_getKey! h
+
+theorem get!_eq_get!_get? [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.get! a = (t.get? a).get! :=
+  TreeMap.Raw.getKey!_eq_get!_getKey? h
+
+theorem get_eq_get! [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {h'} :
+    t.get a h' = t.get! a :=
+  TreeMap.Raw.getKey_eq_getKey! h
+
+@[simp]
+theorem getD_emptyc {a : α} {fallback : α} :
+    (∅ : TreeSet α cmp).getD a fallback = fallback :=
+  TreeMap.Raw.getKeyD_emptyc
+
+theorem getD_of_isEmpty [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.isEmpty = true → t.getD a fallback = fallback :=
+  TreeMap.Raw.getKeyD_of_isEmpty h
+
+theorem getD_insert [TransCmp cmp] (h : t.WF) {k a fallback : α} :
+    (t.insert k).getD a fallback =
+      if cmp k a = .eq ∧ ¬ k ∈ t then k else t.getD a fallback :=
+  TreeMap.Raw.getKeyD_insertIfNew h
+
+theorem getD_eq_fallback_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = false → t.getD a fallback = fallback :=
+  TreeMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h
+
+theorem getD_eq_fallback [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    ¬ a ∈ t → t.getD a fallback = fallback :=
+  TreeMap.Raw.getKeyD_eq_fallback h
+
+theorem getD_erase [TransCmp cmp] (h : t.WF) {k a fallback : α} :
+    (t.erase k).getD a fallback =
+      if cmp k a = .eq then fallback else t.getD a fallback :=
+  TreeMap.Raw.getKeyD_erase h
+
+@[simp]
+theorem getD_erase_self [TransCmp cmp] (h : t.WF) {k fallback : α} :
+    (t.erase k).getD k fallback = fallback :=
+  TreeMap.Raw.getKeyD_erase_self h
+
+theorem get?_eq_some_getD_of_contains [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.contains a = true → t.get? a = some (t.getD a fallback) :=
+  TreeMap.Raw.getKey?_eq_some_getKeyD_of_contains h
+
+theorem get?_eq_some_getD [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    a ∈ t → t.get? a = some (t.getD a fallback) :=
+  TreeMap.Raw.getKey?_eq_some_getKeyD h
+
+theorem getD_eq_getD_get? [TransCmp cmp] (h : t.WF) {a fallback : α} :
+    t.getD a fallback = (t.get? a).getD fallback :=
+  TreeMap.Raw.getKeyD_eq_getD_getKey? h
+
+theorem get_eq_getD [TransCmp cmp] (h : t.WF) {a fallback : α} {h'} :
+    t.get a h' = t.getD a fallback :=
+  TreeMap.Raw.getKey_eq_getKeyD h
+
+theorem get!_eq_getD_default [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
+    t.get! a = t.getD a default :=
+  TreeMap.Raw.getKey!_eq_getKeyD_default h
+
 @[simp]
 theorem containsThenInsert_fst [TransCmp cmp] (h : t.WF) {k : α} :
     (t.containsThenInsert k).1 = t.contains k :=