diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
index 54431353cd5d..43c885f264c8 100644
--- a/src/Std/Data/ExtHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -1409,27 +1409,58 @@ theorem union_insert_right_eq_insert_union [EquivBEq α] [LawfulHashable α] {p
   simp only [union, insert, ExtDHashMap.union_eq, mk.injEq]
   exact ExtDHashMap.union_insert_right_eq_insert_union
 
+/- getElem? -/
+theorem getElem?_union [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m₁ ∪ m₂)[k]? = (m₂[k]?).or (m₁[k]?) :=
+  ExtDHashMap.Const.get?_union
+
+theorem getElem?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]? = m₂[k]? :=
+  ExtDHashMap.Const.get?_union_of_not_mem_left not_mem
+
+theorem getElem?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₂) :
+    (m₁ ∪ m₂)[k]? = m₁[k]? :=
+  ExtDHashMap.Const.get?_union_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} :
     (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) :=
   ExtDHashMap.Const.get?_union
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₁) :
     (m₁ ∪ m₂).get? k = m₂.get? k :=
   ExtDHashMap.Const.get?_union_of_not_mem_left not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₂) :
     (m₁ ∪ m₂).get? k = m₁.get? k :=
   ExtDHashMap.Const.get?_union_of_not_mem_right not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∪ m₂)[k]'(mem_union_of_right mem) = m₂[k]'mem :=
+  ExtDHashMap.Const.get_union_of_mem_right mem
+
+theorem getElem_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₁) {h'} :
+    (m₁ ∪ m₂)[k]'h' = m₂[k]'(mem_of_mem_union_of_not_mem_left h' not_mem) :=
+  ExtDHashMap.Const.get_union_of_not_mem_left not_mem (h' := h')
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (mem : k ∈ m₂) :
     (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem :=
   ExtDHashMap.Const.get_union_of_mem_right mem
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₁) {h'} :
     (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) :=
@@ -1450,16 +1481,33 @@ theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback :=
   ExtDHashMap.Const.getD_union_of_not_mem_right not_mem
 
+/- getElem! -/
+theorem getElem!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
+    (m₁ ∪ m₂)[k]! = m₂.getD k (m₁[k]!) :=
+  ExtDHashMap.Const.get!_union
+
+theorem getElem!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]! = m₂[k]! :=
+  ExtDHashMap.Const.get!_union_of_not_mem_left not_mem
+
+theorem getElem!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂)  :
+    (m₁ ∪ m₂)[k]! = m₁[k]! :=
+  ExtDHashMap.Const.get!_union_of_not_mem_right not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
     (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) :=
   ExtDHashMap.Const.get!_union
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) :
     (m₁ ∪ m₂).get! k = m₂.get! k :=
   ExtDHashMap.Const.get!_union_of_not_mem_left not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂)  :
     (m₁ ∪ m₂).get! k = m₁.get! k :=
   ExtDHashMap.Const.get!_union_of_not_mem_right not_mem
@@ -1579,33 +1627,62 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α
     k ∉ m₁ ∩ m₂ :=
   ExtDHashMap.not_mem_inter_of_not_mem_right not_mem
 
+/- getElem? -/
+theorem getElem?_inter [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none :=
+  ExtDHashMap.Const.get?_inter
+
+theorem getElem?_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]? = m₁[k]? :=
+  ExtDHashMap.Const.get?_inter_of_mem_right mem
+
+theorem getElem?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]? = none :=
+  ExtDHashMap.Const.get?_inter_of_not_mem_left not_mem
+
+theorem getElem?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]? = none :=
+  ExtDHashMap.Const.get?_inter_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m₁ ∩ m₂).get? k =
-    if k ∈ m₂ then m₁.get? k else none :=
+    (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none :=
   ExtDHashMap.Const.get?_inter
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (mem : k ∈ m₂) :
     (m₁ ∩ m₂).get? k = m₁.get? k :=
   ExtDHashMap.Const.get?_inter_of_mem_right mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₁) :
     (m₁ ∩ m₂).get? k = none :=
   ExtDHashMap.Const.get?_inter_of_not_mem_left not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₂) :
     (m₁ ∩ m₂).get? k = none :=
   ExtDHashMap.Const.get?_inter_of_not_mem_right not_mem
 
-/- get -/
+/- getElem -/
 @[simp]
+theorem getElem_inter [EquivBEq α] [LawfulHashable α]
+    {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
+    (m₁ ∩ m₂)[k]'h_mem = m₁[k]'(mem_inter_iff.1 h_mem).1 :=
+  ExtDHashMap.Const.get_inter (h_mem := h_mem)
+
+/- get -/
+@[deprecated getElem_inter (since := "2025-12-10")]
 theorem get_inter [EquivBEq α] [LawfulHashable α]
     {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
-    (m₁ ∩ m₂).get k h_mem =
-    m₁.get k (mem_inter_iff.1 h_mem).1 :=
+    (m₁ ∩ m₂).get k h_mem = m₁.get k (mem_inter_iff.1 h_mem).1 :=
   ExtDHashMap.Const.get_inter
 
 /- getD -/
@@ -1629,22 +1706,45 @@ theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     (m₁ ∩ m₂).getD k fallback = fallback :=
   ExtDHashMap.Const.getD_inter_of_not_mem_left not_mem
 
+/- getElem! -/
+theorem getElem!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
+    (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default :=
+  ExtDHashMap.Const.get!_inter
+
+theorem getElem!_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]! = m₁[k]! :=
+  ExtDHashMap.Const.get!_inter_of_mem_right mem
+
+theorem getElem!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]! = default :=
+  ExtDHashMap.Const.get!_inter_of_not_mem_right not_mem
+
+theorem getElem!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]! = default :=
+  ExtDHashMap.Const.get!_inter_of_not_mem_left not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
-    (m₁ ∩ m₂).get! k =
-    if k ∈ m₂ then m₁.get! k else default :=
+    (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default :=
   ExtDHashMap.Const.get!_inter
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (mem : k ∈ m₂) :
     (m₁ ∩ m₂).get! k = m₁.get! k :=
   ExtDHashMap.Const.get!_inter_of_mem_right mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
     (m₁ ∩ m₂).get! k = default :=
   ExtDHashMap.Const.get!_inter_of_not_mem_right not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
     (m₁ ∩ m₂).get! k = default :=
@@ -2490,12 +2590,12 @@ grind_pattern size_filter_le_size => (m.filter f).size
 
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} :
-    (m.filter f).size = m.size ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
+    (m.filter f).size = m.size ↔ ∀ k h, f (m.getKey k h) (m[k]'h) :=
   ExtDHashMap.Const.size_filter_eq_size_iff
 
 theorem filter_eq_self_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} :
-    m.filter f = m ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
+    m.filter f = m ↔ ∀ k h, f (m.getKey k h) (m[k]'h) :=
   ext_iff.trans ExtDHashMap.Const.filter_eq_self_iff
 
 theorem getElem?_filter [EquivBEq α] [LawfulHashable α]
diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean
index 84b000e25b30..f6bdfc059d0b 100644
--- a/src/Std/Data/ExtTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtTreeMap/Lemmas.lean
@@ -271,7 +271,7 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
 @[grind =] theorem getElem_insert [TransCmp cmp] {k a : α} {v : β} {h₁} :
     (t.insert k v)[a]'h₁ =
       if h₂ : cmp k a = .eq then v
-      else get t a (mem_of_mem_insert h₁ h₂) :=
+      else t[a]'(mem_of_mem_insert h₁ h₂) :=
   ExtDTreeMap.Const.get_insert (h₁ := h₁)
 
 @[simp]
@@ -386,7 +386,7 @@ theorem getD_erase_self [TransCmp cmp] {k : α} {fallback : β} :
   ExtDTreeMap.Const.getD_erase_self
 
 theorem getElem?_eq_some_getD_of_contains [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
+    t.contains a = true → t[a]? = some (getD t a fallback) :=
   ExtDTreeMap.Const.get?_eq_some_getD_of_contains
 
 theorem getElem?_eq_some_getD [TransCmp cmp] {a : α} {fallback : β} :
@@ -743,7 +743,7 @@ theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} :
 
 @[simp, grind =]
 theorem getThenInsertIfNew?_fst [TransCmp cmp] {k : α} {v : β} :
-    (getThenInsertIfNew? t k v).1 = get? t k :=
+    (getThenInsertIfNew? t k v).1 = t[k]? :=
   ExtDTreeMap.Const.getThenInsertIfNew?_fst
 
 @[simp, grind =]
@@ -1071,7 +1071,7 @@ theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
     (contains : (l.map Prod.fst).contains k = false)
     {h'} :
     (t.insertMany l)[k]'h' =
-    t.get k (mem_of_mem_insertMany_list h' contains) :=
+    t[k]'(mem_of_mem_insertMany_list h' contains) :=
   ExtDTreeMap.Const.get_insertMany_list_of_contains_eq_false contains (h' := h')
 
 theorem getElem_insertMany_list_of_mem [TransCmp cmp]
@@ -1086,7 +1086,7 @@ theorem getElem!_insertMany_list_of_contains_eq_false [TransCmp cmp]
     [BEq α] [LawfulBEqCmp cmp]
     {l : List (α × β)} {k : α} [Inhabited β]
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
-    (t.insertMany l)[k]! = t.get! k :=
+    (t.insertMany l)[k]! = t[k]! :=
   ExtDTreeMap.Const.get!_insertMany_list_of_contains_eq_false contains_eq_false
 
 theorem getElem!_insertMany_list_of_mem [TransCmp cmp]
@@ -1553,27 +1553,58 @@ theorem union_insert_right_eq_insert_union [TransCmp cmp] {p : (_ : α) × β} :
   simp only [union, insert, ExtDTreeMap.union_eq, mk.injEq]
   exact ExtDTreeMap.union_insert_right_eq_insert_union
 
+/- getElem? -/
+theorem getElem?_union [TransCmp cmp] {k : α} :
+    (t₁ ∪ t₂)[k]? = (t₂[k]?).or (t₁[k]?) :=
+  ExtDTreeMap.Const.get?_union
+
+theorem getElem?_union_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]? = t₂[k]? :=
+  ExtDTreeMap.Const.get?_union_of_not_mem_left not_mem
+
+theorem getElem?_union_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₂) :
+    (t₁ ∪ t₂)[k]? = t₁[k]? :=
+  ExtDTreeMap.Const.get?_union_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [TransCmp cmp] {k : α} :
     (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k) :=
   ExtDTreeMap.Const.get?_union
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get? k = t₂.get? k :=
   ExtDTreeMap.Const.get?_union_of_not_mem_left not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₂) :
     (t₁ ∪ t₂).get? k = t₁.get? k :=
   ExtDTreeMap.Const.get?_union_of_not_mem_right not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∪ t₂)[k]'(mem_union_of_right mem) = t₂[k]'mem :=
+  ExtDTreeMap.Const.get_union_of_mem_right mem
+
+theorem getElem_union_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₁) {h'} :
+    (t₁ ∪ t₂)[k]'h' = t₂[k]'(mem_of_mem_union_of_not_mem_left h' not_mem) :=
+  ExtDTreeMap.Const.get_union_of_not_mem_left not_mem (h' := h')
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∪ t₂).get k (mem_union_of_right mem) = t₂.get k mem :=
   ExtDTreeMap.Const.get_union_of_mem_right mem
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₁) {h'} :
     (t₁ ∪ t₂).get k h' = t₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) :=
@@ -1594,16 +1625,33 @@ theorem getD_union_of_not_mem_right [TransCmp cmp]
     (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback :=
   ExtDTreeMap.Const.getD_union_of_not_mem_right not_mem
 
+/- getElem! -/
+theorem getElem!_union [TransCmp cmp] {k : α} [Inhabited β] :
+    (t₁ ∪ t₂)[k]! = t₂.getD k (t₁[k]!) :=
+  ExtDTreeMap.Const.get!_union
+
+theorem getElem!_union_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]! = t₂[k]! :=
+  ExtDTreeMap.Const.get!_union_of_not_mem_left not_mem
+
+theorem getElem!_union_of_not_mem_right [TransCmp cmp] {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
+    (t₁ ∪ t₂)[k]! = t₁[k]! :=
+  ExtDTreeMap.Const.get!_union_of_not_mem_right not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [TransCmp cmp] {k : α} [Inhabited β] :
     (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k) :=
   ExtDTreeMap.Const.get!_union
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get! k = t₂.get! k :=
   ExtDTreeMap.Const.get!_union_of_not_mem_left not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [TransCmp cmp] {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
     (t₁ ∪ t₂).get! k = t₁.get! k :=
   ExtDTreeMap.Const.get!_union_of_not_mem_right not_mem
@@ -1720,33 +1768,62 @@ theorem not_mem_inter_of_not_mem_right [TransCmp cmp] {k : α}
     k ∉ t₁ ∩ t₂ :=
   ExtDTreeMap.not_mem_inter_of_not_mem_right not_mem
 
+/- getElem? -/
+theorem getElem?_inter [TransCmp cmp] {k : α} :
+    (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none :=
+  ExtDTreeMap.Const.get?_inter
+
+theorem getElem?_inter_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]? = t₁[k]? :=
+  ExtDTreeMap.Const.get?_inter_of_mem_right mem
+
+theorem getElem?_inter_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]? = none :=
+  ExtDTreeMap.Const.get?_inter_of_not_mem_left not_mem
+
+theorem getElem?_inter_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]? = none :=
+  ExtDTreeMap.Const.get?_inter_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [TransCmp cmp] {k : α} :
-    (t₁ ∩ t₂).get? k =
-    if k ∈ t₂ then t₁.get? k else none :=
+    (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none :=
   ExtDTreeMap.Const.get?_inter
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get? k = t₁.get? k :=
   ExtDTreeMap.Const.get?_inter_of_mem_right mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get? k = none :=
   ExtDTreeMap.Const.get?_inter_of_not_mem_left not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get? k = none :=
   ExtDTreeMap.Const.get?_inter_of_not_mem_right not_mem
 
-/- get -/
+/- getElem -/
 @[simp]
+theorem getElem_inter [TransCmp cmp]
+    {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
+    (t₁ ∩ t₂)[k]'h_mem = t₁[k]'(mem_inter_iff.1 h_mem).1 :=
+  ExtDTreeMap.Const.get_inter (h_mem := h_mem)
+
+/- get -/
+@[deprecated getElem_inter (since := "2025-12-10")]
 theorem get_inter [TransCmp cmp]
     {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
-    (t₁ ∩ t₂).get k h_mem =
-    t₁.get k (mem_inter_iff.1 h_mem).1 :=
+    (t₁ ∩ t₂).get k h_mem = t₁.get k (mem_inter_iff.1 h_mem).1 :=
   ExtDTreeMap.Const.get_inter
 
 /- getD -/
@@ -1770,22 +1847,45 @@ theorem getD_inter_of_not_mem_left [TransCmp cmp]
     (t₁ ∩ t₂).getD k fallback = fallback :=
   ExtDTreeMap.Const.getD_inter_of_not_mem_left not_mem
 
+/- getElem! -/
+theorem getElem!_inter [TransCmp cmp] {k : α} [Inhabited β] :
+    (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default :=
+  ExtDTreeMap.Const.get!_inter
+
+theorem getElem!_inter_of_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]! = t₁[k]! :=
+  ExtDTreeMap.Const.get!_inter_of_mem_right mem
+
+theorem getElem!_inter_of_not_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]! = default :=
+  ExtDTreeMap.Const.get!_inter_of_not_mem_right not_mem
+
+theorem getElem!_inter_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]! = default :=
+  ExtDTreeMap.Const.get!_inter_of_not_mem_left not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [TransCmp cmp] {k : α} [Inhabited β] :
-    (t₁ ∩ t₂).get! k =
-    if k ∈ t₂ then t₁.get! k else default :=
+    (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default :=
   ExtDTreeMap.Const.get!_inter
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get! k = t₁.get! k :=
   ExtDTreeMap.Const.get!_inter_of_mem_right mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get! k = default :=
   ExtDTreeMap.Const.get!_inter_of_not_mem_right not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get! k = default :=
@@ -1932,32 +2032,61 @@ theorem not_mem_diff_of_mem_right [TransCmp cmp] {k : α}
     k ∉ t₁ \ t₂ :=
   ExtDTreeMap.not_mem_diff_of_mem_right mem
 
+/- getElem? -/
+theorem getElem?_diff [TransCmp cmp] {k : α} :
+    (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]? :=
+  ExtDTreeMap.Const.get?_diff
+
+theorem getElem?_diff_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]? = t₁[k]? :=
+  ExtDTreeMap.Const.get?_diff_of_not_mem_right not_mem
+
+theorem getElem?_diff_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]? = none :=
+  ExtDTreeMap.Const.get?_diff_of_not_mem_left not_mem
+
+theorem getElem?_diff_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]? = none :=
+  ExtDTreeMap.Const.get?_diff_of_mem_right mem
+
 /- get? -/
+@[deprecated getElem?_diff (since := "2025-12-10")]
 theorem get?_diff [TransCmp cmp] {k : α} :
-    (t₁ \ t₂).get? k =
-    if k ∈ t₂ then none else t₁.get? k :=
+    (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k :=
   ExtDTreeMap.Const.get?_diff
 
+@[deprecated getElem?_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get? k = t₁.get? k :=
   ExtDTreeMap.Const.get?_diff_of_not_mem_right not_mem
 
+@[deprecated getElem?_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get? k = none :=
   ExtDTreeMap.Const.get?_diff_of_not_mem_left not_mem
 
+@[deprecated getElem?_diff_of_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ \ t₂).get? k = none :=
   ExtDTreeMap.Const.get?_diff_of_mem_right mem
 
+/- getElem -/
+theorem getElem_diff [TransCmp cmp]
+    {k : α} {h_mem : k ∈ t₁ \ t₂} :
+    (t₁ \ t₂)[k]'h_mem = t₁[k]'(mem_diff_iff.1 h_mem).1 :=
+  ExtDTreeMap.Const.get_diff (h_mem := h_mem)
+
 /- get -/
+@[deprecated getElem_diff (since := "2025-12-10")]
 theorem get_diff [TransCmp cmp]
     {k : α} {h_mem : k ∈ t₁ \ t₂} :
-    (t₁ \ t₂).get k h_mem =
-    t₁.get k (mem_diff_iff.1 h_mem).1 :=
+    (t₁ \ t₂).get k h_mem = t₁.get k (mem_diff_iff.1 h_mem).1 :=
   ExtDTreeMap.Const.get_diff
 
 /- getD -/
@@ -1981,22 +2110,45 @@ theorem getD_diff_of_not_mem_left [TransCmp cmp]
     (t₁ \ t₂).getD k fallback = fallback :=
   ExtDTreeMap.Const.getD_diff_of_not_mem_left not_mem
 
+/- getElem! -/
+theorem getElem!_diff [TransCmp cmp] {k : α} [Inhabited β] :
+    (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]! :=
+  ExtDTreeMap.Const.get!_diff
+
+theorem getElem!_diff_of_not_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]! = t₁[k]! :=
+  ExtDTreeMap.Const.get!_diff_of_not_mem_right not_mem
+
+theorem getElem!_diff_of_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]! = default :=
+  ExtDTreeMap.Const.get!_diff_of_mem_right mem
+
+theorem getElem!_diff_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]! = default :=
+  ExtDTreeMap.Const.get!_diff_of_not_mem_left not_mem
+
 /- get! -/
+@[deprecated getElem!_diff (since := "2025-12-10")]
 theorem get!_diff [TransCmp cmp] {k : α} [Inhabited β] :
-    (t₁ \ t₂).get! k =
-    if k ∈ t₂ then default else t₁.get! k :=
+    (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k :=
   ExtDTreeMap.Const.get!_diff
 
+@[deprecated getElem!_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get! k = t₁.get! k :=
   ExtDTreeMap.Const.get!_diff_of_not_mem_right not_mem
 
+@[deprecated getElem!_diff_of_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (mem : k ∈ t₂) :
     (t₁ \ t₂).get! k = default :=
   ExtDTreeMap.Const.get!_diff_of_mem_right mem
 
+@[deprecated getElem!_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get! k = default :=
@@ -2102,12 +2254,12 @@ section Alter
 
 theorem alter_eq_empty_iff_erase_eq_empty [TransCmp cmp] {k : α}
     {f : Option β → Option β} :
-    alter t k f = ∅ ↔ t.erase k = ∅ ∧ f (get? t k) = none := by
+    alter t k f = ∅ ↔ t.erase k = ∅ ∧ f t[k]? = none := by
   simpa only [ext_iff] using ExtDTreeMap.Const.alter_eq_empty_iff_erase_eq_empty
 
 @[simp]
 theorem alter_eq_empty_iff [TransCmp cmp] {k : α} {f : Option β → Option β} :
-    alter t k f = ∅ ↔ (t = ∅ ∨ (t.size = 1 ∧ k ∈ t)) ∧ (f (get? t k)) = none := by
+    alter t k f = ∅ ↔ (t = ∅ ∨ (t.size = 1 ∧ k ∈ t)) ∧ (f t[k]?) = none := by
   simpa only [ext_iff] using ExtDTreeMap.Const.alter_eq_empty_iff
 
 @[grind =]
@@ -2922,7 +3074,7 @@ theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : ExtTreeMap α 
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : alter t k f ≠ ∅) :
     (alter t k f).minKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   ExtDTreeMap.Const.minKey!_alter_eq_self (mt ext he)
 
 theorem minKey?_eq_some_minKeyD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
@@ -3049,7 +3201,7 @@ theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : ExtTreeMap α 
 theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : alter t k f ≠ ∅) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   ExtDTreeMap.Const.minKeyD_alter_eq_self (mt ext he)
 
 end Min
@@ -3499,7 +3651,7 @@ theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : ExtTreeMap α 
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : alter t k f ≠ ∅) :
     (alter t k f).maxKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   ExtDTreeMap.Const.maxKey!_alter_eq_self (mt ext he)
 
 theorem maxKey?_eq_some_maxKeyD [TransCmp cmp] (he : t ≠ ∅) {fallback} :
@@ -3626,7 +3778,7 @@ theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : ExtTreeMap α 
 theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : alter t k f ≠ ∅) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   ExtDTreeMap.Const.maxKeyD_alter_eq_self (mt ext he)
 
 end Max
@@ -3877,12 +4029,12 @@ grind_pattern size_filter_le_size => (t.filter f).size
 
 theorem size_filter_eq_size_iff [TransCmp cmp]
     {f : α → β → Bool} :
-    (t.filter f).size = t.size ↔ ∀ k h, f (t.getKey k h) (t.get k h) :=
+    (t.filter f).size = t.size ↔ ∀ k h, f (t.getKey k h) (t[k]'h) :=
   ExtDTreeMap.Const.size_filter_eq_size_iff
 
 theorem filter_eq_self_iff [TransCmp cmp]
     {f : α → β → Bool} :
-    t.filter f = t ↔ ∀ k h, f (t.getKey k h) (t.get k h) :=
+    t.filter f = t ↔ ∀ k h, f (t.getKey k h) (t[k]'h) :=
   ext_iff.trans ExtDTreeMap.Const.filter_eq_self_iff
 
 @[simp]
@@ -3953,7 +4105,7 @@ theorem getD_filter_of_getKey?_eq_some [TransCmp cmp]
 
 theorem keys_filter [TransCmp cmp] {f : α → β → Bool} :
     (t.filter f).keys =
-      (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h')))).unattach :=
+      (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (t[x]'(mem_of_mem_keys h')))).unattach :=
   ExtDTreeMap.Const.keys_filter
 
 @[grind =]
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 7446672161fd..cc57ffa9f153 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -802,7 +802,7 @@ theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
   DHashMap.getKeyD_insertIfNew
 
 @[simp, grind =]
-theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k :=
+theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = m[k]? :=
   DHashMap.Const.getThenInsertIfNew?_fst
 
 @[simp, grind =]
@@ -978,6 +978,13 @@ theorem getElem?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHas
     m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
   DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toArray
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ m[k]? = some v :=
+  DHashMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+
+@[deprecated find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some (since := "2025-12-10")]
 theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
     [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
     m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
@@ -1413,32 +1420,69 @@ theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α]
     (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) :=
   union_insert_right_equiv_insert_union
 
+/- getElem? -/
+theorem getElem?_union [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m₁ ∪ m₂)[k]? = m₂[k]?.or m₁[k]? :=
+  @DHashMap.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ k
+
+theorem getElem?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]? = m₂[k]? :=
+  @DHashMap.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
+
+theorem getElem?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₂) :
+    (m₁ ∪ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _  _ k not_mem
+
 /- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} :
     (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) :=
   @DHashMap.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ k
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₁) :
     (m₁ ∪ m₂).get? k = m₂.get? k :=
   @DHashMap.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₂) :
     (m₁ ∪ m₂).get? k = m₁.get? k :=
   @DHashMap.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _  _ k not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (contains_right : k ∈ m₂) :
+    (m₁ ∪ m₂)[k]'(mem_union_of_right contains_right) = m₂[k]'contains_right :=
+  @DHashMap.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k contains_right
+
+theorem getElem_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₁) {h'} :
+    (m₁ ∪ m₂)[k]'h' = m₂[k]'(mem_of_mem_union_of_not_mem_left h' not_mem) :=
+  @DHashMap.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h'
+
+theorem getElem_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : ¬k ∈ m₂) {h'} :
+    (m₁ ∪ m₂)[k]'h' = m₁[k]'(mem_of_mem_union_of_not_mem_right h' not_mem) :=
+  @DHashMap.Const.get_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h'
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (contains_right : k ∈ m₂) :
     (m₁ ∪ m₂).get k (mem_union_of_right contains_right) = m₂.get k contains_right :=
   @DHashMap.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k contains_right
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₁) {h'} :
     (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) :=
   @DHashMap.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h'
 
+@[deprecated getElem_union_of_not_mem_right (since := "2025-12-10")]
 theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : ¬k ∈ m₂) {h'} :
     (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) :=
@@ -1459,16 +1503,34 @@ theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback :=
   @DHashMap.Const.getD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
+    (m₁ ∪ m₂)[k]! = m₂.getD k m₁[k]! :=
+  @DHashMap.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ k
+
+theorem getElem!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]! = m₂[k]! :=
+  @DHashMap.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
+theorem getElem!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂)  :
+    (m₁ ∪ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Const.get!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
     (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) :=
   @DHashMap.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ k
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) :
     (m₁ ∪ m₂).get! k = m₂.get! k :=
   @DHashMap.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂)  :
     (m₁ ∪ m₂).get! k = m₁.get! k :=
@@ -1610,32 +1672,62 @@ theorem Equiv.inter_congr {m₃ m₄ : HashMap α β} [EquivBEq α] [LawfulHasha
     (m₁ ∩ m₂) ~m (m₃ ∩ m₄) :=
   ⟨DHashMap.Equiv.inter_congr equiv₁.1 equiv₂.1⟩
 
-/- get? -/
+/- getElem? -/
+theorem getElem?_inter [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none :=
+  @DHashMap.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ k
+
+theorem getElem?_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem
+
+theorem getElem?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]? = none :=
+  @DHashMap.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
+
+theorem getElem?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]? = none :=
+  @DHashMap.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
+
+/- get?-/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m₁ ∩ m₂).get? k =
-    if k ∈ m₂ then m₁.get? k else none :=
+    (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none :=
   @DHashMap.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ k
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (mem : k ∈ m₂) :
     (m₁ ∩ m₂).get? k = m₁.get? k :=
   @DHashMap.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₁) :
     (m₁ ∩ m₂).get? k = none :=
   @DHashMap.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₂) :
     (m₁ ∩ m₂).get? k = none :=
   @DHashMap.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
 
+/- getElem -/
+@[simp]
+theorem getElem_inter [EquivBEq α] [LawfulHashable α]
+    {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
+    (m₁ ∩ m₂)[k]'h_mem = m₁[k]'((mem_inter_iff.1 h_mem).1) :=
+  @DHashMap.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ k h_mem
+
 /- get -/
-@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α]
+@[deprecated getElem_inter (since := "2025-12-10")]
+theorem get_inter [EquivBEq α] [LawfulHashable α]
     {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
-    (m₁ ∩ m₂).get k h_mem =
-    m₁.get k ((mem_inter_iff.1 h_mem).1) :=
+    (m₁ ∩ m₂).get k h_mem = m₁.get k ((mem_inter_iff.1 h_mem).1) :=
   @DHashMap.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ k h_mem
 
 /- getD -/
@@ -1659,22 +1751,45 @@ theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     (m₁ ∩ m₂).getD k fallback = fallback :=
   @DHashMap.Const.getD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
+    (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default :=
+  @DHashMap.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ k
+
+theorem getElem!_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem
+
+theorem getElem!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]! = default :=
+  @DHashMap.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
+theorem getElem!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]! = default :=
+  @DHashMap.Const.get!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
-    (m₁ ∩ m₂).get! k =
-    if k ∈ m₂ then m₁.get! k else default :=
+    (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default :=
   @DHashMap.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ k
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (mem : k ∈ m₂) :
     (m₁ ∩ m₂).get! k = m₁.get! k :=
   @DHashMap.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
     (m₁ ∩ m₂).get! k = default :=
   @DHashMap.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
     (m₁ ∩ m₂).get! k = default :=
@@ -1822,22 +1937,45 @@ theorem not_mem_diff_of_mem_right [EquivBEq α] [LawfulHashable α] {k : α}
     k ∉ m₁ \ m₂ :=
   @DHashMap.not_mem_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem
 
+/- getElem? -/
+theorem getElem?_diff [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m₁ \ m₂)[k]? = if k ∈ m₂ then none else m₁[k]? :=
+  @DHashMap.Const.get?_diff _ _ _ _ m₁.inner m₂.inner _ _ k
+
+theorem getElem?_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ \ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Const.get?_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
+
+theorem getElem?_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ \ m₂)[k]? = none :=
+  @DHashMap.Const.get?_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
+
+theorem getElem?_diff_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ \ m₂)[k]? = none :=
+  @DHashMap.Const.get?_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem
+
 /- get? -/
+@[deprecated getElem?_diff (since := "2025-12-10")]
 theorem get?_diff [EquivBEq α] [LawfulHashable α] {k : α} :
-    (m₁ \ m₂).get? k =
-    if k ∈ m₂ then none else m₁.get? k :=
+    (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k :=
   @DHashMap.Const.get?_diff _ _ _ _ m₁.inner m₂.inner _ _ k
 
+@[deprecated getElem?_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₂) :
     (m₁ \ m₂).get? k = m₁.get? k :=
   @DHashMap.Const.get?_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
 
+@[deprecated getElem?_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} (not_mem : k ∉ m₁) :
     (m₁ \ m₂).get? k = none :=
   @DHashMap.Const.get?_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem
 
+@[deprecated getElem?_diff_of_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} (mem : k ∈ m₂) :
     (m₁ \ m₂).get? k = none :=
@@ -1859,11 +1997,18 @@ theorem Equiv.diff_congr {m₃ m₄ : HashMap α β} [EquivBEq α] [LawfulHashab
     (m₁ \ m₂) ~m (m₃ \ m₄) :=
   ⟨DHashMap.Equiv.diff_congr equiv₁.1 equiv₂.1⟩
 
+/- getElem -/
+@[simp]
+theorem getElem_diff [EquivBEq α] [LawfulHashable α]
+    {k : α} {h_mem : k ∈ m₁ \ m₂} :
+    (m₁ \ m₂)[k]'h_mem = m₁[k]'(mem_diff_iff.1 h_mem).1 :=
+  @DHashMap.Const.get_diff _ _ _ _ m₁.inner m₂.inner _ _ k h_mem
+
 /- get -/
-@[simp] theorem get_diff [EquivBEq α] [LawfulHashable α]
+@[deprecated getElem_diff (since := "2025-12-10")]
+theorem get_diff [EquivBEq α] [LawfulHashable α]
     {k : α} {h_mem : k ∈ m₁ \ m₂} :
-    (m₁ \ m₂).get k h_mem =
-    m₁.get k ((mem_diff_iff.1 h_mem).1) :=
+    (m₁ \ m₂).get k h_mem = m₁.get k ((mem_diff_iff.1 h_mem).1) :=
   @DHashMap.Const.get_diff _ _ _ _ m₁.inner m₂.inner _ _ k h_mem
 
 /- getD -/
@@ -1887,22 +2032,45 @@ theorem getD_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     (m₁ \ m₂).getD k fallback = fallback :=
   @DHashMap.Const.getD_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_diff [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
+    (m₁ \ m₂)[k]! = if k ∈ m₂ then default else m₁[k]! :=
+  @DHashMap.Const.get!_diff _ _ _ _ m₁.inner m₂.inner _ _ _ k
+
+theorem getElem!_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
+    (m₁ \ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Const.get!_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
+theorem getElem!_diff_of_mem_right [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (mem : k ∈ m₂) :
+    (m₁ \ m₂)[k]! = default :=
+  @DHashMap.Const.get!_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem
+
+theorem getElem!_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α]
+    {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
+    (m₁ \ m₂)[k]! = default :=
+  @DHashMap.Const.get!_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
+
 /- get! -/
+@[deprecated getElem!_diff (since := "2025-12-10")]
 theorem get!_diff [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] :
-    (m₁ \ m₂).get! k =
-    if k ∈ m₂ then default else m₁.get! k :=
+    (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k :=
   @DHashMap.Const.get!_diff _ _ _ _ m₁.inner m₂.inner _ _ _ k
 
+@[deprecated getElem!_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₂) :
     (m₁ \ m₂).get! k = m₁.get! k :=
   @DHashMap.Const.get!_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem
 
+@[deprecated getElem!_diff_of_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_mem_right [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (mem : k ∈ m₂) :
     (m₁ \ m₂).get! k = default :=
   @DHashMap.Const.get!_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem
 
+@[deprecated getElem!_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α]
     {k : α} [Inhabited β] (not_mem : k ∉ m₁) :
     (m₁ \ m₂).get! k = default :=
@@ -3195,12 +3363,12 @@ grind_pattern size_filter_le_size => (m.filter f).size
 
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} :
-    (m.filter f).size = m.size ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
+    (m.filter f).size = m.size ↔ ∀ k h, f (m.getKey k h) (m[k]'h) :=
   DHashMap.Const.size_filter_eq_size_iff
 
 theorem filter_equiv_self_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} :
-    m.filter f ~m m ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
+    m.filter f ~m m ↔ ∀ k h, f (m.getKey k h) (m[k]'h) :=
   ⟨fun h => DHashMap.Const.filter_equiv_self_iff.mp h.1,
     fun h => ⟨DHashMap.Const.filter_equiv_self_iff.mpr h⟩⟩
 
@@ -3272,7 +3440,7 @@ theorem getD_filter_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
 
 theorem keys_filter [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
     (m.filter f).keys.Perm
-      (m.keys.attach.filter (fun ⟨x, h'⟩ => f x (get m x (mem_of_mem_keys h')))).unattach :=
+      (m.keys.attach.filter (fun ⟨x, h'⟩ => f x (m[x]'(mem_of_mem_keys h')))).unattach :=
   DHashMap.Const.keys_filter
 
 @[grind =]
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 1a259c4ae58f..1e2d9a71ee5d 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -820,7 +820,7 @@ theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α
 
 @[simp, grind =]
 theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
-    (getThenInsertIfNew? m k v).1 = get? m k :=
+    (getThenInsertIfNew? m k v).1 = m[k]? :=
   DHashMap.Raw.Const.getThenInsertIfNew?_fst h.out
 
 @[simp, grind =]
@@ -983,6 +983,12 @@ theorem mem_toArray_iff_getElem?_eq_some [LawfulBEq α]
     (k, v) ∈ m.toArray ↔ m[k]? = some v :=
   DHashMap.Raw.Const.mem_toArray_iff_get?_eq_some h.out
 
+theorem getElem?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} (h : m.WF) :
+    m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
+  DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toArray h.out
+
+@[deprecated getElem?_eq_some_iff_exists_beq_and_mem_toArray (since := "2025-12-10")]
 theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
     {k : α} {v : β} (h : m.WF) :
     get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
@@ -1379,31 +1385,69 @@ theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α]
     (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) :=
   union_insert_right_equiv_insert_union h₁ h₂
 
+/- getElem? -/
+theorem getElem?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ ∪ m₂)[k]? = m₂[k]?.or m₁[k]? :=
+  @DHashMap.Raw.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
+
+theorem getElem?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]? = m₂[k]? :=
+  @DHashMap.Raw.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
+theorem getElem?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₂) :
+    (m₁ ∪ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Raw.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
+/- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
     get? (m₁ ∪ m₂) k = (get? m₂ k).or (get? m₁ k) :=
   @DHashMap.Raw.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₁) :
     get? (m₁ ∪ m₂) k = get? m₂ k :=
   @DHashMap.Raw.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₂) :
     get? (m₁ ∪ m₂) k = get? m₁ k :=
   @DHashMap.Raw.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∪ m₂)[k]'(mem_union_of_right h₁ h₂ mem) = m₂[k]'mem :=
+  @DHashMap.Raw.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
+
+theorem getElem_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₁) {h'} :
+    (m₁ ∪ m₂)[k]'h' = m₂[k]'(mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) :=
+  @DHashMap.Raw.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h'
+
+theorem getElem_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₂) {h'} :
+    (m₁ ∪ m₂)[k]'h' = m₁[k]'(mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) :=
+  @DHashMap.Raw.Const.get_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h'
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (mem : k ∈ m₂) :
     get (m₁ ∪ m₂) k (mem_union_of_right h₁ h₂ mem) = get m₂ k mem :=
   @DHashMap.Raw.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₁) {h'} :
     get (m₁ ∪ m₂) k h' = get m₂ k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) :=
   @DHashMap.Raw.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h'
 
+@[deprecated getElem_union_of_not_mem_right (since := "2025-12-10")]
 theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₂) {h'} :
     get (m₁ ∪ m₂) k h' = get m₁ k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) :=
@@ -1424,16 +1468,34 @@ theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m
     getD (m₁ ∪ m₂) k fallback = getD m₁ k fallback :=
   @DHashMap.Raw.Const.getD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ ∪ m₂)[k]! = getD m₂ k m₁[k]! :=
+  @DHashMap.Raw.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
+
+theorem getElem!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₁) :
+    (m₁ ∪ m₂)[k]! = m₂[k]! :=
+  @DHashMap.Raw.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
+theorem getElem!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : ¬k ∈ m₂) :
+    (m₁ ∪ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Raw.Const.get!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
     get! (m₁ ∪ m₂) k = getD m₂ k (get! m₁ k) :=
   @DHashMap.Raw.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₁) :
     get! (m₁ ∪ m₂) k = get! m₂ k :=
   @DHashMap.Raw.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : ¬k ∈ m₂) :
     get! (m₁ ∪ m₂) k = get! m₁ k :=
@@ -1589,32 +1651,62 @@ theorem Equiv.inter_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable
     (m₁ ∩ m₂) ~m (m₃ ∩ m₄) :=
   ⟨@DHashMap.Raw.Equiv.inter_congr _ _ _ _ m₁.inner m₂.inner m₃.inner m₄.inner _ _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩
 
+/- getElem? -/
+theorem getElem?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none :=
+  @DHashMap.Raw.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
+
+theorem getElem?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Raw.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
+
+theorem getElem?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]? = none :=
+  @DHashMap.Raw.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
+theorem getElem?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]? = none :=
+  @DHashMap.Raw.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
 /- get? -/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
-    get? (m₁ ∩ m₂) k =
-    if k ∈ m₂ then get? m₁ k else none :=
+    get? (m₁ ∩ m₂) k = if k ∈ m₂ then get? m₁ k else none :=
   @DHashMap.Raw.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (mem : k ∈ m₂) :
     get? (m₁ ∩ m₂) k = get? m₁ k :=
   @DHashMap.Raw.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₁) :
     get? (m₁ ∩ m₂) k = none :=
   @DHashMap.Raw.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₂) :
     get? (m₁ ∩ m₂) k = none :=
   @DHashMap.Raw.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+/- getElem -/
+@[simp]
+theorem getElem_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
+    (m₁ ∩ m₂)[k]'h_mem = m₁[k]'((mem_inter_iff h₁ h₂).1 h_mem).1 :=
+  @DHashMap.Raw.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem
+
 /- get -/
-@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+@[deprecated getElem_inter (since := "2025-12-10")]
+theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} {h_mem : k ∈ m₁ ∩ m₂} :
-    get (m₁ ∩ m₂) k h_mem =
-    get m₁ k ((mem_inter_iff h₁ h₂).1 h_mem).1 :=
+    get (m₁ ∩ m₂) k h_mem = get m₁ k ((mem_inter_iff h₁ h₂).1 h_mem).1 :=
   @DHashMap.Raw.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem
 
 /- getD -/
@@ -1639,22 +1731,45 @@ theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m
     getD (m₁ ∩ m₂) k fallback = fallback :=
   @DHashMap.Raw.Const.getD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default :=
+  @DHashMap.Raw.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
+
+theorem getElem!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ ∩ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Raw.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem
+
+theorem getElem!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ ∩ m₂)[k]! = default :=
+  @DHashMap.Raw.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
+theorem getElem!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ ∩ m₂)[k]! = default :=
+  @DHashMap.Raw.Const.get!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
-    get! (m₁ ∩ m₂) k =
-    if k ∈ m₂ then get! m₁ k else default :=
+    get! (m₁ ∩ m₂) k = if k ∈ m₂ then get! m₁ k else default :=
   @DHashMap.Raw.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (mem : k ∈ m₂) :
     get! (m₁ ∩ m₂) k = get! m₁ k :=
   @DHashMap.Raw.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₂) :
     get! (m₁ ∩ m₂) k = default :=
   @DHashMap.Raw.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₁) :
     get! (m₁ ∩ m₂) k = default :=
@@ -1830,32 +1945,62 @@ theorem Equiv.diff_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable 
     (m₁ \ m₂) ~m (m₃ \ m₄) :=
   ⟨@DHashMap.Raw.Equiv.diff_congr _ _ _ _ m₁.inner m₂.inner m₃.inner m₄.inner _ _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩
 
+/- getElem? -/
+theorem getElem?_diff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ \ m₂)[k]? = if k ∈ m₂ then none else m₁[k]? :=
+  @DHashMap.Raw.Const.get?_diff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
+
+theorem getElem?_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ \ m₂)[k]? = m₁[k]? :=
+  @DHashMap.Raw.Const.get?_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
+theorem getElem?_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ \ m₂)[k]? = none :=
+  @DHashMap.Raw.Const.get?_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
+
+theorem getElem?_diff_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ \ m₂)[k]? = none :=
+  @DHashMap.Raw.Const.get?_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
+
 /- get? -/
+@[deprecated getElem?_diff (since := "2025-12-10")]
 theorem get?_diff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
-    get? (m₁ \ m₂) k =
-    if k ∈ m₂ then none else get? m₁ k :=
+    get? (m₁ \ m₂) k = if k ∈ m₂ then none else get? m₁ k :=
   @DHashMap.Raw.Const.get?_diff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k
 
+@[deprecated getElem?_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₂) :
     get? (m₁ \ m₂) k = get? m₁ k :=
   @DHashMap.Raw.Const.get?_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem?_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₁) :
     get? (m₁ \ m₂) k = none :=
   @DHashMap.Raw.Const.get?_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem?_diff_of_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (mem : k ∈ m₂) :
     get? (m₁ \ m₂) k = none :=
   @DHashMap.Raw.Const.get?_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem
 
+/- getElem -/
+@[simp]
+theorem getElem_diff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} {h_mem : k ∈ m₁ \ m₂} :
+    (m₁ \ m₂)[k]'h_mem = m₁[k]'((mem_diff_iff h₁ h₂).1 h_mem).1 :=
+  @DHashMap.Raw.Const.get_diff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem
+
 /- get -/
-@[simp] theorem get_diff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
+@[deprecated getElem_diff (since := "2025-12-10")]
+theorem get_diff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} {h_mem : k ∈ m₁ \ m₂} :
-    get (m₁ \ m₂) k h_mem =
-    get m₁ k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
+    get (m₁ \ m₂) k h_mem = get m₁ k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
   @DHashMap.Raw.Const.get_diff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem
 
 /- getD -/
@@ -1880,22 +2025,45 @@ theorem getD_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁
     getD (m₁ \ m₂) k fallback = fallback :=
   @DHashMap.Raw.Const.getD_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem
 
+/- getElem! -/
+theorem getElem!_diff [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
+    (m₁ \ m₂)[k]! = if k ∈ m₂ then default else m₁[k]! :=
+  @DHashMap.Raw.Const.get!_diff _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
+
+theorem getElem!_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₂) :
+    (m₁ \ m₂)[k]! = m₁[k]! :=
+  @DHashMap.Raw.Const.get!_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
+theorem getElem!_diff_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (mem : k ∈ m₂) :
+    (m₁ \ m₂)[k]! = default :=
+  @DHashMap.Raw.Const.get!_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem
+
+theorem getElem!_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
+    {k : α} (not_mem : k ∉ m₁) :
+    (m₁ \ m₂)[k]! = default :=
+  @DHashMap.Raw.Const.get!_diff_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
+
 /- get! -/
+@[deprecated getElem!_diff (since := "2025-12-10")]
 theorem get!_diff [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} :
-    get! (m₁ \ m₂) k =
-    if k ∈ m₂ then default else get! m₁ k :=
+    get! (m₁ \ m₂) k = if k ∈ m₂ then default else get! m₁ k :=
   @DHashMap.Raw.Const.get!_diff _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k
 
+@[deprecated getElem!_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₂) :
     get! (m₁ \ m₂) k = get! m₁ k :=
   @DHashMap.Raw.Const.get!_diff_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem
 
+@[deprecated getElem!_diff_of_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (mem : k ∈ m₂) :
     get! (m₁ \ m₂) k = default :=
   @DHashMap.Raw.Const.get!_diff_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem
 
+@[deprecated getElem!_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF)
     {k : α} (not_mem : k ∉ m₁) :
     get! (m₁ \ m₂) k = default :=
@@ -3508,7 +3676,7 @@ theorem getElem!_map [LawfulBEq α] [Inhabited γ]
 theorem getElem!_map' [EquivBEq α] [LawfulHashable α] [Inhabited γ]
     {f : α → β → γ} {k : α} (h : m.WF) :
     (m.map f)[k]! =
-      ((get? m k).pmap (fun v h => f (m.getKey k h) v)
+      (m[k]?.pmap (fun v h => f (m.getKey k h) v)
         (fun _ h' => (mem_iff_isSome_getElem? h).mpr (Option.isSome_of_eq_some h'))).get! :=
   DHashMap.Raw.Const.get!_map' h.out
 
@@ -3528,7 +3696,7 @@ theorem getD_map [LawfulBEq α]
 theorem getD_map' [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} {fallback : γ} (h : m.WF) :
     getD (m.map f) k fallback =
-      ((get? m k).pmap (fun v h => f (m.getKey k h) v)
+      (m[k]?.pmap (fun v h => f (m.getKey k h) v)
         (fun _ h' => (mem_iff_isSome_getElem? h).mpr (Option.isSome_of_eq_some h'))).getD fallback :=
   DHashMap.Raw.Const.getD_map' h.out
 
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index 260d565f9e24..588c4e41ce76 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -290,7 +290,7 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
 @[grind =] theorem getElem_insert [TransCmp cmp] {k a : α} {v : β} {h₁} :
     (t.insert k v)[a]'h₁ =
       if h₂ : cmp k a = .eq then v
-      else get t a (mem_of_mem_insert h₁ h₂) :=
+      else t[a]'(mem_of_mem_insert h₁ h₂) :=
   DTreeMap.Const.get_insert
 
 @[simp]
@@ -413,7 +413,7 @@ theorem getD_erase_self [TransCmp cmp] {k : α} {fallback : β} :
   DTreeMap.Const.getD_erase_self
 
 theorem getElem?_eq_some_getD_of_contains [TransCmp cmp] {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
+    t.contains a = true → t[a]? = some (getD t a fallback) :=
   DTreeMap.Const.get?_eq_some_getD_of_contains
 
 theorem getElem?_eq_some_getD [TransCmp cmp] {a : α} {fallback : β} :
@@ -774,7 +774,7 @@ theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} :
 
 @[simp, grind =]
 theorem getThenInsertIfNew?_fst [TransCmp cmp] {k : α} {v : β} :
-    (getThenInsertIfNew? t k v).1 = get? t k :=
+    (getThenInsertIfNew? t k v).1 = t[k]? :=
   DTreeMap.Const.getThenInsertIfNew?_fst
 
 @[simp, grind =]
@@ -1089,7 +1089,7 @@ theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
     (contains : (l.map Prod.fst).contains k = false)
     {h'} :
     (t.insertMany l)[k]'h' =
-    t.get k (mem_of_mem_insertMany_list h' contains) :=
+    t[k]'(mem_of_mem_insertMany_list h' contains) :=
   DTreeMap.Const.get_insertMany_list_of_contains_eq_false contains
 
 theorem getElem_insertMany_list_of_mem [TransCmp cmp]
@@ -1104,7 +1104,7 @@ theorem getElem!_insertMany_list_of_contains_eq_false [TransCmp cmp]
     [BEq α] [LawfulBEqCmp cmp]
     {l : List (α × β)} {k : α} [Inhabited β]
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
-    (t.insertMany l)[k]! = t.get! k :=
+    (t.insertMany l)[k]! = t[k]! :=
   DTreeMap.Const.get!_insertMany_list_of_contains_eq_false contains_eq_false
 
 theorem getElem!_insertMany_list_of_mem [TransCmp cmp]
@@ -1579,33 +1579,71 @@ theorem union_insert_right_equiv_insert_union [TransCmp cmp] {p : (_ : α) × β
     (t₁ ∪ (t₂.insert p.fst p.snd)).Equiv ((t₁ ∪ t₂).insert p.fst p.snd) :=
   ⟨DTreeMap.union_insert_right_equiv_insert_union⟩
 
+/- getElem? -/
+theorem getElem?_union [TransCmp cmp]
+    {k : α} :
+    (t₁ ∪ t₂)[k]? = (t₂[k]?).or (t₁[k]?) :=
+  DTreeMap.Const.get?_union
+
+theorem getElem?_union_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]? = t₂[k]? :=
+  DTreeMap.Const.get?_union_of_not_mem_left not_mem
+
+theorem getElem?_union_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₂) :
+    (t₁ ∪ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Const.get?_union_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [TransCmp cmp]
     {k : α} :
     (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k) :=
   DTreeMap.Const.get?_union
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get? k = t₂.get? k :=
   DTreeMap.Const.get?_union_of_not_mem_left not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₂) :
     (t₁ ∪ t₂).get? k = t₁.get? k :=
   DTreeMap.Const.get?_union_of_not_mem_right not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∪ t₂)[k]'(mem_union_of_right mem) = t₂[k]'mem :=
+  DTreeMap.Const.get_union_of_mem_right mem
+
+theorem getElem_union_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₁) {h'} :
+    (t₁ ∪ t₂)[k]'h' = t₂[k]'(mem_of_mem_union_of_not_mem_left h' not_mem) :=
+  DTreeMap.Const.get_union_of_not_mem_left not_mem
+
+theorem getElem_union_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : ¬k ∈ t₂) {h'} :
+    (t₁ ∪ t₂)[k]'h' = t₁[k]'(mem_of_mem_union_of_not_mem_right h' not_mem) :=
+  DTreeMap.Const.get_union_of_not_mem_right not_mem
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∪ t₂).get k (mem_union_of_right mem) = t₂.get k mem :=
   DTreeMap.Const.get_union_of_mem_right mem
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₁) {h'} :
     (t₁ ∪ t₂).get k h' = t₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) :=
   DTreeMap.Const.get_union_of_not_mem_left not_mem
 
+@[deprecated getElem_union_of_not_mem_right (since := "2025-12-10")]
 theorem get_union_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : ¬k ∈ t₂) {h'} :
     (t₁ ∪ t₂).get k h' = t₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) :=
@@ -1627,17 +1665,36 @@ theorem getD_union_of_not_mem_right [TransCmp cmp]
     (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback :=
   DTreeMap.Const.getD_union_of_not_mem_right not_mem
 
+/- getElem! -/
+theorem getElem!_union [TransCmp cmp]
+    {k : α} [Inhabited β] :
+    (t₁ ∪ t₂)[k]! = t₂.getD k (t₁[k]!) :=
+  DTreeMap.Const.get!_union
+
+theorem getElem!_union_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]! = t₂[k]! :=
+  DTreeMap.Const.get!_union_of_not_mem_left not_mem
+
+theorem getElem!_union_of_not_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
+    (t₁ ∪ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Const.get!_union_of_not_mem_right not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [TransCmp cmp]
     {k : α} [Inhabited β] :
     (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k) :=
   DTreeMap.Const.get!_union
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get! k = t₂.get! k :=
   DTreeMap.Const.get!_union_of_not_mem_left not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
     (t₁ ∪ t₂).get! k = t₁.get! k :=
@@ -1779,33 +1836,62 @@ theorem Equiv.inter_congr {t₃ t₄ : TreeMap α β cmp} [TransCmp cmp]
   constructor
   apply DTreeMap.Equiv.inter_congr equiv₁.1 equiv₂.1
 
+/- getElem? -/
+theorem getElem?_inter [TransCmp cmp] {k : α} :
+    (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none :=
+  DTreeMap.Const.get?_inter
+
+theorem getElem?_inter_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Const.get?_inter_of_mem_right mem
+
+theorem getElem?_inter_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]? = none :=
+  DTreeMap.Const.get?_inter_of_not_mem_left not_mem
+
+theorem getElem?_inter_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]? = none :=
+  DTreeMap.Const.get?_inter_of_not_mem_right not_mem
+
 /- get? -/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [TransCmp cmp] {k : α} :
-    (t₁ ∩ t₂).get? k =
-    if k ∈ t₂ then t₁.get? k else none :=
+    (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none :=
   DTreeMap.Const.get?_inter
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get? k = t₁.get? k :=
   DTreeMap.Const.get?_inter_of_mem_right mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get? k = none :=
   DTreeMap.Const.get?_inter_of_not_mem_left not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get? k = none :=
   DTreeMap.Const.get?_inter_of_not_mem_right not_mem
 
-/- get -/
+/- getElem -/
 @[simp]
+theorem getElem_inter [TransCmp cmp]
+    {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
+    (t₁ ∩ t₂)[k]'h_mem = t₁[k]'(mem_inter_iff.1 h_mem).1 :=
+  DTreeMap.Const.get_inter
+
+/- get -/
+@[deprecated getElem_inter (since := "2025-12-10")]
 theorem get_inter [TransCmp cmp]
     {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
-    (t₁ ∩ t₂).get k h_mem =
-    t₁.get k (mem_inter_iff.1 h_mem).1 :=
+    (t₁ ∩ t₂).get k h_mem = t₁.get k (mem_inter_iff.1 h_mem).1 :=
   DTreeMap.Const.get_inter
 
 /- getD -/
@@ -1829,22 +1915,45 @@ theorem getD_inter_of_not_mem_left [TransCmp cmp]
     (t₁ ∩ t₂).getD k fallback = fallback :=
   DTreeMap.Const.getD_inter_of_not_mem_left not_mem
 
+/- getElem! -/
+theorem getElem!_inter [TransCmp cmp] {k : α} [Inhabited β] :
+    (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default :=
+  DTreeMap.Const.get!_inter
+
+theorem getElem!_inter_of_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Const.get!_inter_of_mem_right mem
+
+theorem getElem!_inter_of_not_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]! = default :=
+  DTreeMap.Const.get!_inter_of_not_mem_right not_mem
+
+theorem getElem!_inter_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]! = default :=
+  DTreeMap.Const.get!_inter_of_not_mem_left not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [TransCmp cmp] {k : α} [Inhabited β] :
-    (t₁ ∩ t₂).get! k =
-    if k ∈ t₂ then t₁.get! k else default :=
+    (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default :=
   DTreeMap.Const.get!_inter
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get! k = t₁.get! k :=
   DTreeMap.Const.get!_inter_of_mem_right mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get! k = default :=
   DTreeMap.Const.get!_inter_of_not_mem_right not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get! k = default :=
@@ -2010,32 +2119,61 @@ theorem Equiv.diff_congr {t₃ t₄ : TreeMap α β cmp} [TransCmp cmp]
   constructor
   apply DTreeMap.Equiv.diff_congr equiv₁.1 equiv₂.1
 
+/- getElem? -/
+theorem getElem?_diff [TransCmp cmp] {k : α} :
+    (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]? :=
+  DTreeMap.Const.get?_diff
+
+theorem getElem?_diff_of_not_mem_right [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Const.get?_diff_of_not_mem_right not_mem
+
+theorem getElem?_diff_of_not_mem_left [TransCmp cmp]
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]? = none :=
+  DTreeMap.Const.get?_diff_of_not_mem_left not_mem
+
+theorem getElem?_diff_of_mem_right [TransCmp cmp]
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]? = none :=
+  DTreeMap.Const.get?_diff_of_mem_right mem
+
 /- get? -/
+@[deprecated getElem?_diff (since := "2025-12-10")]
 theorem get?_diff [TransCmp cmp] {k : α} :
-    (t₁ \ t₂).get? k =
-    if k ∈ t₂ then none else t₁.get? k :=
+    (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k :=
   DTreeMap.Const.get?_diff
 
+@[deprecated getElem?_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_right [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get? k = t₁.get? k :=
   DTreeMap.Const.get?_diff_of_not_mem_right not_mem
 
+@[deprecated getElem?_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_left [TransCmp cmp]
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get? k = none :=
   DTreeMap.Const.get?_diff_of_not_mem_left not_mem
 
+@[deprecated getElem?_diff_of_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_mem_right [TransCmp cmp]
     {k : α} (mem : k ∈ t₂) :
     (t₁ \ t₂).get? k = none :=
   DTreeMap.Const.get?_diff_of_mem_right mem
 
+/- getElem -/
+theorem getElem_diff [TransCmp cmp]
+    {k : α} {h_mem : k ∈ t₁ \ t₂} :
+    (t₁ \ t₂)[k]'h_mem = t₁[k]'(mem_diff_iff.1 h_mem).1 :=
+  DTreeMap.Const.get_diff
+
 /- get -/
+@[deprecated getElem_diff (since := "2025-12-10")]
 theorem get_diff [TransCmp cmp]
     {k : α} {h_mem : k ∈ t₁ \ t₂} :
-    (t₁ \ t₂).get k h_mem =
-    t₁.get k (mem_diff_iff.1 h_mem).1 :=
+    (t₁ \ t₂).get k h_mem = t₁.get k (mem_diff_iff.1 h_mem).1 :=
   DTreeMap.Const.get_diff
 
 /- getD -/
@@ -2059,22 +2197,45 @@ theorem getD_diff_of_not_mem_left [TransCmp cmp]
     (t₁ \ t₂).getD k fallback = fallback :=
   DTreeMap.Const.getD_diff_of_not_mem_left not_mem
 
+/- getElem! -/
+theorem getElem!_diff [TransCmp cmp] {k : α} [Inhabited β] :
+    (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]! :=
+  DTreeMap.Const.get!_diff
+
+theorem getElem!_diff_of_not_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Const.get!_diff_of_not_mem_right not_mem
+
+theorem getElem!_diff_of_mem_right [TransCmp cmp]
+    {k : α} [Inhabited β] (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]! = default :=
+  DTreeMap.Const.get!_diff_of_mem_right mem
+
+theorem getElem!_diff_of_not_mem_left [TransCmp cmp]
+    {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]! = default :=
+  DTreeMap.Const.get!_diff_of_not_mem_left not_mem
+
 /- get! -/
+@[deprecated getElem!_diff (since := "2025-12-10")]
 theorem get!_diff [TransCmp cmp] {k : α} [Inhabited β] :
-    (t₁ \ t₂).get! k =
-    if k ∈ t₂ then default else t₁.get! k :=
+    (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k :=
   DTreeMap.Const.get!_diff
 
+@[deprecated getElem!_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get! k = t₁.get! k :=
   DTreeMap.Const.get!_diff_of_not_mem_right not_mem
 
+@[deprecated getElem!_diff_of_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_mem_right [TransCmp cmp]
     {k : α} [Inhabited β] (mem : k ∈ t₂) :
     (t₁ \ t₂).get! k = default :=
   DTreeMap.Const.get!_diff_of_mem_right mem
 
+@[deprecated getElem!_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_left [TransCmp cmp]
     {k : α} [Inhabited β] (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get! k = default :=
@@ -3004,7 +3165,7 @@ theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β}
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   DTreeMap.Const.minKey!_alter_eq_self he
 
 theorem minKey?_eq_some_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
@@ -3132,7 +3293,7 @@ theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β}
 theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   DTreeMap.Const.minKeyD_alter_eq_self he
 
 end Min
@@ -3585,7 +3746,7 @@ theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β}
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Const.maxKey!_alter_eq_self he
 
 theorem maxKey?_eq_some_maxKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
@@ -3713,7 +3874,7 @@ theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β}
 theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Const.maxKeyD_alter_eq_self he
 
 end Max
@@ -4381,12 +4542,12 @@ grind_pattern size_filter_le_size => (t.filter f).size
 
 theorem size_filter_eq_size_iff [TransCmp cmp]
     {f : α → β → Bool} :
-    (t.filter f).size = t.size ↔ ∀ k h, f (t.getKey k h) (t.get k h) :=
+    (t.filter f).size = t.size ↔ ∀ k h, f (t.getKey k h) (t[k]'h) :=
   DTreeMap.Const.size_filter_eq_size_iff
 
 theorem filter_equiv_self_iff [TransCmp cmp]
     {f : α → β → Bool} :
-    t.filter f ~m t ↔ ∀ k h, f (t.getKey k h) (t.get k h) :=
+    t.filter f ~m t ↔ ∀ k h, f (t.getKey k h) (t[k]'h) :=
   ⟨fun h => DTreeMap.Const.filter_equiv_self_iff.mp h.1,
     fun h => ⟨DTreeMap.Const.filter_equiv_self_iff.mpr h⟩⟩
 
@@ -4458,7 +4619,7 @@ theorem getD_filter_of_getKey?_eq_some [TransCmp cmp]
 
 theorem keys_filter [TransCmp cmp] {f : α → β → Bool} :
     (t.filter f).keys =
-      (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h')))).unattach :=
+      (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (t[x]'(mem_of_mem_keys h')))).unattach :=
   DTreeMap.Const.keys_filter
 
 @[grind =]
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index 636374c70f03..5619ebdd88a0 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -405,7 +405,7 @@ theorem getD_erase_self [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} :
   DTreeMap.Raw.Const.getD_erase_self h
 
 theorem getElem?_eq_some_getD_of_contains [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
-    t.contains a = true → get? t a = some (getD t a fallback) :=
+    t.contains a = true → t[a]? = some (getD t a fallback) :=
   DTreeMap.Raw.Const.get?_eq_some_getD_of_contains h
 
 theorem getElem?_eq_some_getD [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} :
@@ -781,7 +781,7 @@ theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
 
 @[simp, grind =]
 theorem getThenInsertIfNew?_fst [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
-    (getThenInsertIfNew? t k v).1 = get? t k :=
+    (getThenInsertIfNew? t k v).1 = t[k]? :=
   DTreeMap.Raw.Const.getThenInsertIfNew?_fst h
 
 @[simp, grind =]
@@ -1608,33 +1608,71 @@ theorem union_insert_right_equiv_insert_union [TransCmp cmp] {p : (_ : α) × β
     (t₁ ∪ (t₂.insert p.fst p.snd)).Equiv ((t₁ ∪ t₂).insert p.fst p.snd) :=
   ⟨DTreeMap.Raw.union_insert_right_equiv_insert_union h₁ h₂⟩
 
+/- getElem? -/
+theorem getElem?_union [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} :
+    (t₁ ∪ t₂)[k]? = (t₂[k]?).or (t₁[k]?) :=
+  DTreeMap.Raw.Const.get?_union h₁ h₂
+
+theorem getElem?_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]? = t₂[k]? :=
+  DTreeMap.Raw.Const.get?_union_of_not_mem_left h₁ h₂ not_mem
+
+theorem getElem?_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : ¬k ∈ t₂) :
+    (t₁ ∪ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Raw.Const.get?_union_of_not_mem_right h₁ h₂ not_mem
+
 /- get? -/
+@[deprecated getElem?_union (since := "2025-12-10")]
 theorem get?_union [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} :
     (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k) :=
   DTreeMap.Raw.Const.get?_union h₁ h₂
 
+@[deprecated getElem?_union_of_not_mem_left (since := "2025-12-10")]
 theorem get?_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get? k = t₂.get? k :=
   DTreeMap.Raw.Const.get?_union_of_not_mem_left h₁ h₂ not_mem
 
+@[deprecated getElem?_union_of_not_mem_right (since := "2025-12-10")]
 theorem get?_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : ¬k ∈ t₂) :
     (t₁ ∪ t₂).get? k = t₁.get? k :=
   DTreeMap.Raw.Const.get?_union_of_not_mem_right h₁ h₂ not_mem
 
+/- getElem -/
+theorem getElem_union_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∪ t₂)[k]'(mem_union_of_right h₁ h₂ mem) = t₂[k]'mem :=
+  DTreeMap.Raw.Const.get_union_of_mem_right h₁ h₂ mem
+
+theorem getElem_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : ¬k ∈ t₁) {h'} :
+    (t₁ ∪ t₂)[k]'h' = t₂[k]'(mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) :=
+  DTreeMap.Raw.Const.get_union_of_not_mem_left h₁ h₂ not_mem
+
+theorem getElem_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : ¬k ∈ t₂) {h'} :
+    (t₁ ∪ t₂)[k]'h' = t₁[k]'(mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) :=
+  DTreeMap.Raw.Const.get_union_of_not_mem_right h₁ h₂ not_mem
+
 /- get -/
+@[deprecated getElem_union_of_mem_right (since := "2025-12-10")]
 theorem get_union_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∪ t₂).get k (mem_union_of_right h₁ h₂ mem) = t₂.get k mem :=
   DTreeMap.Raw.Const.get_union_of_mem_right h₁ h₂ mem
 
+@[deprecated getElem_union_of_not_mem_left (since := "2025-12-10")]
 theorem get_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : ¬k ∈ t₁) {h'} :
     (t₁ ∪ t₂).get k h' = t₂.get k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) :=
   DTreeMap.Raw.Const.get_union_of_not_mem_left h₁ h₂ not_mem
 
+@[deprecated getElem_union_of_not_mem_right (since := "2025-12-10")]
 theorem get_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : ¬k ∈ t₂) {h'} :
     (t₁ ∪ t₂).get k h' = t₁.get k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) :=
@@ -1656,17 +1694,36 @@ theorem getD_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂
     (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback :=
   DTreeMap.Raw.Const.getD_union_of_not_mem_right h₁ h₂ not_mem
 
+/- getElem! -/
+theorem getElem!_union [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} [Inhabited β] :
+    (t₁ ∪ t₂)[k]! = t₂.getD k (t₁[k]!) :=
+  DTreeMap.Raw.Const.get!_union h₁ h₂
+
+theorem getElem!_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
+    (t₁ ∪ t₂)[k]! = t₂[k]! :=
+  DTreeMap.Raw.Const.get!_union_of_not_mem_left h₁ h₂ not_mem
+
+theorem getElem!_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
+    (t₁ ∪ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Raw.Const.get!_union_of_not_mem_right h₁ h₂ not_mem
+
 /- get! -/
+@[deprecated getElem!_union (since := "2025-12-10")]
 theorem get!_union [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} [Inhabited β] :
     (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k) :=
   DTreeMap.Raw.Const.get!_union h₁ h₂
 
+@[deprecated getElem!_union_of_not_mem_left (since := "2025-12-10")]
 theorem get!_union_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} [Inhabited β] (not_mem : ¬k ∈ t₁) :
     (t₁ ∪ t₂).get! k = t₂.get! k :=
   DTreeMap.Raw.Const.get!_union_of_not_mem_left h₁ h₂ not_mem
 
+@[deprecated getElem!_union_of_not_mem_right (since := "2025-12-10")]
 theorem get!_union_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} [Inhabited β] (not_mem : ¬k ∈ t₂)  :
     (t₁ ∪ t₂).get! k = t₁.get! k :=
@@ -1821,33 +1878,62 @@ theorem Equiv.inter_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp}
     (t₁ ∩ t₂).Equiv (t₃ ∩ t₄) :=
   ⟨DTreeMap.Raw.Equiv.inter_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1⟩
 
+/- getElem? -/
+theorem getElem?_inter [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
+    (t₁ ∩ t₂)[k]? = if k ∈ t₂ then t₁[k]? else none :=
+  DTreeMap.Raw.Const.get?_inter h₁ h₂
+
+theorem getElem?_inter_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Raw.Const.get?_inter_of_mem_right h₁ h₂ mem
+
+theorem getElem?_inter_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]? = none :=
+  DTreeMap.Raw.Const.get?_inter_of_not_mem_left h₁ h₂ not_mem
+
+theorem getElem?_inter_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]? = none :=
+  DTreeMap.Raw.Const.get?_inter_of_not_mem_right h₁ h₂ not_mem
+
 /- get? -/
+@[deprecated getElem?_inter (since := "2025-12-10")]
 theorem get?_inter [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
-    (t₁ ∩ t₂).get? k =
-    if k ∈ t₂ then t₁.get? k else none :=
+    (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none :=
   DTreeMap.Raw.Const.get?_inter h₁ h₂
 
+@[deprecated getElem?_inter_of_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get? k = t₁.get? k :=
   DTreeMap.Raw.Const.get?_inter_of_mem_right h₁ h₂ mem
 
+@[deprecated getElem?_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get? k = none :=
   DTreeMap.Raw.Const.get?_inter_of_not_mem_left h₁ h₂ not_mem
 
+@[deprecated getElem?_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get?_inter_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get? k = none :=
   DTreeMap.Raw.Const.get?_inter_of_not_mem_right h₁ h₂ not_mem
 
-/- get -/
+/- getElem -/
 @[simp]
+theorem getElem_inter [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
+    (t₁ ∩ t₂)[k]'h_mem = t₁[k]'((mem_inter_iff h₁ h₂).1 h_mem).1 :=
+  DTreeMap.Raw.Const.get_inter h₁ h₂
+
+/- get -/
+@[deprecated getElem_inter (since := "2025-12-10")]
 theorem get_inter [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} {h_mem : k ∈ t₁ ∩ t₂} :
-    (t₁ ∩ t₂).get k h_mem =
-    t₁.get k ((mem_inter_iff h₁ h₂).1 h_mem).1 :=
+    (t₁ ∩ t₂).get k h_mem = t₁.get k ((mem_inter_iff h₁ h₂).1 h_mem).1 :=
   DTreeMap.Raw.Const.get_inter h₁ h₂
 
 /- getD -/
@@ -1872,22 +1958,45 @@ theorem getD_inter_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.
     (t₁ ∩ t₂).getD k fallback = fallback :=
   DTreeMap.Raw.Const.getD_inter_of_not_mem_left h₁ h₂ not_mem
 
+/- getElem! -/
+theorem getElem!_inter [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
+    (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default :=
+  DTreeMap.Raw.Const.get!_inter h₁ h₂
+
+theorem getElem!_inter_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ ∩ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Raw.Const.get!_inter_of_mem_right h₁ h₂ mem
+
+theorem getElem!_inter_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ ∩ t₂)[k]! = default :=
+  DTreeMap.Raw.Const.get!_inter_of_not_mem_right h₁ h₂ not_mem
+
+theorem getElem!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ ∩ t₂)[k]! = default :=
+  DTreeMap.Raw.Const.get!_inter_of_not_mem_left h₁ h₂ not_mem
+
 /- get! -/
+@[deprecated getElem!_inter (since := "2025-12-10")]
 theorem get!_inter [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
-    (t₁ ∩ t₂).get! k =
-    if k ∈ t₂ then t₁.get! k else default :=
+    (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default :=
   DTreeMap.Raw.Const.get!_inter h₁ h₂
 
+@[deprecated getElem!_inter_of_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (mem : k ∈ t₂) :
     (t₁ ∩ t₂).get! k = t₁.get! k :=
   DTreeMap.Raw.Const.get!_inter_of_mem_right h₁ h₂ mem
 
+@[deprecated getElem!_inter_of_not_mem_right (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ ∩ t₂).get! k = default :=
   DTreeMap.Raw.Const.get!_inter_of_not_mem_right h₁ h₂ not_mem
 
+@[deprecated getElem!_inter_of_not_mem_left (since := "2025-12-10")]
 theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ ∩ t₂).get! k = default :=
@@ -2064,32 +2173,61 @@ theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp}
     (t₁ \ t₂).Equiv (t₃ \ t₄) :=
   ⟨DTreeMap.Raw.Equiv.diff_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1⟩
 
+/- getElem? -/
+theorem getElem?_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
+    (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]? :=
+  DTreeMap.Raw.Const.get?_diff h₁ h₂
+
+theorem getElem?_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]? = t₁[k]? :=
+  DTreeMap.Raw.Const.get?_diff_of_not_mem_right h₁ h₂ not_mem
+
+theorem getElem?_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]? = none :=
+  DTreeMap.Raw.Const.get?_diff_of_not_mem_left h₁ h₂ not_mem
+
+theorem getElem?_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]? = none :=
+  DTreeMap.Raw.Const.get?_diff_of_mem_right h₁ h₂ mem
+
 /- get? -/
+@[deprecated getElem?_diff (since := "2025-12-10")]
 theorem get?_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
-    (t₁ \ t₂).get? k =
-    if k ∈ t₂ then none else t₁.get? k :=
+    (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k :=
   DTreeMap.Raw.Const.get?_diff h₁ h₂
 
+@[deprecated getElem?_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get? k = t₁.get? k :=
   DTreeMap.Raw.Const.get?_diff_of_not_mem_right h₁ h₂ not_mem
 
+@[deprecated getElem?_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get?_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get? k = none :=
   DTreeMap.Raw.Const.get?_diff_of_not_mem_left h₁ h₂ not_mem
 
+@[deprecated getElem?_diff_of_mem_right (since := "2025-12-10")]
 theorem get?_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (mem : k ∈ t₂) :
     (t₁ \ t₂).get? k = none :=
   DTreeMap.Raw.Const.get?_diff_of_mem_right h₁ h₂ mem
 
+/- getElem -/
+theorem getElem_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} {h_mem : k ∈ t₁ \ t₂} :
+    (t₁ \ t₂)[k]'h_mem = t₁[k]'((mem_diff_iff h₁ h₂).1 h_mem).1 :=
+  DTreeMap.Raw.Const.get_diff h₁ h₂
+
 /- get -/
+@[deprecated getElem_diff (since := "2025-12-10")]
 theorem get_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} {h_mem : k ∈ t₁ \ t₂} :
-    (t₁ \ t₂).get k h_mem =
-    t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
+    (t₁ \ t₂).get k h_mem = t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 :=
   DTreeMap.Raw.Const.get_diff h₁ h₂
 
 /- getD -/
@@ -2114,22 +2252,45 @@ theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.W
     (t₁ \ t₂).getD k fallback = fallback :=
   DTreeMap.Raw.Const.getD_diff_of_not_mem_left h₁ h₂ not_mem
 
+/- getElem! -/
+theorem getElem!_diff [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
+    (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]! :=
+  DTreeMap.Raw.Const.get!_diff h₁ h₂
+
+theorem getElem!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₂) :
+    (t₁ \ t₂)[k]! = t₁[k]! :=
+  DTreeMap.Raw.Const.get!_diff_of_not_mem_right h₁ h₂ not_mem
+
+theorem getElem!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (mem : k ∈ t₂) :
+    (t₁ \ t₂)[k]! = default :=
+  DTreeMap.Raw.Const.get!_diff_of_mem_right h₁ h₂ mem
+
+theorem getElem!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
+    {k : α} (not_mem : k ∉ t₁) :
+    (t₁ \ t₂)[k]! = default :=
+  DTreeMap.Raw.Const.get!_diff_of_not_mem_left h₁ h₂ not_mem
+
 /- get! -/
+@[deprecated getElem!_diff (since := "2025-12-10")]
 theorem get!_diff [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} :
-    (t₁ \ t₂).get! k =
-    if k ∈ t₂ then default else t₁.get! k :=
+    (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k :=
   DTreeMap.Raw.Const.get!_diff h₁ h₂
 
+@[deprecated getElem!_diff_of_not_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₂) :
     (t₁ \ t₂).get! k = t₁.get! k :=
   DTreeMap.Raw.Const.get!_diff_of_not_mem_right h₁ h₂ not_mem
 
+@[deprecated getElem!_diff_of_mem_right (since := "2025-12-10")]
 theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (mem : k ∈ t₂) :
     (t₁ \ t₂).get! k = default :=
   DTreeMap.Raw.Const.get!_diff_of_mem_right h₁ h₂ mem
 
+@[deprecated getElem!_diff_of_not_mem_left (since := "2025-12-10")]
 theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF)
     {k : α} (not_mem : k ∉ t₁) :
     (t₁ \ t₂).get! k = default :=
@@ -2794,7 +2955,7 @@ theorem compare_minKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
 
 theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
     (t.alter k f).minKey? = some k ↔
-      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   DTreeMap.Raw.Const.minKey?_alter_eq_self h
 
 theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
@@ -2916,7 +3077,7 @@ theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inh
 theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).minKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   DTreeMap.Raw.Const.minKey!_alter_eq_self h he
 
 theorem minKey?_eq_some_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
@@ -3044,7 +3205,7 @@ theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h :
 theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.minKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
   DTreeMap.Raw.Const.minKeyD_alter_eq_self h he
 
 end Min
@@ -3232,7 +3393,7 @@ theorem compare_maxKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
 
 theorem maxKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
     (t.alter k f).maxKey? = some k ↔
-      (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Raw.Const.maxKey?_alter_eq_self h
 
 theorem maxKey?_eq_some_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
@@ -3356,7 +3517,7 @@ theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inh
 theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) :
     (alter t k f).maxKey! = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Raw.Const.maxKey!_alter_eq_self h he
 
 theorem maxKey?_eq_some_maxKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
@@ -3484,7 +3645,7 @@ theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h :
 theorem maxKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
     (he : (alter t k f).isEmpty = false) {fallback} :
     (alter t k f |>.maxKeyD fallback) = k ↔
-      (f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
+      (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
   DTreeMap.Raw.Const.maxKeyD_alter_eq_self h he
 
 end Max
@@ -4365,7 +4526,7 @@ theorem getElem!_map [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited γ]
 theorem getElem!_map' [TransCmp cmp] [Inhabited γ]
     {f : α → β → γ} {k : α} (h : t.WF) :
     (t.map f)[k]! =
-      ((get? t k).pmap (fun v h => f (t.getKey k h) v)
+      ((t[k]?).pmap (fun v h => f (t.getKey k h) v)
         (fun _ h' => (mem_iff_isSome_getElem? h).mpr (Option.isSome_of_eq_some h'))).get! :=
   DTreeMap.Raw.Const.get!_map' h.out
 
@@ -4385,7 +4546,7 @@ theorem getD_map [TransCmp cmp] [LawfulEqCmp cmp]
 theorem getD_map' [TransCmp cmp]
     {f : α → β → γ} {k : α} {fallback : γ} (h : t.WF) :
     getD (t.map f) k fallback =
-      ((get? t k).pmap (fun v h => f (t.getKey k h) v)
+      (t[k]?.pmap (fun v h => f (t.getKey k h) v)
         (fun _ h' => (mem_iff_isSome_getElem? h).mpr (Option.isSome_of_eq_some h'))).getD fallback :=
   DTreeMap.Raw.Const.getD_map' h.out