diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index cc3d969a156e..11288481adc2 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -704,7 +704,7 @@ theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h :
     {v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
   simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
 
-/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
+/-- 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 contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
     {v : β k} :
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 90edc69978a4..4c86c0a17251 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -815,13 +815,13 @@ theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v :
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew
 
-/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
+/-- 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 contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   Raw₀.contains_of_contains_insertIfNew' ⟨m.1, _⟩ m.2
 
-/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
+/-- 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' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index e11b6a29c999..603103498b6c 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -895,14 +895,14 @@ theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
 
-/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
+/-- 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 contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
     {v : β k} :
     (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a := by
   simp_to_raw using Raw₀.contains_of_contains_insertIfNew'
 
-/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
+/-- 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' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index 7ae56b03e63a..99154e03f19e 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 prelude
-import Std.Data.DTreeMap.Internal.Impl
+import Std.Data.DTreeMap.Internal.WF
 import Std.Data.DTreeMap.Raw
 
 /-!
@@ -97,9 +97,16 @@ def containsThenInsert (t : DTreeMap α β cmp) (a : α) (b : β a) : Bool × DT
   let p := t.inner.containsThenInsert a b t.wf.balanced
   (p.1, ⟨p.2.impl, t.wf.containsThenInsert⟩)
 
+@[inline, inherit_doc Raw.insertIfNew]
+def insertIfNew (t : DTreeMap α β cmp) (a : α) (b : β a) : DTreeMap α β cmp :=
+    letI : Ord α := ⟨cmp⟩; ⟨(t.inner.insertIfNew a b t.wf.balanced).impl, t.wf.insertIfNew⟩
+
 instance : Membership α (DTreeMap α β cmp) where
   mem m a := m.contains a
 
+instance {m : DTreeMap α β cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end DTreeMap
 
 end Std
diff --git a/src/Std/Data/DTreeMap/Internal/Impl/Query.lean b/src/Std/Data/DTreeMap/Internal/Impl/Query.lean
index 5d13a588e12b..268db6d5f14f 100644
--- a/src/Std/Data/DTreeMap/Internal/Impl/Query.lean
+++ b/src/Std/Data/DTreeMap/Internal/Impl/Query.lean
@@ -45,6 +45,9 @@ def contains [Ord α] (k : α) (t : Impl α β) : Bool :=
 instance [Ord α] : Membership α (Impl α β) where
   mem t a := t.contains a
 
+instance [Ord α] {m : Impl α β} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 /-- Returns `true` if the tree is empty. -/
 @[inline]
 def isEmpty (t : Impl α β) : Bool :=
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index 459e227ba85f..4d98dd4f98f5 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -28,6 +28,7 @@ scoped macro "wf_trivial" : tactic => `(tactic|
     | apply WF.ordered | apply WF.balanced | apply WF.insert | apply WF.insertSlow
     | apply WF.erase | apply WF.eraseSlow
     | apply WF.containsThenInsert | apply WF.containsThenInsertSlow
+    | apply WF.insertIfNew | apply WF.insertIfNewSlow
     | apply Ordered.distinctKeys
     | assumption
     ))
@@ -42,7 +43,8 @@ private def queryNames : Array Name :=
 
 private def modifyNames : Array Name :=
   #[``toListModel_insert, ``toListModel_insertSlow, ``toListModel_erase, ``toListModel_eraseSlow,
-    ``toListModel_containsThenInsert, ``toListModel_containsThenInsertSlow]
+    ``toListModel_containsThenInsert, ``toListModel_containsThenInsertSlow,
+    ``toListModel_insertIfNew, ``toListModel_insertIfNewSlow]
 
 private def congrNames : MacroM (Array (TSyntax `term)) := do
   return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
@@ -195,6 +197,118 @@ theorem containsThenInsertSlow_snd [TransOrd α] (h : t.WF) {k : α} {v : β k}
   rw [snd_containsThenInsertSlow_eq_containsThenInsert _ h.balanced, containsThenInsert_snd h,
     insert_eq_insertSlow]
 
+@[simp]
+theorem isEmpty_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.isEmpty = false := by
+  simp_to_model using List.isEmpty_insertEntryIfNew
+
+@[simp]
+theorem isEmpty_insertIfNewSlow [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNewSlow k v).isEmpty = false := by
+  simp_to_model using List.isEmpty_insertEntryIfNew
+
+@[simp]
+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 using List.containsKey_insertEntryIfNew
+
+@[simp]
+theorem contains_insertIfNewSlow [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNewSlow k v).contains a = (k == a || t.contains a) := by
+  simp_to_model using List.containsKey_insertEntryIfNew
+
+@[simp]
+theorem mem_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ (t.insertIfNew k v h.balanced).impl ↔ k == a ∨ a ∈ t := by
+  simp [mem_iff_contains, contains_insertIfNew, h]
+
+@[simp]
+theorem mem_insertIfNewSlow [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNewSlow k v ↔ k == a ∨ a ∈ t := by
+  simp [mem_iff_contains, contains_insertIfNew, h]
+
+theorem contains_insertIfNew_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.contains k := by
+  simp [contains_insertIfNew, h]
+
+theorem contains_insertIfNewSlow_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNewSlow k v).contains k := by
+  simp [contains_insertIfNewSlow, h]
+
+theorem mem_insertIfNew_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    k ∈ (t.insertIfNew k v h.balanced).impl := by
+  simp [contains_insertIfNew, h]
+
+theorem mem_insertIfNewSlow_self [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    k ∈ t.insertIfNewSlow k v := by
+  simp [contains_insertIfNewSlow, h]
+
+theorem contains_of_contains_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.contains a → (k == a) = false → t.contains a := by
+  simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
+
+theorem contains_of_contains_insertIfNewSlow [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNewSlow k v).contains a → (k == a) = false → t.contains a := by
+  simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
+
+theorem mem_of_mem_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ (t.insertIfNew k v h.balanced).impl → (k == a) = false → a ∈ t := by
+  simpa [mem_iff_contains] using contains_of_contains_insertIfNew h
+
+theorem mem_of_mem_insertIfNewSlow [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNewSlow k v → (k == a) = false → a ∈ t := by
+  simpa [mem_iff_contains] using contains_of_contains_insertIfNewSlow h
+
+/-- 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 contains_of_contains_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by
+  simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
+
+/-- This is a restatement of `contains_of_contains_insertIfNewSlow` that is written to exactly match the proof
+obligation in the statement of `get_insertIfNewSlow`. -/
+theorem contains_of_contains_insertIfNewSlow' [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    (t.insertIfNewSlow k v).contains a → ¬((k == a) ∧ t.contains k = false) → t.contains a := by
+  simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
+
+/-- 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' [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ (t.insertIfNew k v h.balanced).impl → ¬((k == a) ∧ ¬k ∈ t) → a ∈ t := by
+  simpa [mem_iff_contains] using 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_insertIfNewSlow' [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNewSlow k v → ¬((k == a) ∧ ¬k ∈ t) → a ∈ t := by
+  simpa [mem_iff_contains] using contains_of_contains_insertIfNewSlow' h
+
+theorem size_insertIfNew [TransOrd α] {k : α} (h : t.WF) {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.size = if k ∈ t then t.size else t.size + 1 := by
+  simp only [mem_iff_contains]
+  simp_to_model using List.length_insertEntryIfNew
+
+theorem size_insertIfNewSlow [TransOrd α] {k : α} (h : t.WF) {v : β k} :
+    (t.insertIfNewSlow k v).size = if k ∈ t then t.size else t.size + 1 := by
+  simp only [mem_iff_contains]
+  simp_to_model using List.length_insertEntryIfNew
+
+theorem size_le_size_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insertIfNew k v h.balanced).impl.size := by
+  simp_to_model using List.length_le_length_insertEntryIfNew
+
+theorem size_le_size_insertIfNewSlow [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    t.size ≤ (t.insertIfNewSlow k v).size := by
+  simp_to_model using List.length_le_length_insertEntryIfNew
+
+theorem size_insertIfNew_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.size ≤ t.size + 1 := by
+  simp_to_model using List.length_insertEntryIfNew_le
+
+theorem size_insertIfNewSlow_le [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNewSlow k v).size ≤ t.size + 1 := by
+  simp_to_model using List.length_insertEntryIfNew_le
+
 end Std.DTreeMap.Internal.Impl
 
 /-- Used as instance by the dependents of this file -/
diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean
index ed5cc267675c..1bec346efbff 100644
--- a/src/Std/Data/DTreeMap/Internal/Model.lean
+++ b/src/Std/Data/DTreeMap/Internal/Model.lean
@@ -216,6 +216,15 @@ Internal implementation detail of the tree map
 def eraseₘ [Ord α] (k : α) (t : Impl α β) (h : t.Balanced) : Impl α β :=
   updateCell k (fun _ => .empty) t h |>.impl
 
+/--
+Model implementation of the `insertIfNew` function.
+Internal implementation detail of the tree map
+-/
+def insertIfNewₘ [Ord α] (k : α) (v : β k) (l : Impl α β) (h : l.Balanced) : Impl α β :=
+  updateCell k (fun
+    | ⟨.none, _⟩ => .of k v
+    | c => c) l h |>.impl
+
 /-!
 ## Helper theorems for reasoning with key-value pairs
 -/
@@ -380,6 +389,25 @@ theorem snd_containsThenInsertIfNewSlow_eq_containsThenInsert [Ord α] (t : Impl
   · rfl
   · simp [insertSlow_eq_insertₘ, insert_eq_insertₘ, htb]
 
+theorem insertIfNew_eq_insertIfNewSlow [Ord α] {k : α} {v : β k} {l : Impl α β} {h} :
+    (insertIfNew k v l h).impl = insertIfNewSlow k v l := by
+  simp [insertIfNew, insertIfNewSlow]
+  split
+  · rfl
+  · simp [insert_eq_insertSlow]
+
+-- theorem insertIfNew_eq_insertₘ [Ord α] {k : α} {v : β k} {l : Impl α β} {h} :
+--     (insertIfNew k v l h).impl = insertₘ k v l h := by
+--   simp only [insertIfNewₘ]
+--   induction l
+--   · simp only [insertIfNew, updateCell]
+--     split <;> split <;> simp_all [balanceL_eq_balance, balanceR_eq_balance]
+--   · simp [insertIfNew, insertₘ, updateCell]
+
+-- theorem insertIfNewSlow_eq_insertₘ [Ord α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) :
+--     insertIfNewSlow k v l = insertₘ k v l h := by
+--   rw [← insertIfNew_eq_insertSlow (h := h), insert_eq_insertₘ]
+
 end Impl
 
 end Std.DTreeMap.Internal
diff --git a/src/Std/Data/DTreeMap/Internal/WF.lean b/src/Std/Data/DTreeMap/Internal/WF.lean
index 9079328c443f..d571e2f2eca0 100644
--- a/src/Std/Data/DTreeMap/Internal/WF.lean
+++ b/src/Std/Data/DTreeMap/Internal/WF.lean
@@ -717,6 +717,58 @@ theorem toListModel_containsThenInsertSlow [Ord α] [TransOrd α] {k : α} {v :
   rw [containsThenInsertSlow_eq_insertₘ]
   exact toListModel_insertₘ htb hto
 
+
+-- /-!
+-- ### `insertIfNewₘ`
+-- -/
+
+-- theorem WF.insert
+
+-- theorem ordered_insertIfNewₘ [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
+--     (hlo : l.Ordered) : (l.insertIfNewₘ k v hlb).Ordered :=
+--   ordered_updateAtKey _ hlo
+
+-- theorem toListModel_insertIfNewₘ [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced)
+--     (hlo : l.Ordered) : (l.insertIfNewₘ k v hlb).toListModel.Perm (insertEntry k v l.toListModel) := by
+--   refine toListModel_updateAtKey_perm _ hlo ?_ insertIfNewEntry_of_perm
+--     insertIfNewEntry_append_of_not_contains_right
+--   rintro ⟨(_|l), hl⟩
+--   · simp
+--   · simp only [Option.toList_some, Cell.of_inner]
+--     have h : l.fst == k := by simpa using OrientedCmp.eq_symm (hl l rfl)
+--     rw [insertIfNewEntry_of_containsKey (containsKey_cons_of_beq h), replaceEntry_cons_of_true h]
+
+/-!
+### `insertIfNew`
+-/
+
+theorem WF.insertIfNew [Ord α] {k : α} {v : β k} {l : Impl α β}
+    (h : l.WF) : (l.insertIfNew k v h.balanced).impl.WF := by
+  simp [Impl.insertIfNew]
+  split <;> simp only [h, h.insert]
+
+theorem toListModel_insertIfNew [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+    (hlb : l.Balanced) (hlo : l.Ordered) :
+    (l.insertIfNew k v hlb).impl.toListModel.Perm (insertEntryIfNew k v l.toListModel) := by
+  simp only [Impl.insertIfNew, insertEntryIfNew, cond_eq_if, apply_contains hlo]
+  split
+  · rfl
+  · refine (toListModel_insert hlb hlo).trans ?_
+    simp [insertEntry_of_containsKey_eq_false, *]
+
+/-!
+### `insertIfNewSlow`
+-/
+
+theorem WF.insertIfNewSlow [Ord α] {k : α} {v : β k} {l : Impl α β}
+    (h : l.WF) : (l.insertIfNewSlow k v).WF := by
+  simpa [insertIfNew_eq_insertIfNewSlow] using WF.insertIfNew h
+
+theorem toListModel_insertIfNewSlow [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
+    (hlb : l.Balanced) (hlo : l.Ordered) :
+    (l.insertIfNewSlow k v).toListModel.Perm (insertEntryIfNew k v l.toListModel) := by
+  simpa [insertIfNew_eq_insertIfNewSlow] using toListModel_insertIfNew hlb hlo
+
 /-!
 ## Deducing that well-formed trees are ordered
 -/
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index 0434af99ff70..d2dd05fd6b15 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -98,4 +98,59 @@ theorem containsThenInsert_snd [TransCmp cmp] {k : α} {v : β k} :
     (t.containsThenInsert k v).2 = t.insert k v :=
   ext <| congrArg Impl.TreeB.impl <| Impl.containsThenInsert_snd 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) = false → 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) = false → a ∈ t :=
+  Impl.contains_of_contains_insertIfNew t.wf
+
+/-- 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 contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β k} :
+    (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a :=
+  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
+
 end Std.DTreeMap
diff --git a/src/Std/Data/DTreeMap/Raw.lean b/src/Std/Data/DTreeMap/Raw.lean
index aca3d5efd931..5dd7b82503de 100644
--- a/src/Std/Data/DTreeMap/Raw.lean
+++ b/src/Std/Data/DTreeMap/Raw.lean
@@ -155,9 +155,19 @@ def containsThenInsert (t : Raw α β cmp) (a : α) (b : β a) : Bool × Raw α
   let p := t.inner.containsThenInsertSlow a b
   (p.1, ⟨p.2⟩)
 
+/--
+If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
+returns the map unaltered.
+-/
+@[inline] def insertIfNew (t : Raw α β cmp) (a : α) (b : β a) : Raw α β cmp :=
+    letI : Ord α := ⟨cmp⟩; ⟨t.inner.insertIfNewSlow a b⟩
+
 instance : Membership α (Raw α β cmp) where
   mem m a := m.contains a
 
+instance {m : Raw α β cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end Raw
 
 end DTreeMap
diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean
index 0ca9dfd06c8e..4b062eaebf78 100644
--- a/src/Std/Data/DTreeMap/RawLemmas.lean
+++ b/src/Std/Data/DTreeMap/RawLemmas.lean
@@ -98,4 +98,59 @@ theorem containsThenInsert_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
     (t.containsThenInsert k v).2 = t.insert k v :=
   ext <| Impl.containsThenInsertSlow_snd h
 
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).isEmpty = false :=
+  Impl.isEmpty_insertIfNewSlow 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_insertIfNewSlow 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_insertIfNewSlow h
+
+theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).contains k :=
+  Impl.contains_insertIfNewSlow_self h
+
+theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    k ∈ t.insertIfNew k v :=
+  Impl.mem_insertIfNewSlow_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) = false → t.contains a :=
+  Impl.contains_of_contains_insertIfNewSlow h
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} {v : β k} :
+    a ∈ t.insertIfNew k v → (cmp k a == .eq) = false → a ∈ t :=
+  Impl.contains_of_contains_insertIfNewSlow h
+
+/-- 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 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 k = false) → t.contains a :=
+  Impl.contains_of_contains_insertIfNewSlow' 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_insertIfNewSlow' 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_insertIfNewSlow 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_insertIfNewSlow h
+
+theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).size ≤ t.size + 1 :=
+  Impl.size_insertIfNewSlow_le h
+
 end Std.DTreeMap.Raw
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index c49f0c3d2858..5f823d0397ef 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -597,13 +597,13 @@ theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v :
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m :=
   DHashMap.mem_of_mem_insertIfNew
 
-/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
+/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `getElem_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   DHashMap.contains_of_contains_insertIfNew'
 
-/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `getElem_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 11da7fe358d4..fee929a69694 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -612,13 +612,13 @@ theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m :=
   DHashMap.Raw.mem_of_mem_insertIfNew h.out
 
-/-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
+/-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `getElem_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
     {v : β} : (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   DHashMap.Raw.contains_of_contains_insertIfNew' h.out
 
-/-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
+/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `getElem_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 5349b508418f..72c9a57a2d2b 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -95,9 +95,16 @@ def containsThenInsert (t : TreeMap α β cmp) (a : α) (b : β) : Bool × TreeM
   let p := t.inner.containsThenInsert a b
   (p.1, ⟨p.2⟩)
 
+@[inline, inherit_doc DTreeMap.insertIfNew]
+def insertIfNew (t : TreeMap α β cmp) (a : α) (b : β) : TreeMap α β cmp :=
+  ⟨t.inner.insertIfNew a b⟩
+
 instance : Membership α (TreeMap α β cmp) where
   mem m a := m.contains a
 
+instance {m : TreeMap α β cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end TreeMap
 
 end Std
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index bd8c8e71eac1..d95e22b6ad9c 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -96,4 +96,59 @@ theorem containsThenInsert_snd [TransCmp cmp] {k : α} {v : β} :
     (t.containsThenInsert k v).2 = t.insert k v :=
   ext <| DTreeMap.containsThenInsert_snd
 
+@[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
+
+theorem contains_insertIfNew_self [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).contains k :=
+  DTreeMap.contains_insertIfNew_self
+
+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) = false → 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) = false → a ∈ t :=
+  DTreeMap.contains_of_contains_insertIfNew
+
+/-- 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 contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a :=
+  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
+
 end Std.TreeMap
diff --git a/src/Std/Data/TreeMap/Raw.lean b/src/Std/Data/TreeMap/Raw.lean
index 5d12abf3a450..e89fde153a66 100644
--- a/src/Std/Data/TreeMap/Raw.lean
+++ b/src/Std/Data/TreeMap/Raw.lean
@@ -115,9 +115,16 @@ def containsThenInsert (t : Raw α β cmp) (a : α) (b : β) : Bool × Raw α β
   let p := t.inner.containsThenInsert a b
   (p.1, ⟨p.2⟩)
 
+@[inline, inherit_doc DTreeMap.Raw.insertIfNew]
+def insertIfNew (t : Raw α β cmp) (a : α) (b : β) : Raw α β cmp :=
+    letI : Ord α := ⟨cmp⟩; ⟨t.inner.insertIfNew a b⟩
+
 instance : Membership α (Raw α β cmp) where
   mem m a := m.contains a
 
+instance {m : Raw α β cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end Raw
 
 end TreeMap
diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean
index e79ffcd917e8..dd9a4b344b6c 100644
--- a/src/Std/Data/TreeMap/RawLemmas.lean
+++ b/src/Std/Data/TreeMap/RawLemmas.lean
@@ -96,4 +96,59 @@ theorem containsThenInsert_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (t.containsThenInsert k v).2 = t.insert k v :=
   ext <| DTreeMap.Raw.containsThenInsert_snd 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) = false → 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) = false → a ∈ t :=
+  DTreeMap.Raw.contains_of_contains_insertIfNew h
+
+/-- 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 contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} {v : β} :
+    (t.insertIfNew k v).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a :=
+  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
+
 end Std.TreeMap.Raw
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index b106c3a26b4c..087e1850fd31 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -95,9 +95,16 @@ def containsThenInsert (t : TreeSet α cmp) (a : α) : Bool × TreeSet α cmp :=
   let p := t.inner.containsThenInsert a ()
   (p.1, ⟨p.2⟩)
 
+@[inline, inherit_doc Raw.insertIfNew]
+def insertIfNew (t : TreeSet α cmp) (a : α) : TreeSet α cmp :=
+  ⟨t.inner.insertIfNew a ()⟩
+
 instance : Membership α (TreeSet α cmp) where
   mem m a := m.contains a
 
+instance {m : TreeSet α cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end TreeSet
 
 end Std
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index 9c400d043981..f3b8b68dbb3d 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -96,4 +96,59 @@ theorem containsThenInsert_snd [TransCmp cmp] {k : α} :
     (t.containsThenInsert k).2 = t.insert k :=
   ext <| TreeMap.containsThenInsert_snd
 
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} :
+    (t.insertIfNew k).isEmpty = false :=
+  DTreeMap.isEmpty_insertIfNew
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] {k a : α} :
+    (t.insertIfNew k).contains a = (cmp k a == .eq || t.contains a) :=
+  DTreeMap.contains_insertIfNew
+
+@[simp]
+theorem mem_insertIfNew [TransCmp cmp] {k a : α} :
+    a ∈ t.insertIfNew k ↔ cmp k a == .eq ∨ a ∈ t :=
+  DTreeMap.mem_insertIfNew
+
+theorem contains_insertIfNew_self [TransCmp cmp] {k : α} :
+    (t.insertIfNew k).contains k :=
+  DTreeMap.contains_insertIfNew_self
+
+theorem mem_insertIfNew_self [TransCmp cmp] {k : α} :
+    k ∈ t.insertIfNew k :=
+  DTreeMap.mem_insertIfNew_self
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] {k a : α} :
+    (t.insertIfNew k).contains a → (cmp k a == .eq) = false → t.contains a :=
+  DTreeMap.contains_of_contains_insertIfNew
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] {k a : α} :
+    a ∈ t.insertIfNew k → (cmp k a == .eq) = false → a ∈ t :=
+  DTreeMap.contains_of_contains_insertIfNew
+
+/-- 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 contains_of_contains_insertIfNew' [TransCmp cmp] {k a : α} :
+    (t.insertIfNew k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a :=
+  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 : α} :
+    a ∈ t.insertIfNew k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t :=
+  DTreeMap.mem_of_mem_insertIfNew'
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} :
+    (t.insertIfNew k).size = if k ∈ t then t.size else t.size + 1 :=
+  DTreeMap.size_insertIfNew
+
+theorem size_le_size_insertIfNew [TransCmp cmp] {k : α} :
+    t.size ≤ (t.insertIfNew k).size :=
+  DTreeMap.size_le_size_insertIfNew
+
+theorem size_insertIfNew_le [TransCmp cmp] {k : α} :
+    (t.insertIfNew k).size ≤ t.size + 1 :=
+  DTreeMap.size_insertIfNew_le
+
 end Std.TreeSet
diff --git a/src/Std/Data/TreeSet/Raw.lean b/src/Std/Data/TreeSet/Raw.lean
index a13f6a71a476..5fd82c6c533f 100644
--- a/src/Std/Data/TreeSet/Raw.lean
+++ b/src/Std/Data/TreeSet/Raw.lean
@@ -146,9 +146,24 @@ def containsThenInsert (t : Raw α cmp) (a : α) : Bool × Raw α cmp :=
   let p := t.inner.containsThenInsert a ()
   (p.1, ⟨p.2⟩)
 
+/--
+Inserts the given element into the set. If the tree set already contains an element that is
+equal (with regard to `==`) to the given element, then the tree set is returned unchanged.
+
+Note: this non-replacement behavior is true for `TreeSet` and `TreeSet.Raw`.
+The `insert` function on `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw` behaves
+differently: it will overwrite an existing mapping.
+-/
+@[inline]
+def insertIfNew (t : Raw α cmp) (a : α) : Raw α cmp :=
+    letI : Ord α := ⟨cmp⟩; ⟨t.inner.insertIfNew a ()⟩
+
 instance : Membership α (Raw α cmp) where
   mem m a := m.contains a
 
+instance {m : Raw α cmp} {a : α} : Decidable (a ∈ m) :=
+  show Decidable (m.contains a) from inferInstance
+
 end Raw
 
 end TreeSet
diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean
index f9de469e4788..415c479a0ac1 100644
--- a/src/Std/Data/TreeSet/RawLemmas.lean
+++ b/src/Std/Data/TreeSet/RawLemmas.lean
@@ -96,4 +96,59 @@ theorem containsThenInsert_snd [TransCmp cmp] (h : t.WF) {k : α} :
     (t.containsThenInsert k).2 = t.insert k :=
   ext <| TreeMap.Raw.containsThenInsert_snd h
 
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.insertIfNew k).isEmpty = false :=
+  DTreeMap.Raw.isEmpty_insertIfNew h
+
+@[simp]
+theorem contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.insertIfNew k).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 : α} :
+    a ∈ t.insertIfNew k ↔ cmp k a == .eq ∨ a ∈ t :=
+  DTreeMap.Raw.mem_insertIfNew h
+
+theorem contains_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.insertIfNew k).contains k :=
+  DTreeMap.Raw.contains_insertIfNew_self h
+
+theorem mem_insertIfNew_self [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.insertIfNew k :=
+  DTreeMap.Raw.mem_insertIfNew_self h
+
+theorem contains_of_contains_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.insertIfNew k).contains a → (cmp k a == .eq) = false → t.contains a :=
+  DTreeMap.Raw.contains_of_contains_insertIfNew h
+
+theorem mem_of_mem_insertIfNew [TransCmp cmp] (h : t.WF) {k a : α} :
+    a ∈ t.insertIfNew k → (cmp k a == .eq) = false → a ∈ t :=
+  DTreeMap.Raw.contains_of_contains_insertIfNew h
+
+/-- 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 contains_of_contains_insertIfNew' [TransCmp cmp] (h : t.WF) {k a : α} :
+    (t.insertIfNew k).contains a → ¬((cmp k a == .eq) ∧ t.contains k = false) → t.contains a :=
+  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 : α} :
+    a ∈ t.insertIfNew k → ¬((cmp k a == .eq) ∧ ¬k ∈ t) → a ∈ t :=
+  DTreeMap.Raw.mem_of_mem_insertIfNew' h
+
+theorem size_insertIfNew [TransCmp cmp] {k : α} (h : t.WF) :
+    (t.insertIfNew k).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 : α} :
+    t.size ≤ (t.insertIfNew k).size :=
+  DTreeMap.Raw.size_le_size_insertIfNew h
+
+theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.insertIfNew k).size ≤ t.size + 1 :=
+  DTreeMap.Raw.size_insertIfNew_le h
+
 end Std.TreeSet.Raw