refactor: HashMap/TreeMap and their extensional variants to use getElem instance (#11578)

This PR refactors the usage of `get` operation on
`HashMap`/`TreeMap`/`ExtHashMap`/`ExtTreeMap` to `getElem` instace.

Author: wkrozowski

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 α]