sorting

src/Std/Data/DHashMap/Basic.lean

@@ -152,6 +152,18 @@ variable {β : Type v}
 
 end
 
+@[inline, inherit_doc Raw.getKey?] def getKey? (m : DHashMap α β) (a : α) : Option α :=
+  Raw₀.getKey? ⟨m.1, m.2.size_buckets_pos⟩ a
+
+@[inline, inherit_doc Raw.getKey] def getKey (m : DHashMap α β) (a : α) (h : a ∈ m) : α :=
+  Raw₀.getKey ⟨m.1, m.2.size_buckets_pos⟩ a h
+
+@[inline, inherit_doc Raw.getKey!] def getKey! [Inhabited α] (m : DHashMap α β) (a : α) : α :=
+  Raw₀.getKey! ⟨m.1, m.2.size_buckets_pos⟩ a
+
+@[inline, inherit_doc Raw.getKeyD] def getKeyD (m : DHashMap α β) (a : α) (fallback : α) : α :=
+  Raw₀.getKeyD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
+
 @[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
   m.1.size
 

src/Std/Data/DHashMap/Internal/AssocList/Basic.lean

@@ -102,16 +102,31 @@ def getCast [BEq α] [LawfulBEq α] (a : α) : (l : AssocList α β) → l.conta
   | cons k v es, h => if hka : k == a then cast (congrArg β (eq_of_beq hka)) v
       else es.getCast a (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or])
 
+/-- Internal implementation detail of the hash map -/
+def getKey [BEq α] (a : α) : (l : AssocList α β) → l.contains a → α
+  | cons k _ es, h => if hka : k == a then k
+      else es.getKey a (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or])
+
 /-- Internal implementation detail of the hash map -/
 def getCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] : AssocList α β → β a
   | nil => panic! "key is not present in hash table"
   | cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v else es.getCast! a
 
+/-- Internal implementation detail of the hash map -/
+def getKey? [BEq α] (a : α) : AssocList α β → Option α
+  | nil => none
+  | cons k _ es => if k == a then some k else es.getKey? a
+
 /-- Internal implementation detail of the hash map -/
 def get! {β : Type v} [BEq α] [Inhabited β] (a : α) : AssocList α (fun _ => β) → β
   | nil => panic! "key is not present in hash table"
   | cons k v es => bif k == a then v else es.get! a
 
+/-- Internal implementation detail of the hash map -/
+def getKey! [BEq α] [Inhabited α] (a : α) : AssocList α β → α
+  | nil => panic! "key is not present in hash table"
+  | cons k _ es => if k == a then k else es.getKey! a
+
 /-- Internal implementation detail of the hash map -/
 def getCastD [BEq α] [LawfulBEq α] (a : α) (fallback : β a) : AssocList α β → β a
   | nil => fallback
@@ -123,6 +138,11 @@ def getD {β : Type v} [BEq α] (a : α) (fallback : β) : AssocList α (fun _ =
   | nil => fallback
   | cons k v es => bif k == a then v else es.getD a fallback
 
+/-- Internal implementation detail of the hash map -/
+def getKeyD [BEq α] (a : α) (fallback : α) : AssocList α β → α
+  | nil => fallback
+  | cons k _ es => if k == a then k else es.getKeyD a fallback
+
 /-- Internal implementation detail of the hash map -/
 def replace [BEq α] (a : α) (b : β a) : AssocList α β → AssocList α β
   | nil => nil

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -112,6 +112,32 @@ theorem get!_eq {β : Type v} [BEq α] [Inhabited β] {l : AssocList α (fun _ =
   · simp_all [get!, List.getValue!, List.getValue!, List.getValue?_cons,
       Bool.apply_cond Option.get!]
 
+@[simp]
+theorem getKey?_eq [BEq α] {l : AssocList α β} {a : α} :
+    l.getKey? a = List.getKey? a l.toList := by
+  induction l <;> simp_all [getKey?]
+
+@[simp]
+theorem getKey_eq [BEq α] {l : AssocList α β} {a : α} {h} :
+    l.getKey a h = List.getKey a l.toList (contains_eq.symm.trans h) := by
+  induction l
+  · simp [contains] at h
+  · next k v t ih => simp only [getKey, toList_cons, List.getKey_cons, ih]
+
+@[simp]
+theorem getKeyD_eq [BEq α] {l : AssocList α β} {a fallback : α} :
+    l.getKeyD a fallback = List.getKeyD a l.toList fallback := by
+  induction l
+  · simp [getKeyD, List.getKeyD]
+  · simp_all [getKeyD, List.getKeyD, Bool.apply_cond (fun x => Option.getD x fallback)]
+
+@[simp]
+theorem getKey!_eq [BEq α] [Inhabited α] {l : AssocList α β} {a : α} :
+    l.getKey! a = List.getKey! a l.toList := by
+  induction l
+  · simp [getKey!, List.getKey!]
+  · simp_all [getKey!, List.getKey!, Bool.apply_cond Option.get!]
+
 @[simp]
 theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} :
     (l.replace a b).toList = replaceEntry a b l.toList := by

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -100,9 +100,9 @@ Here is a summary of the steps required to add and verify a new operation:
   * Connect the implementation on lists and associative lists in `Internal.AssocList.Lemmas` via a
     lemma `AssocList.operation_eq`.
 3. Write the model implementation
-  * Write the model implementation `Raw₀.operationₘ` in `Internal.List.Model`
+  * Write the model implementation `Raw₀.operationₘ` in `Internal.Model`
   * Prove that the model implementation is equal to the actual implementation in
-    `Internal.List.Model` via a lemma `operation_eq_operationₘ`.
+    `Internal.Model` via a lemma `operation_eq_operationₘ`.
 4. Verify the model implementation
   * In `Internal.WF`, prove `operationₘ_eq_List.operation` (for access operations) or
     `wfImp_operationₘ` and `toListModel_operationₘ`
@@ -121,18 +121,18 @@ Here is a summary of the steps required to add and verify a new operation:
     might also have to prove that your list operation is invariant under permutation and add that to
     the tactic.
 7. State and prove the user-facing lemmas
-  * Restate all of your lemmas for `DHashMap.Raw` in `DHashMap.Lemmas` and prove them using the
+  * Restate all of your lemmas for `DHashMap.Raw` in `DHashMap.RawLemmas` and prove them using the
     provided tactic after hooking in your `operation_eq` and `operation_val` from step 5.
   * Restate all of your lemmas for `DHashMap` in `DHashMap.Lemmas` and prove them by reducing to
     `Raw₀`.
-  * Restate all of your lemmas for `HashMap.Raw` in `HashMap.Lemmas` and prove them by reducing to
+  * Restate all of your lemmas for `HashMap.Raw` in `HashMap.RawLemmas` and prove them by reducing to
     `DHashMap.Raw`.
   * Restate all of your lemmas for `HashMap` in `HashMap.Lemmas` and prove them by reducing to
     `DHashMap`.
-  * Restate all of your lemmas for `HashSet.Raw` in `HashSet.Lemmas` and prove them by reducing to
-    `DHashSet.Raw`.
+  * Restate all of your lemmas for `HashSet.Raw` in `HashSet.RawLemmas` and prove them by reducing to
+    `HashMap.Raw`.
   * Restate all of your lemmas for `HashSet` in `HashSet.Lemmas` and prove them by reducing to
-    `DHashSet`.
+    `HashMap`.
 
 This sounds like a lot of work (and it is if you have to add a lot of user-facing lemmas), but the
 framework is set up in such a way that each step is really easy and the proofs are all really short
@@ -420,6 +420,30 @@ variable {β : Type v}
 
 end
 
+/-- Internal implementation detail of the hash map -/
+@[inline] def getKey? [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α :=
+  let ⟨⟨_, buckets⟩, h⟩ := m
+  let ⟨i, h⟩ := mkIdx buckets.size h (hash a)
+  buckets[i].getKey? a
+
+/-- Internal implementation detail of the hash map -/
+@[inline] def getKey [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (hma : m.contains a) : α :=
+  let ⟨⟨_, buckets⟩, h⟩ := m
+  let idx := mkIdx buckets.size h (hash a)
+  buckets[idx.1].getKey a hma
+
+/-- Internal implementation detail of the hash map -/
+@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α :=
+  let ⟨⟨_, buckets⟩, h⟩ := m
+  let idx := mkIdx buckets.size h (hash a)
+  buckets[idx.1].getKeyD a fallback
+
+/-- Internal implementation detail of the hash map -/
+@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α :=
+  let ⟨⟨_, buckets⟩, h⟩ := m
+  let idx := mkIdx buckets.size h (hash a)
+  buckets[idx.1].getKey! a
+
 end Raw₀
 
 /-- Internal implementation detail of the hash map -/

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -526,6 +526,111 @@ theorem getValue!_eq_getValueD_default [BEq α] [Inhabited β] {l : List ((_ :
 
 end
 
+/-- Internal implementation detail of the hash map -/
+def getKey? [BEq α] (a : α) : List ((a : α) × β a) → Option α
+  | [] => none
+  | ⟨k, _⟩ :: l => bif k == a then some k else getKey? a l
+
+@[simp] theorem getKey?_nil [BEq α] {a : α} :
+    getKey? a ([] : List ((a : α) × β a)) = none := rfl
+
+@[simp] theorem getKey?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
+    getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else getKey? a l := rfl
+
+theorem getKey?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
+    getKey? a (⟨k, v⟩ :: l) = some k := by
+  simp [h]
+
+theorem getKey?_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
+    (h : (k == a) = false) : getKey? a (⟨k, v⟩ :: l) = getKey? a l := by
+  simp [h]
+
+theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
+    getKey? a l = (getEntry? a l).map (·.1) := by
+  induction l using assoc_induction
+  · simp
+  · next k v l ih =>
+    cases h : k == a
+    · rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]
+    · rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']
+
+theorem containsKey_eq_isSome_getKey? [BEq α] {l : List ((a : α) × β a)} {a : α} :
+    containsKey a l = (getKey? a l).isSome := by
+  simp [containsKey_eq_isSome_getEntry?, getKey?_eq_getEntry?]
+
+/-- Internal implementation detail of the hash map -/
+def getKey [BEq α] (a : α) (l : List ((a : α) × β a)) (h : containsKey a l) : α :=
+  (getKey? a l).get <| containsKey_eq_isSome_getKey?.symm.trans h
+
+theorem getKey?_eq_some_getKey [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
+    getKey? a l = some (getKey a l h) := by
+  simp [getKey]
+
+theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {h} :
+    getKey a (⟨k, v⟩ :: l) h = if h' : k == a then k
+      else getKey a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, getKey?_cons, apply_dite Option.some,
+    cond_eq_if]
+  split
+  · rfl
+  · exact getKey?_eq_some_getKey _
+
+/-- Internal implementation detail of the hash map -/
+def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
+  (getKey? a l).getD fallback
+
+@[simp]
+theorem getKeyD_nil [BEq α] {a fallback : α} :
+  getKeyD a ([] : List ((a : α) × β a)) fallback = fallback := rfl
+
+theorem getKeyD_eq_getKey? [BEq α] {l : List ((a : α) × β a)} {a fallback : α} :
+  getKeyD a l fallback = (getKey? a l).getD fallback := rfl
+
+theorem getKeyD_eq_fallback [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
+    (h : containsKey a l = false) : getKeyD a l fallback = fallback := by
+  rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
+    Option.not_isSome_iff_eq_none] at h
+  rw [getKeyD_eq_getKey?, h, Option.getD_none]
+
+theorem getKey_eq_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
+    (h : containsKey a l = true) :
+    getKey a l h = getKeyD a l fallback := by
+  rw [getKeyD_eq_getKey?, getKey, Option.get_eq_getD]
+
+theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
+    (h : containsKey a l = true) :
+    getKey? a l = some (getKeyD a l fallback) := by
+  rw [getKey?_eq_some_getKey h, getKey_eq_getKeyD]
+
+/-- Internal implementation detail of the hash map -/
+def getKey! [BEq α] [Inhabited α] (a : α) (l : List ((a : α) × β a)) : α :=
+  (getKey? a l).get!
+
+@[simp]
+theorem getKey!_nil [BEq α] [Inhabited α] {a : α} :
+    getKey! a ([] : List ((a : α) × β a)) = default := rfl
+
+theorem getKey!_eq_getKey? [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α} :
+    getKey! a l = (getKey? a l).get! := rfl
+
+theorem getKey!_eq_default [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
+    (h : containsKey a l = false) : getKey! a l = default := by
+  rw [containsKey_eq_isSome_getKey?, Bool.eq_false_iff, ne_eq,
+    Option.not_isSome_iff_eq_none] at h
+  rw [getKey!_eq_getKey?, h, Option.get!_none]
+
+theorem getKey_eq_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
+    (h : containsKey a l = true) : getKey a l h = getKey! a l := by
+  rw [getKey!_eq_getKey?, getKey, Option.get_eq_get!]
+
+theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
+    (h : containsKey a l = true) :
+    getKey? a l = some (getKey! a l) := by
+  rw [getKey?_eq_some_getKey h, getKey_eq_getKey!]
+
+theorem getKey!_eq_getKeyD_default [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
+    {a : α} : getKey! a l = getKeyD a l default := rfl
+
 /-- Internal implementation detail of the hash map -/
 def replaceEntry [BEq α] (k : α) (v : β k) : List ((a : α) × β a) → List ((a : α) × β a)
   | [] => []
@@ -643,6 +748,18 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α)
     · rw [Option.dmap_congr (getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h)),
         getValueCast?_eq_getEntry?]
 
+theorem getKey?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
+    {v : β k} : getKey? a (replaceEntry k v l) =
+      if containsKey k l ∧ k == a then some k else getKey? a l := by
+  rw [getKey?_eq_getEntry?]
+  split
+  · next h => simp [getEntry?_replaceEntry_of_true h.1 h.2]
+  · next h =>
+    simp only [Decidable.not_and_iff_or_not_not] at h
+    rcases h with h|h
+    · rw [getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]
+    · rw [getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]
+
 @[simp]
 theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by
@@ -974,6 +1091,39 @@ theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : Lis
     {k : α} {fallback v : β} : getValueD k (insertEntry k v l) fallback = v := by
   simp [getValueD_insertEntry, BEq.refl]
 
+theorem getKey?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
+    {v : β k} : getKey? a (insertEntry k v l) = if k == a then some k else getKey? a l := by
+  cases hl : containsKey k l
+  · simp [insertEntry_of_containsKey_eq_false hl]
+  · rw [insertEntry_of_containsKey hl, getKey?_replaceEntry, hl]
+    split <;> simp_all
+
+theorem getKey?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
+    {v : β k} : getKey? k (insertEntry k v l) = some k := by
+  simp [getKey?_insertEntry]
+
+theorem getKey?_eq_none [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α}
+    (h : containsKey a l = false) : getKey? a l = none := by
+  rwa [← Option.not_isSome_iff_eq_none, ← containsKey_eq_isSome_getKey?, Bool.not_eq_true]
+
+theorem getKey!_insertEntry [BEq α] [EquivBEq α] [Inhabited α]  {l : List ((a : α) × β a)}
+    {k a : α} {v : β k} : getKey! a (insertEntry k v l) =
+      if k == a then k else getKey! a l := by
+  simp [getKey!_eq_getKey?, getKey?_insertEntry, apply_ite Option.get!]
+
+theorem getKey!_insertEntry_self [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
+    {k : α} {v : β k} : getKey! k (insertEntry k v l) = k := by
+  rw [getKey!_insertEntry, if_pos BEq.refl]
+
+theorem getKeyD_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
+    {v : β k} : getKeyD a (insertEntry k v l) fallback =
+      if k == a then k else getKeyD a l fallback := by
+  simp [getKeyD_eq_getKey?, getKey?_insertEntry, apply_ite (fun x => Option.getD x fallback)]
+
+theorem getKeyD_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k fallback : α}
+    {v : β k} : getKeyD k (insertEntry k v l) fallback = k := by
+  rw [getKeyD_insertEntry, if_pos BEq.refl]
+
 @[local simp]
 theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : containsKey a (insertEntry k v l) = ((k == a) || containsKey a l) := by
@@ -1017,6 +1167,17 @@ theorem getValue_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List
     {v : β} : getValue k (insertEntry k v l) containsKey_insertEntry_self = v := by
   simp [getValue_insertEntry]
 
+theorem getKey_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α}
+    {v : β k} {h} : getKey a (insertEntry k v l) h =
+    if h' : k == a then k
+    else getKey a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, apply_dite Option.some, getKey?_insertEntry]
+  simp only [← getKey?_eq_some_getKey, dite_eq_ite]
+
+theorem getKey_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
+    {v : β k} : getKey k (insertEntry k v l) containsKey_insertEntry_self = k := by
+  simp [getKey_insertEntry]
+
 /-- Internal implementation detail of the hash map -/
 def insertEntryIfNew [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : List ((a : α) × β a) :=
   bif containsKey k l then l else ⟨k, v⟩ :: l
@@ -1135,6 +1296,32 @@ theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {
   simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
     apply_ite (fun x => Option.getD x fallback)]
 
+theorem getKey?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
+    {v : β k} : getKey? a (insertEntryIfNew k v l) =
+      if k == a ∧ containsKey k l = false then some k else getKey? a l := by
+  cases h : containsKey k l
+  · rw [insertEntryIfNew_of_containsKey_eq_false h]
+    split <;> simp_all
+  · simp [insertEntryIfNew_of_containsKey h]
+
+theorem getKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
+    {k a : α} {v : β k} {h} : getKey a (insertEntryIfNew k v l) h =
+    if h' : k == a ∧ containsKey k l = false then k
+    else getKey a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, apply_dite Option.some,
+    getKey?_insertEntryIfNew, ← dite_eq_ite]
+  simp [← getKey?_eq_some_getKey]
+
+theorem getKey!_insertEntryIfNew [BEq α] [PartialEquivBEq α] [Inhabited α]
+    {l : List ((a : α) × β a)} {k a : α} {v : β k} : getKey! a (insertEntryIfNew k v l) =
+      if k == a ∧ containsKey k l = false then k else getKey! a l := by
+  simp [getKey!_eq_getKey?, getKey?_insertEntryIfNew, apply_ite Option.get!]
+
+theorem getKeyD_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
+    {k a fallback : α} {v : β k} : getKeyD a (insertEntryIfNew k v l) fallback =
+      if k == a ∧ containsKey k l = false then k else getKeyD a l fallback := by
+  simp [getKeyD_eq_getKey?, getKey?_insertEntryIfNew, apply_ite (fun x => Option.getD x fallback)]
+
 theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
     (insertEntryIfNew k v l).length = if containsKey k l then l.length else l.length + 1 := by
   simp [insertEntryIfNew, Bool.apply_cond List.length]
@@ -1253,6 +1440,36 @@ theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) ×
 
 end
 
+theorem getKey?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
+    (hl : DistinctKeys l) :
+    getKey? a (eraseKey k l) = if k == a then none else getKey? a l := by
+  rw [getKey?_eq_getEntry?, getEntry?_eraseKey hl]
+  by_cases h : k == a
+  . simp [h]
+  . simp [h, getKey?_eq_getEntry?]
+
+theorem getKey?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
+    (hl : DistinctKeys l) : getKey? k (eraseKey k l) = none := by
+  simp [getKey?_eq_getEntry?, getEntry?_eraseKey_self hl]
+
+theorem getKey!_eraseKey [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
+    {k a : α} (hl : DistinctKeys l) :
+    getKey! a (eraseKey k l) = if k == a then default else getKey! a l := by
+  simp [getKey!_eq_getKey?, getKey?_eraseKey hl, apply_ite Option.get!]
+
+theorem getKey!_eraseKey_self [BEq α] [PartialEquivBEq α] [Inhabited α]  {l : List ((a : α) × β a)}
+    {k : α} (hl : DistinctKeys l) : getKey! k (eraseKey k l) = default := by
+  simp [getKey!_eq_getKey?, getKey?_eraseKey_self hl]
+
+theorem getKeyD_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
+    (hl : DistinctKeys l) :
+    getKeyD a (eraseKey k l) fallback = if k == a then fallback else getKeyD a l fallback := by
+  simp [getKeyD_eq_getKey?, getKey?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)]
+
+theorem getKeyD_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
+    {k fallback : α} (hl : DistinctKeys l) : getKeyD k (eraseKey k l) fallback = fallback := by
+  simp [getKeyD_eq_getKey?, getKey?_eraseKey_self hl]
+
 theorem containsKey_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
     (h : DistinctKeys l) : containsKey k (eraseKey k l) = false := by
   simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_self h]
@@ -1340,6 +1557,13 @@ theorem getValue_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1]
   simp [← getValue?_eq_some_getValue]
 
+theorem getKey_eraseKey [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α} {h}
+    (hl : DistinctKeys l) : getKey a (eraseKey k l) h =
+      getKey a l (containsKey_of_containsKey_eraseKey hl h) := by
+  rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, getKey?_eraseKey hl, h.1]
+  simp [← getKey?_eq_some_getKey]
+
 theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
     (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by
   induction h
@@ -1412,6 +1636,26 @@ theorem getValueD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α)
 
 end
 
+theorem getKey?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
+    (hl : DistinctKeys l) (h : Perm l l') : getKey? a l = getKey? a l' := by
+  rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?, getEntry?_of_perm hl h]
+
+theorem getKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {h'}
+    (hl : DistinctKeys l) (h : Perm l l') :
+    getKey a l h' = getKey a l' ((containsKey_of_perm h).symm.trans h') := by
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
+    getKey?_of_perm hl h]
+
+theorem getKey!_of_perm [BEq α] [PartialEquivBEq α] [Inhabited α] {l l' : List ((a : α) × β a)}
+    {a : α} (hl : DistinctKeys l) (h : Perm l l') :
+    getKey! a l = getKey! a l' := by
+  simp only [getKey!_eq_getKey?, getKey?_of_perm hl h]
+
+theorem getKeyD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a fallback : α}
+    (hl : DistinctKeys l) (h : Perm l l') :
+    getKeyD a l fallback = getKeyD a l' fallback := by
+  simp only [getKeyD_eq_getKey?, getKey?_of_perm hl h]
+
 theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
     ∃ l', Perm l (getEntry a l h :: l') := by
   induction l using assoc_induction
@@ -1521,6 +1765,18 @@ theorem getValueCast_append_of_containsKey_eq_false [BEq α] [LawfulBEq α]
   rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast,
     getValueCast?_append_of_containsKey_eq_false hl']
 
+theorem getKey?_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
+    {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
+    getKey? a (l ++ l') = getKey? a l := by
+  simp [getKey?_eq_getEntry?, getEntry?_eq_none.2 hl']
+
+theorem getKey_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
+    {l l' : List ((a : α) × β a)} {a : α} {h} (hl' : containsKey a l' = false) :
+    getKey a (l ++ l') h =
+      getKey a l ((containsKey_append_of_not_contains_right hl').symm.trans h) := by
+  rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
+    getKey?_append_of_containsKey_eq_false hl']
+
 theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α) × β a)} {k : α}
     {v : β k} (h : containsKey k l) : replaceEntry k v (l ++ l') = replaceEntry k v l ++ l' := by
   induction l using assoc_induction

src/Std/Data/DHashMap/Internal/Model.lean

@@ -262,6 +262,10 @@ def consₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : Raw
 def get?ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option (β a) :=
   (bucket m.1.buckets m.2 a).getCast? a
 
+/-- Internal implementation detail of the hash map -/
+def getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Option α :=
+  (bucket m.1.buckets m.2 a).getKey? a
+
 /-- Internal implementation detail of the hash map -/
 def containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Bool :=
   (bucket m.1.buckets m.2 a).contains a
@@ -278,6 +282,18 @@ def getDₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) (f
 def get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β) (a : α) [Inhabited (β a)] : β a :=
   (m.get?ₘ a).get!
 
+/-- Internal implementation detail of the hash map -/
+def getKeyₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.containsₘ a) : α :=
+  (bucket m.1.buckets m.2 a).getKey a h
+
+/-- Internal implementation detail of the hash map -/
+def getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (fallback : α) : α :=
+  (m.getKey?ₘ a).getD fallback
+
+/-- Internal implementation detail of the hash map -/
+def getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) : α :=
+  (m.getKey?ₘ a).get!
+
 /-- Internal implementation detail of the hash map -/
 def insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : Raw₀ α β :=
   if m.containsₘ a then m.replaceₘ a b else Raw₀.expandIfNecessary (m.consₘ a b)
@@ -348,6 +364,20 @@ theorem get!_eq_get!ₘ [BEq α] [LawfulBEq α] [Hashable α] (m : Raw₀ α β)
     get! m a = get!ₘ m a := by
   simp [get!, get!ₘ, get?ₘ, List.getValueCast!_eq_getValueCast?, bucket]
 
+theorem getKey?_eq_getKey?ₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
+    getKey? m a = getKey?ₘ m a := rfl
+
+theorem getKey_eq_getKeyₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (h : m.contains a) :
+    getKey m a h = getKeyₘ m a h := rfl
+
+theorem getKeyD_eq_getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a fallback : α) :
+    getKeyD m a fallback = getKeyDₘ m a fallback := by
+  simp [getKeyD, getKeyDₘ, getKey?ₘ, List.getKeyD_eq_getKey?, bucket]
+
+theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) :
+    getKey! m a = getKey!ₘ m a := by
+  simp [getKey!, getKey!ₘ, getKey?ₘ, List.getKey!_eq_getKey?, bucket]
+
 theorem contains_eq_containsₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
     m.contains a = m.containsₘ a := rfl
 

src/Std/Data/DHashMap/Internal/Raw.lean

@@ -135,6 +135,37 @@ theorem get!_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a :
     m.val.get! a = m.get! a := by
   simp [Raw.get!, m.2]
 
+theorem getKey?_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
+    m.getKey? a = Raw₀.getKey? ⟨m, h.size_buckets_pos⟩ a := by
+  simp [Raw.getKey?, h.size_buckets_pos]
+
+theorem getKey?_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} :
+    m.val.getKey? a = m.getKey? a := by
+  simp [Raw.getKey?, m.2]
+
+theorem getKey_eq [BEq α] [Hashable α] {m : Raw α β} {a : α} {h : a ∈ m} :
+    m.getKey a h = Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
+      (by change dite .. = true at h; split at h <;> simp_all) := rfl
+
+theorem getKey_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {h : a ∈ m.val}  :
+    m.val.getKey a h = m.getKey a (contains_val (m := m) ▸ h) := rfl
+
+theorem getKeyD_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} :
+    m.getKeyD a fallback = Raw₀.getKeyD ⟨m, h.size_buckets_pos⟩ a fallback := by
+  simp [Raw.getKeyD, h.size_buckets_pos]
+
+theorem getKeyD_val [BEq α] [Hashable α] {m : Raw₀ α β} {a fallback : α} :
+    m.val.getKeyD a fallback = m.getKeyD a fallback := by
+  simp [Raw.getKeyD, m.2]
+
+theorem getKey!_eq [BEq α] [Hashable α] [Inhabited α] {m : Raw α β} (h : m.WF) {a : α} :
+    m.getKey! a = Raw₀.getKey! ⟨m, h.size_buckets_pos⟩ a := by
+  simp [Raw.getKey!, h.size_buckets_pos]
+
+theorem getKey!_val [BEq α] [Hashable α] [Inhabited α] {m : Raw₀ α β} {a : α} :
+    m.val.getKey! a = m.getKey! a := by
+  simp [Raw.getKey!, m.2]
+
 theorem erase_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
     m.erase a = Raw₀.erase ⟨m, h.size_buckets_pos⟩ a := by
   simp [Raw.erase, h.size_buckets_pos]

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -83,7 +83,8 @@ private def queryNames : Array Name :=
   #[``contains_eq_containsKey, ``Raw.isEmpty_eq_isEmpty, ``Raw.size_eq_length,
     ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?, ``get_eq_getValueCast,
     ``Const.get_eq_getValue, ``get!_eq_getValueCast!, ``getD_eq_getValueCastD,
-    ``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD]
+    ``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?,
+    ``getKey_eq_getKey, ``getKeyD_eq_getKeyD, ``getKey!_eq_getKey!]
 
 private def modifyNames : Array Name :=
   #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew]
@@ -93,7 +94,8 @@ private def congrNames : MacroM (Array (TSyntax `term)) := do
     ← `(_root_.List.Perm.length_eq), ← `(getValueCast?_of_perm _),
     ← `(getValue?_of_perm _), ← `(getValue_of_perm _), ← `(getValueCast_of_perm _),
     ← `(getValueCast!_of_perm _), ← `(getValueCastD_of_perm _), ← `(getValue!_of_perm _),
-    ← `(getValueD_of_perm _) ]
+    ← `(getValueD_of_perm _), ← `(getKey?_of_perm _), ← `(getKey_of_perm _), ← `(getKeyD_of_perm _),
+    ← `(getKey!_of_perm _)]
 
 /-- Internal implementation detail of the hash map -/
 scoped syntax "simp_to_model" ("using" term)? : tactic
@@ -535,6 +537,147 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} {fa
 
 end Const
 
+@[simp]
+theorem getKey?_empty {a : α} {c} : (empty c : Raw₀ α β).getKey? a = none := by
+  simp [getKey?]
+
+theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
+    m.1.isEmpty = true → m.getKey? a = none := by
+  simp_to_model; empty
+
+theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a k : α} {v : β k} :
+    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a := by
+  simp_to_model using List.getKey?_insertEntry
+
+theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
+    (m.insert k v).getKey? k = some k := by
+  simp_to_model using List.getKey?_insertEntry_self
+
+theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
+    m.contains a = (m.getKey? a).isSome := by
+  simp_to_model using List.containsKey_eq_isSome_getKey?
+
+theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
+    m.contains a = false → m.getKey? a = none := by
+  simp_to_model using List.getKey?_eq_none
+
+theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
+    (m.erase k).getKey? a = if k == a then none else m.getKey? a := by
+  simp_to_model using List.getKey?_eraseKey
+
+theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+    (m.erase k).getKey? k = none := by
+  simp_to_model using List.getKey?_eraseKey_self
+
+theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then
+        k
+      else
+        m.getKey a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
+  simp_to_model using List.getKey_insertEntry
+
+theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
+    (m.insert k v).getKey k (contains_insert_self _ h) = k := by
+  simp_to_model using List.getKey_insertEntry_self
+
+@[simp]
+theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {h'} :
+    (m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h') := by
+  simp_to_model using List.getKey_eraseKey
+
+theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} :
+    m.getKey? a = some (m.getKey a h) := by
+  simp_to_model using List.getKey?_eq_some_getKey
+
+theorem getKey!_empty {a : α} [Inhabited α] {c} :
+    (empty c : Raw₀ α β).getKey! a = default := by
+  simp [getKey!, empty]
+
+theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
+    m.1.isEmpty = true → m.getKey! a = default := by
+  simp_to_model; empty;
+
+theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
+    {v : β k} :
+    (m.insert k v).getKey! a = if k == a then k else m.getKey! a := by
+  simp_to_model using List.getKey!_insertEntry
+
+theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α}
+    {b : β a} : (m.insert a b).getKey! a = a := by
+  simp_to_model using List.getKey!_insertEntry_self
+
+theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
+    m.contains a = false → m.getKey! a = default := by
+  simp_to_model using List.getKey!_eq_default
+
+theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α} :
+    (m.erase k).getKey! a = if k == a then default else m.getKey! a := by
+  simp_to_model using List.getKey!_eraseKey
+
+theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k : α} :
+    (m.erase k).getKey! k = default := by
+  simp_to_model using List.getKey!_eraseKey_self
+
+theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
+    m.contains a = true → m.getKey? a = some (m.getKey! a) := by
+  simp_to_model using List.getKey?_eq_some_getKey!
+
+theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
+    m.getKey! a = (m.getKey? a).get! := by
+  simp_to_model using List.getKey!_eq_getKey?
+
+theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} {h} :
+    m.getKey a h = m.getKey! a := by
+  simp_to_model using List.getKey_eq_getKey!
+
+theorem getKeyD_empty {a : α} {fallback : α} {c} :
+    (empty c : Raw₀ α β).getKeyD a fallback = fallback := by
+  simp [getKeyD, empty]
+
+theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
+    m.1.isEmpty = true → m.getKeyD a fallback = fallback := by
+  simp_to_model; empty
+
+theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} {v : β k} :
+    (m.insert k v).getKeyD a fallback =
+      if k == a then k else m.getKeyD a fallback := by
+  simp_to_model using List.getKeyD_insertEntry
+
+theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α}
+    {b : β a} :
+    (m.insert a b).getKeyD a fallback = a := by
+  simp_to_model using List.getKeyD_insertEntry_self
+
+theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
+    m.contains a = false → m.getKeyD a fallback = fallback := by
+  simp_to_model using List.getKeyD_eq_fallback
+
+theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} :
+    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback := by
+  simp_to_model using List.getKeyD_eraseKey
+
+theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k fallback : α} :
+    (m.erase k).getKeyD k fallback = fallback := by
+  simp_to_model using List.getKeyD_eraseKey_self
+
+theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
+    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback) := by
+  simp_to_model using List.getKey?_eq_some_getKeyD
+
+theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
+    m.getKeyD a fallback = (m.getKey? a).getD fallback := by
+  simp_to_model using List.getKeyD_eq_getKey?
+
+theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} {h} :
+    m.getKey a h = m.getKeyD a fallback := by
+  simp_to_model using List.getKey_eq_getKeyD
+
+theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
+    {a : α} :
+    m.getKey! a = m.getKeyD a default := by
+  simp_to_model using List.getKey!_eq_getKeyD_default
+
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).1.isEmpty = false := by
   simp_to_model using List.isEmpty_insertEntryIfNew
@@ -620,6 +763,29 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a :
 
 end Const
 
+theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
+    (m.insertIfNew k v).getKey? a =
+      if k == a ∧ m.contains k = false then some k else m.getKey? a := by
+  simp_to_model using List.getKey?_insertEntryIfNew
+
+theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
+    (m.insertIfNew k v).getKey a h₁ =
+      if h₂ : k == a ∧ m.contains k = false then k
+      else m.getKey a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
+  simp_to_model using List.getKey_insertEntryIfNew
+
+theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {k a : α}
+    {v : β k} :
+    (m.insertIfNew k v).getKey! a =
+      if k == a ∧ m.contains k = false then k else m.getKey! a := by
+  simp_to_model using List.getKey!_insertEntryIfNew
+
+theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α}
+    {v : β k} :
+    (m.insertIfNew k v).getKeyD a fallback =
+      if k == a ∧ m.contains k = false then k else m.getKeyD a fallback := by
+  simp_to_model using List.getKeyD_insertEntryIfNew
+
 @[simp]
 theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).1 = m.get? k := by

src/Std/Data/DHashMap/Internal/WF.lean

@@ -233,6 +233,47 @@ theorem getD_eq_getValueCastD [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀
     m.getD a fallback = getValueCastD a (toListModel m.1.buckets) fallback := by
   rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hm]
 
+theorem getKey?ₘ_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a : α} :
+    m.getKey?ₘ a = List.getKey? a (toListModel m.1.buckets) :=
+  apply_bucket hm AssocList.getKey?_eq List.getKey?_of_perm List.getKey?_append_of_containsKey_eq_false
+
+theorem getKey?_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a : α} :
+    m.getKey? a = List.getKey? a (toListModel m.1.buckets) := by
+  rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hm]
+
+theorem getKeyₘ_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
+    m.getKeyₘ a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) :=
+  apply_bucket_with_proof hm a AssocList.getKey List.getKey AssocList.getKey_eq
+    List.getKey_of_perm List.getKey_append_of_containsKey_eq_false
+
+theorem getKey_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
+    m.getKey a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h) := by
+  rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey hm]
+
+theorem getKey!ₘ_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
+    m.getKey!ₘ a = List.getKey! a (toListModel m.1.buckets) := by
+  rw [getKey!ₘ, getKey?ₘ_eq_getKey? hm, List.getKey!_eq_getKey?]
+
+theorem getKey!_eq_getKey! [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
+    m.getKey! a = List.getKey! a (toListModel m.1.buckets) := by
+  rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hm]
+
+theorem getKeyDₘ_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a fallback : α} :
+    m.getKeyDₘ a fallback = List.getKeyD a (toListModel m.1.buckets) fallback := by
+  rw [getKeyDₘ, getKey?ₘ_eq_getKey? hm, List.getKeyD_eq_getKey?]
+
+theorem getKeyD_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
+    (hm : Raw.WFImp m.1) {a fallback : α} :
+    m.getKeyD a fallback = List.getKeyD a (toListModel m.1.buckets) fallback := by
+  rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hm]
+
 section
 
 variable {β : Type v}

src/Std/Data/DHashMap/Lemmas.lean

@@ -599,6 +599,189 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
 
 end Const
 
+@[simp]
+theorem getKey?_empty {a : α} {c} : (empty c : DHashMap α β).getKey? a = none :=
+  Raw₀.getKey?_empty
+
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : DHashMap α β).getKey? a = none :=
+  Raw₀.getKey?_empty
+
+theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty = true → m.getKey? a = none :=
+  Raw₀.getKey?_of_isEmpty ⟨m.1, _⟩ m.2
+
+theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
+    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
+  Raw₀.getKey?_insert ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insert k v).getKey? k = some k :=
+  Raw₀.getKey?_insert_self ⟨m.1, _⟩ m.2
+
+theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = (m.getKey? a).isSome :=
+  Raw₀.contains_eq_isSome_getKey? ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = false → m.getKey? a = none :=
+  Raw₀.getKey?_eq_none ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.getKey? a = none := by
+  simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false
+
+theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.erase k).getKey? a = if k == a then none else m.getKey? a :=
+  Raw₀.getKey?_erase ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
+  Raw₀.getKey?_erase_self ⟨m.1, _⟩ m.2
+
+theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then
+        k
+      else
+        m.getKey a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
+  Raw₀.getKey_insert ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insert k v).getKey k mem_insert_self = k :=
+  Raw₀.getKey_insert_self ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
+    (m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h') :=
+  Raw₀.getKey_erase ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α}
+    {h} :
+    m.getKey? a = some (m.getKey a h) :=
+  Raw₀.getKey?_eq_some_getKey ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey!_empty [Inhabited α] {a : α} {c} :
+    (empty c : DHashMap α β).getKey! a = default :=
+  Raw₀.getKey!_empty
+
+@[simp]
+theorem getKey!_emptyc [Inhabited α] {a : α} :
+    (∅ : DHashMap α β).getKey! a = default :=
+  getKey!_empty
+
+theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.isEmpty = true → m.getKey! a = default :=
+  Raw₀.getKey!_of_isEmpty ⟨m.1, _⟩ m.2
+
+theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
+    (m.insert k v).getKey! a =
+      if k == a then k else m.getKey! a :=
+  Raw₀.getKey!_insert ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {b : β a} :
+    (m.insert a b).getKey! a = a :=
+  Raw₀.getKey!_insert_self ⟨m.1, _⟩ m.2
+
+theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {a : α} :
+    m.contains a = false → m.getKey! a = default :=
+  Raw₀.getKey!_eq_default ⟨m.1, _⟩ m.2
+
+theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    ¬a ∈ m → m.getKey! a = default := by
+  simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false
+
+theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
+    (m.erase k).getKey! a = if k == a then default else m.getKey! a :=
+  Raw₀.getKey!_erase ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
+    (m.erase k).getKey! k = default :=
+  Raw₀.getKey!_erase_self ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.contains a = true → m.getKey? a = some (m.getKey! a) :=
+  Raw₀.getKey?_eq_some_getKey! ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    a ∈ m → m.getKey? a = some (m.getKey! a) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains
+
+theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.getKey! a = (m.getKey? a).get! :=
+  Raw₀.getKey!_eq_get!_getKey? ⟨m.1, _⟩ m.2
+
+theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h} :
+    m.getKey a h = m.getKey! a :=
+  Raw₀.getKey_eq_getKey! ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKeyD_empty {a fallback : α} {c} :
+    (empty c : DHashMap α β).getKeyD a fallback = fallback :=
+  Raw₀.getKeyD_empty
+
+@[simp]
+theorem getKeyD_emptyc {a fallback : α} :
+    (∅ : DHashMap α β).getKeyD a fallback = fallback :=
+  getKeyD_empty
+
+theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.isEmpty = true → m.getKeyD a fallback = fallback :=
+  Raw₀.getKeyD_of_isEmpty ⟨m.1, _⟩ m.2
+
+theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
+    (m.insert k v).getKeyD a fallback =
+      if k == a then k else m.getKeyD a fallback :=
+  Raw₀.getKeyD_insert ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β k} :
+    (m.insert k v).getKeyD k fallback = k :=
+  Raw₀.getKeyD_insert_self ⟨m.1, _⟩ m.2
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
+    {fallback : α} :
+    m.contains a = false → m.getKeyD a fallback = fallback :=
+  Raw₀.getKeyD_eq_fallback ⟨m.1, _⟩ m.2
+
+theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    ¬a ∈ m → m.getKeyD a fallback = fallback := by
+  simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
+  Raw₀.getKeyD_erase ⟨m.1, _⟩ m.2
+
+@[simp]
+theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] {k fallback : α} :
+    (m.erase k).getKeyD k fallback = fallback :=
+  Raw₀.getKeyD_erase_self ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback) :=
+  Raw₀.getKey?_eq_some_getKeyD ⟨m.1, _⟩ m.2
+
+theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    a ∈ m → m.getKey? a = some (m.getKeyD a fallback) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains
+
+theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.getKeyD a fallback = (m.getKey? a).getD fallback :=
+  Raw₀.getKeyD_eq_getD_getKey? ⟨m.1, _⟩ m.2
+
+theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] {a fallback : α} {h} :
+    m.getKey a h = m.getKeyD a fallback :=
+  Raw₀.getKey_eq_getKeyD ⟨m.1, _⟩ m.2
+
+theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.getKey! a = m.getKeyD a default :=
+  Raw₀.getKey!_eq_getKeyD_default ⟨m.1, _⟩ m.2
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insertIfNew k v).isEmpty = false :=
@@ -706,6 +889,29 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback
 
 end Const
 
+theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
+    getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a := by
+  simp [mem_iff_contains, contains_insertIfNew]
+  exact Raw₀.getKey?_insertIfNew ⟨m.1, _⟩ m.2
+
+theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
+    getKey (m.insertIfNew k v) a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) := by
+  simp [mem_iff_contains, contains_insertIfNew]
+  exact Raw₀.getKey_insertIfNew ⟨m.1, _⟩ m.2
+
+theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
+    getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a := by
+  simp [mem_iff_contains, contains_insertIfNew]
+  exact Raw₀.getKey!_insertIfNew ⟨m.1, _⟩ m.2
+
+theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
+    getKeyD (m.insertIfNew k v) a fallback =
+      if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback := by
+  simp [mem_iff_contains, contains_insertIfNew]
+  exact Raw₀.getKeyD_insertIfNew ⟨m.1, _⟩ m.2
+
+
 @[simp]
 theorem getThenInsertIfNew?_fst [LawfulBEq α] {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).1 = m.get? k :=

src/Std/Data/DHashMap/Raw.lean

@@ -237,6 +237,41 @@ returned map has a new value inserted.
 
 end
 
+/--
+Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
+The result in the `some` case is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) : Option α :=
+  if h : 0 < m.buckets.size then
+    Raw₀.getKey? ⟨m, h⟩ a
+  else none -- will never happen for well-formed inputs
+
+/--
+Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
+requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α) (h : a ∈ m) : α :=
+  Raw₀.getKey ⟨m, by change dite .. = true at h; split at h <;> simp_all⟩ a
+    (by change dite .. = true at h; split at h <;> simp_all)
+
+/--
+Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
+If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α) (fallback : α) : α :=
+  if h : 0 < m.buckets.size then
+    Raw₀.getKeyD ⟨m, h⟩ a fallback
+  else fallback -- will never happen for well-formed inputs
+
+/--
+Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
+If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline] def getKey! [BEq α] [Hashable α] [Inhabited α] (m : Raw α β) (a : α) : α :=
+  if h : 0 < m.buckets.size then
+    Raw₀.getKey! ⟨m, h⟩ a
+  else default -- will never happen for well-formed inputs
+
 /--
 Returns `true` if the hash map contains no mappings.
 

src/Std/Data/DHashMap/RawLemmas.lean

@@ -54,7 +54,11 @@ private def baseNames : Array Name :=
     ``contains_eq, ``contains_val,
     ``get_eq, ``get_val,
     ``getD_eq, ``getD_val,
-    ``get!_eq, ``get!_val]
+    ``get!_eq, ``get!_val,
+    ``getKey?_eq, ``getKey?_val,
+    ``getKey_eq, ``getKey_val,
+    ``getKey!_eq, ``getKey!_val,
+    ``getKeyD_eq, ``getKeyD_val]
 
 /-- Internal implementation detail of the hash map -/
 scoped syntax "simp_to_raw" ("using" term)? : tactic
@@ -661,6 +665,194 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
 
 end Const
 
+@[simp]
+theorem getKey?_empty {a : α} {c} :
+    (empty c : Raw α β).getKey? a = none := by
+  simp_to_raw using Raw₀.getKey?_empty
+
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none :=
+  getKey?_empty
+
+theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.getKey? a = none := by
+  simp_to_raw using Raw₀.getKey?_of_isEmpty ⟨m, _⟩
+
+theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
+    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a := by
+  simp_to_raw using Raw₀.getKey?_insert
+
+@[simp]
+theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
+    (m.insert k v).getKey? k = some k := by
+  simp_to_raw using Raw₀.getKey?_insert_self
+
+theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = (m.getKey? a).isSome := by
+  simp_to_raw using Raw₀.contains_eq_isSome_getKey?
+
+theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = false → m.getKey? a = none := by
+  simp_to_raw using Raw₀.getKey?_eq_none
+
+theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    ¬a ∈ m → m.getKey? a = none := by
+  simpa [mem_iff_contains] using getKey?_eq_none_of_contains_eq_false h
+
+theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.erase k).getKey? a = if k == a then none else m.getKey? a := by
+  simp_to_raw using Raw₀.getKey?_erase
+
+@[simp]
+theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.erase k).getKey? k = none := by
+  simp_to_raw using Raw₀.getKey?_erase_self
+
+theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then
+        k
+      else
+        m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
+  simp_to_raw using Raw₀.getKey_insert ⟨m, _⟩
+
+@[simp]
+theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
+    (m.insert k v).getKey k (mem_insert_self h) = k := by
+  simp_to_raw using Raw₀.getKey_insert_self ⟨m, _⟩
+
+@[simp]
+theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
+    (m.erase a).getKey k h' = m.getKey k (mem_of_mem_erase h h') := by
+  simp_to_raw using Raw₀.getKey_erase ⟨m, _⟩
+
+theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h} :
+    m.getKey? a = some (m.getKey a h) := by
+  simp_to_raw using Raw₀.getKey?_eq_some_getKey
+
+@[simp]
+theorem getKey!_empty [Inhabited α] {a : α} {c} :
+    (empty c : Raw α β).getKey! a = default := by
+  simp_to_raw using Raw₀.getKey!_empty
+
+@[simp]
+theorem getKey!_emptyc [Inhabited α] {a : α} :
+    (∅ : Raw α β).getKey! a = default :=
+  getKey!_empty
+
+theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.getKey! a = default := by
+  simp_to_raw using Raw₀.getKey!_of_isEmpty ⟨m, _⟩
+
+theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β k} :
+    (m.insert k v).getKey! a = if k == a then k else m.getKey! a := by
+  simp_to_raw using Raw₀.getKey!_insert
+
+@[simp]
+theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α}
+    {v : β k} :
+    (m.insert k v).getKey! k = k := by
+  simp_to_raw using Raw₀.getKey!_insert_self
+
+theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    (h : m.WF) {a : α} :
+    m.contains a = false → m.getKey! a = default := by
+  simp_to_raw using Raw₀.getKey!_eq_default
+
+theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α}:
+    ¬a ∈ m → m.getKey! a = default := by
+  simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false h
+
+theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
+    (m.erase k).getKey! a = if k == a then default else m.getKey! a := by
+  simp_to_raw using Raw₀.getKey!_erase
+
+@[simp]
+theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} :
+    (m.erase k).getKey! k = default := by
+  simp_to_raw using Raw₀.getKey!_erase_self
+
+theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
+    {a : α} :
+    m.contains a = true → m.getKey? a = some (m.getKey! a) := by
+  simp_to_raw using Raw₀.getKey?_eq_some_getKey!
+
+theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    a ∈ m → m.getKey? a = some (m.getKey! a) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains h
+
+theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    m.getKey! a = (m.getKey? a).get! := by
+  simp_to_raw using Raw₀.getKey!_eq_get!_getKey?
+
+theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h} :
+    m.getKey a h = m.getKey! a := by
+  simp_to_raw using Raw₀.getKey_eq_getKey!
+
+@[simp]
+theorem getKeyD_empty {a fallback : α} {c} :
+    (empty c : Raw α β).getKeyD a fallback = fallback := by
+  simp_to_raw using Raw₀.getKeyD_empty
+
+@[simp]
+theorem getKeyD_emptyc {a fallback : α} :
+    (∅ : Raw α β).getKeyD a fallback = fallback :=
+  getKeyD_empty
+
+theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    m.isEmpty = true → m.getKeyD a fallback = fallback := by
+  simp_to_raw using Raw₀.getKeyD_of_isEmpty ⟨m, _⟩
+
+theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β k} :
+    (m.insert k v).getKeyD a fallback =
+      if k == a then k else m.getKeyD a fallback := by
+  simp_to_raw using Raw₀.getKeyD_insert
+
+@[simp]
+theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {b : β a} :
+    (m.insert a b).getKeyD a fallback = a := by
+  simp_to_raw using Raw₀.getKeyD_insert_self
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {a fallback : α} :
+    m.contains a = false → m.getKeyD a fallback = fallback := by
+  simp_to_raw using Raw₀.getKeyD_eq_fallback
+
+theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    ¬a ∈ m → m.getKeyD a fallback = fallback := by
+  simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false h
+
+theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback := by
+  simp_to_raw using Raw₀.getKeyD_erase
+
+@[simp]
+theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
+    (m.erase k).getKeyD k fallback = fallback := by
+  simp_to_raw using Raw₀.getKeyD_erase_self
+
+theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {a fallback : α} :
+    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback) := by
+  simp_to_raw using Raw₀.getKey?_eq_some_getKeyD
+
+theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    a ∈ m → m.getKey? a = some (m.getKeyD a fallback) := by
+  simpa [mem_iff_contains] using getKey?_eq_some_getKeyD_of_contains h
+
+theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    m.getKeyD a fallback = (m.getKey? a).getD fallback := by
+  simp_to_raw using Raw₀.getKeyD_eq_getD_getKey?
+
+theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h} :
+    m.getKey a h = m.getKeyD a fallback := by
+  simp_to_raw using Raw₀.getKey_eq_getKeyD
+
+theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
+    {a : α} :
+    m.getKey! a = m.getKeyD a default := by
+  simp_to_raw using Raw₀.getKey!_eq_getKeyD_default
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).isEmpty = false := by
@@ -774,6 +966,30 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
 
 end Const
 
+theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
+    getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_raw using Raw₀.getKey?_insertIfNew
+
+theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
+    getKey (m.insertIfNew k v) a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h h₁ h₂) := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_raw using Raw₀.getKey_insertIfNew ⟨m, _⟩
+
+theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α}
+    {v : β k} :
+    getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_raw using Raw₀.getKey!_insertIfNew
+
+theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α}
+    {v : β k} :
+    getKeyD (m.insertIfNew k v) a fallback =
+      if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
+  simp_to_raw using Raw₀.getKeyD_insertIfNew
+
 @[simp]
 theorem getThenInsertIfNew?_fst [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).1 = m.get? k := by

src/Std/Data/HashMap/Basic.lean

@@ -160,6 +160,18 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a
   getElem? m a := m.get? a
   getElem! m a := m.get! a
 
+@[inline, inherit_doc DHashMap.getKey?] def getKey? (m : HashMap α β) (a : α) : Option α :=
+  DHashMap.getKey? m.inner a
+
+@[inline, inherit_doc DHashMap.getKey] def getKey (m : HashMap α β) (a : α) (h : a ∈ m) : α :=
+  DHashMap.getKey m.inner a h
+
+@[inline, inherit_doc DHashMap.getKeyD] def getKeyD (m : HashMap α β) (a : α) (fallback : α) : α :=
+  DHashMap.getKeyD m.inner a fallback
+
+@[inline, inherit_doc DHashMap.getKey!] def getKey! [Inhabited α] (m : HashMap α β) (a : α) : α :=
+  DHashMap.getKey! m.inner a
+
 @[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
     HashMap α β :=
   ⟨m.inner.erase a⟩

src/Std/Data/HashMap/Lemmas.lean

@@ -391,6 +391,178 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
     m.getD a fallback = m.getD b fallback :=
   DHashMap.Const.getD_congr hab
 
+@[simp]
+theorem getKey?_empty {a : α} {c} : (empty c : HashMap α β).getKey? a = none :=
+  DHashMap.getKey?_empty
+
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : HashMap α β).getKey? a = none :=
+  DHashMap.getKey?_emptyc
+
+theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty = true → m.getKey? a = none :=
+  DHashMap.getKey?_of_isEmpty
+
+theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
+    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
+  DHashMap.getKey?_insert
+
+@[simp]
+theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insert k v).getKey? k = some k :=
+  DHashMap.getKey?_insert_self
+
+theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = (m.getKey? a).isSome :=
+  DHashMap.contains_eq_isSome_getKey?
+
+theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = false → m.getKey? a = none :=
+  DHashMap.getKey?_eq_none_of_contains_eq_false
+
+theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.getKey? a = none :=
+  DHashMap.getKey?_eq_none
+
+theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.erase k).getKey? a = if k == a then none else m.getKey? a :=
+  DHashMap.getKey?_erase
+
+@[simp]
+theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
+  DHashMap.getKey?_erase_self
+
+theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+    (m.insert k v)[a]'h₁ =
+      if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
+  DHashMap.Const.get_insert (h₁ := h₁)
+
+@[simp]
+theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insert k v).getKey k mem_insert_self = k :=
+  DHashMap.getKey_insert_self
+
+@[simp]
+theorem getKey_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
+    (m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h') :=
+  DHashMap.getKey_erase (h' := h')
+
+theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} :
+    m.getKey? a = some (m.getKey a h') :=
+  @DHashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
+
+@[simp]
+theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default :=
+  DHashMap.getKey!_empty
+
+@[simp]
+theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : HashMap α β).getKey! a = default :=
+  DHashMap.getKey!_emptyc
+
+theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.isEmpty = true → m.getKey! a = default :=
+  DHashMap.getKey!_of_isEmpty
+
+theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
+    (m.insert k v).getKey! a = if k == a then k else m.getKey! a :=
+  DHashMap.getKey!_insert
+
+@[simp]
+theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {v : β} :
+    (m.insert k v).getKey! k = k :=
+  DHashMap.getKey!_insert_self
+
+theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {a : α} : m.contains a = false → m.getKey! a = default :=
+  DHashMap.getKey!_eq_default_of_contains_eq_false
+
+theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    ¬a ∈ m → m.getKey! a = default :=
+  DHashMap.getKey!_eq_default
+
+theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
+    (m.erase k).getKey! a = if k == a then default else m.getKey! a :=
+  DHashMap.getKey!_erase
+
+@[simp]
+theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
+    (m.erase k).getKey! k = default :=
+  DHashMap.getKey!_erase_self
+
+theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {a : α} : m.contains a = true → m.getKey? a = some (m.getKey! a) :=
+  DHashMap.getKey?_eq_some_getKey!_of_contains
+
+theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    a ∈ m → m.getKey? a = some (m.getKey! a) :=
+  DHashMap.getKey?_eq_some_getKey!
+
+theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.getKey! a = (m.getKey? a).get! :=
+  DHashMap.getKey!_eq_get!_getKey?
+
+theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h'} :
+    m.getKey a h' = m.getKey! a :=
+  @DHashMap.getKey_eq_getKey! _ _ _ _ _ _ _ _ _ h'
+
+@[simp]
+theorem getKeyD_empty {a : α} {fallback : α} {c} :
+    (empty c : HashMap α β).getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_empty
+
+@[simp]
+theorem getKeyD_emptyc {a : α} {fallback : α} : (∅ : HashMap α β).getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_empty
+
+theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
+    m.isEmpty = true → m.getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_of_isEmpty
+
+theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
+    (m.insert k v).getKeyD a fallback = if k == a then k else m.getKeyD a fallback :=
+  DHashMap.getKeyD_insert
+
+@[simp]
+theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β} :
+   (m.insert k v).getKeyD k fallback = k :=
+  DHashMap.getKeyD_insert_self
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α}
+    {fallback : α} : m.contains a = false → m.getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
+    ¬a ∈ m → m.getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_eq_fallback
+
+theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : α} :
+    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
+  DHashMap.getKeyD_erase
+
+@[simp]
+theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : α} :
+    (m.erase k).getKeyD k fallback = fallback :=
+  DHashMap.getKeyD_erase_self
+
+theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
+    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback) :=
+  DHashMap.getKey?_eq_some_getKeyD_of_contains
+
+theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
+    a ∈ m → m.getKey? a = some (m.getKeyD a fallback) :=
+  DHashMap.getKey?_eq_some_getKeyD
+
+theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
+    m.getKeyD a fallback = (m.getKey? a).getD fallback :=
+  DHashMap.getKeyD_eq_getD_getKey?
+
+theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} {h'} :
+    m.getKey a h' = m.getKeyD a fallback :=
+  @DHashMap.getKey_eq_getKeyD _ _ _ _ _ _ _ _ _ h'
+
+theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.getKey! a = m.getKeyD a default :=
+  DHashMap.getKey!_eq_getKeyD_default
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insertIfNew k v).isEmpty = false :=
@@ -464,6 +636,23 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback
       if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
   DHashMap.Const.getD_insertIfNew
 
+theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
+    getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a :=
+  DHashMap.getKey?_insertIfNew
+
+theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+    getKey (m.insertIfNew k v) a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) :=
+  DHashMap.getKey_insertIfNew
+
+theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
+    getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a :=
+  DHashMap.getKey!_insertIfNew
+
+theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
+    getKeyD (m.insertIfNew k v) a fallback = if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback :=
+  DHashMap.getKeyD_insertIfNew
+
 @[simp]
 theorem getThenInsertIfNew?_fst {k : α} {v : β} : (getThenInsertIfNew? m k v).1 = get? m k :=
   DHashMap.Const.getThenInsertIfNew?_fst

src/Std/Data/HashMap/Raw.lean

@@ -138,6 +138,22 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
   getElem? m a := m.get? a
   getElem! m a := m.get! a
 
+@[inline, inherit_doc DHashMap.Raw.getKey?] def getKey? [BEq α] [Hashable α] (m : Raw α β) (a : α) :
+    Option α :=
+  DHashMap.Raw.getKey? m.inner a
+
+@[inline, inherit_doc DHashMap.Raw.getKey] def getKey [BEq α] [Hashable α] (m : Raw α β) (a : α)
+    (h : a ∈ m) : α :=
+  DHashMap.Raw.getKey m.inner a h
+
+@[inline, inherit_doc DHashMap.Raw.getKeyD] def getKeyD [BEq α] [Hashable α] (m : Raw α β) (a : α)
+    (fallback : α) : α :=
+  DHashMap.Raw.getKeyD m.inner a fallback
+
+@[inline, inherit_doc DHashMap.Raw.getKey!] def getKey! [BEq α] [Hashable α] [Inhabited α]
+    (m : Raw α β) (a : α) : α :=
+  DHashMap.Raw.getKey! m.inner a
+
 @[inline, inherit_doc DHashMap.Raw.erase] def erase [BEq α] [Hashable α] (m : Raw α β)
     (a : α) : Raw α β :=
   ⟨m.inner.erase a⟩

src/Std/Data/HashMap/RawLemmas.lean

@@ -400,6 +400,181 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
     (hab : a == b) : m.getD a fallback = m.getD b fallback :=
   DHashMap.Raw.Const.getD_congr h.out hab
 
+@[simp]
+theorem getKey?_empty {a : α} {c} : (empty c : Raw α β).getKey? a = none :=
+  DHashMap.Raw.getKey?_empty
+
+@[simp]
+theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none :=
+  DHashMap.Raw.getKey?_emptyc
+
+theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.getKey? a = none :=
+  DHashMap.Raw.getKey?_of_isEmpty h.out
+
+theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
+    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
+  DHashMap.Raw.getKey?_insert h.out
+
+@[simp]
+theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
+    (m.insert k v).getKey? k = some k :=
+  DHashMap.Raw.getKey?_insert_self h.out
+
+theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = (m.getKey? a).isSome :=
+  DHashMap.Raw.contains_eq_isSome_getKey? h.out
+
+theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = false → m.getKey? a = none :=
+  DHashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out
+
+theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    ¬a ∈ m → m.getKey? a = none :=
+  DHashMap.Raw.getKey?_eq_none h.out
+
+theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.erase k).getKey? a = if k == a then none else m.getKey? a :=
+  DHashMap.Raw.getKey?_erase h.out
+
+@[simp]
+theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.erase k).getKey? k = none :=
+  DHashMap.Raw.getKey?_erase_self h.out
+
+theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then k else m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
+  DHashMap.Raw.getKey_insert (h₁ := h₁) h.out
+
+@[simp]
+theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
+    (m.insert k v).getKey k (mem_insert_self h) = k :=
+  DHashMap.Raw.getKey_insert_self h.out
+
+@[simp]
+theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
+    (m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h h') :=
+  DHashMap.Raw.getKey_erase (h' := h') h.out
+
+theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m} :
+    m.getKey? a = some (m.getKey a h') :=
+  @DHashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
+
+@[simp]
+theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default :=
+  DHashMap.Raw.getKey!_empty
+
+@[simp]
+theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default :=
+  DHashMap.Raw.getKey!_emptyc
+
+theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.getKey! a = default :=
+  DHashMap.Raw.getKey!_of_isEmpty h.out
+
+theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β} :
+    (m.insert k v).getKey! a = if k == a then k else m.getKey! a :=
+  DHashMap.Raw.getKey!_insert h.out
+
+@[simp]
+theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α}
+    {v : β} : (m.insert k v).getKey! k = k :=
+  DHashMap.Raw.getKey!_insert_self h.out
+
+theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    (h : m.WF) {a : α} : m.contains a = false → m.getKey! a = default :=
+  DHashMap.Raw.getKey!_eq_default_of_contains_eq_false h.out
+
+theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    ¬a ∈ m → m.getKey! a = default :=
+  DHashMap.Raw.getKey!_eq_default h.out
+
+theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} :
+    (m.erase k).getKey! a = if k == a then default else m.getKey! a :=
+  DHashMap.Raw.getKey!_erase h.out
+
+@[simp]
+theorem getKey!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} :
+    (m.erase k).getKey! k = default :=
+  DHashMap.Raw.getKey!_erase_self h.out
+
+theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    (h : m.WF) {a : α} : m.contains a = true → m.getKey? a = some (m.getKey! a) :=
+  DHashMap.Raw.getKey?_eq_some_getKey!_of_contains h.out
+
+theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    a ∈ m → m.getKey? a = some (m.getKey! a) :=
+  DHashMap.Raw.getKey?_eq_some_getKey! h.out
+
+theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    m.getKey! a = (m.getKey? a).get! :=
+  DHashMap.Raw.getKey!_eq_get!_getKey? h.out
+
+theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h'} :
+    m.getKey a h' = m.getKey! a :=
+  DHashMap.Raw.getKey_eq_getKey! h.out
+
+@[simp]
+theorem getKeyD_empty {a fallback : α} {c} :
+    (empty c : Raw α β).getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_empty
+
+@[simp]
+theorem getKeyD_emptyc {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_empty
+
+theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    m.isEmpty = true → m.getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_of_isEmpty h.out
+
+theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β} :
+    (m.insert k v).getKeyD a fallback = if k == a then k else m.getKeyD a fallback :=
+  DHashMap.Raw.getKeyD_insert h.out
+
+@[simp]
+theorem getKeyD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} {v : β} :
+   (m.insert k v).getKeyD k fallback = k :=
+  DHashMap.Raw.getKeyD_insert_self h.out
+
+theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {a fallback : α} : m.contains a = false → m.getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h.out
+
+theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    ¬a ∈ m → m.getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_eq_fallback h.out
+
+theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+    (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
+  DHashMap.Raw.getKeyD_erase h.out
+
+@[simp]
+theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
+    (m.erase k).getKeyD k fallback = fallback :=
+  DHashMap.Raw.getKeyD_erase_self h.out
+
+theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {a fallback : α} : m.contains a = true → m.getKey? a = some (m.getKeyD a fallback) :=
+  DHashMap.Raw.getKey?_eq_some_getKeyD_of_contains h.out
+
+theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    a ∈ m → m.getKey? a = some (m.getKeyD a fallback) :=
+  DHashMap.Raw.getKey?_eq_some_getKeyD h.out
+
+theorem getKeyD_eq_getD_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    m.getKeyD a fallback = (m.getKey? a).getD fallback :=
+  DHashMap.Raw.getKeyD_eq_getD_getKey? h.out
+
+theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h'} :
+    m.getKey a h' = m.getKeyD a fallback :=
+  @DHashMap.Raw.getKey_eq_getKeyD _ _ _ _ _ _ _ h.out _ _ h'
+
+theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
+    {a : α} :
+    m.getKey! a = m.getKeyD a default :=
+  DHashMap.Raw.getKey!_eq_getKeyD_default h.out
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
     (m.insertIfNew k v).isEmpty = false :=
@@ -473,6 +648,24 @@ theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
       if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
   DHashMap.Raw.Const.getD_insertIfNew h.out
 
+theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} :
+    (m.insertIfNew k v).getKey? a = if k == a ∧ ¬k ∈ m then some k else m.getKey? a :=
+  DHashMap.Raw.getKey?_insertIfNew h.out
+
+theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
+    (m.insertIfNew k v).getKey a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else m.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) :=
+  DHashMap.Raw.getKey_insertIfNew h.out
+
+theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k a : α} {v : β} :
+    (m.insertIfNew k v).getKey! a = if k == a ∧ ¬k ∈ m then k else m.getKey! a :=
+  DHashMap.Raw.getKey!_insertIfNew h.out
+
+theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} {v : β} :
+    (m.insertIfNew k v).getKeyD a fallback = if k == a ∧ ¬k ∈ m then k else m.getKeyD a fallback :=
+  DHashMap.Raw.getKeyD_insertIfNew h.out
+
+
 @[simp]
 theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
     (getThenInsertIfNew? m k v).1 = get? m k :=

src/Std/Data/HashSet/Basic.lean

@@ -112,6 +112,34 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
 @[inline] def size (m : HashSet α) : Nat :=
   m.inner.size
 
+/--
+Checks if given key is contained and returns the key if it is, otherwise `none`.
+The result in the `some` case is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def get? (m : HashSet α) (a : α) : Option α :=
+  m.inner.getKey? a
+
+/--
+Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
+of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def get [BEq α] [Hashable α] (m : HashSet α) (a : α) (h : a ∈ m) : α :=
+  m.inner.getKey a h
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise `fallback`.
+If they key is contained the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def getD [BEq α] [Hashable α] (m : HashSet α) (a : α) (fallback : α) : α :=
+  m.inner.getKeyD a fallback
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise panics.
+If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : HashSet α) (a : α) : α :=
+  m.inner.getKey! a
+
 /--
 Returns `true` if the hash set contains no elements.
 

src/Std/Data/HashSet/Lemmas.lean

@@ -106,6 +106,18 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.insert k → (k == a) = false → a ∈ m :=
   HashMap.mem_of_mem_insertIfNew
 
+/-- This is a restatement of `contains_insert` that is written to exactly match the proof
+obligation in the statement of `get_insert`. -/
+theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.insert k).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
+  HashMap.contains_of_contains_insertIfNew'
+
+/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
+in the statement of `get_insert`. -/
+theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
+    a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
+  DHashMap.mem_of_mem_insertIfNew'
+
 @[simp]
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α}  : (m.insert k).contains k :=
   HashMap.contains_insertIfNew_self
@@ -177,6 +189,158 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     m.size ≤ (m.erase k).size + 1 :=
   HashMap.size_le_size_erase
 
+@[simp]
+theorem get?_empty {a : α} {c} : (empty c : HashSet α).get? a = none :=
+  HashMap.getKey?_empty
+
+@[simp]
+theorem get?_emptyc {a : α} : (∅ : HashSet α).get? a = none :=
+  HashMap.getKey?_emptyc
+
+theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty = true → m.get? a = none :=
+  HashMap.getKey?_of_isEmpty
+
+theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.insert k).get? a = if k == a ∧ ¬k ∈ m then some k else m.get? a :=
+  HashMap.getKey?_insertIfNew
+
+theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = (m.get? a).isSome :=
+  HashMap.contains_eq_isSome_getKey?
+
+theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = false → m.get? a = none :=
+  HashMap.getKey?_eq_none_of_contains_eq_false
+
+theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get? a = none :=
+  HashMap.getKey?_eq_none
+
+theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.erase k).get? a = if k == a then none else m.get? a :=
+  HashMap.getKey?_erase
+
+@[simp]
+theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get? k = none :=
+  HashMap.getKey?_erase_self
+
+theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
+    (m.insert k).get a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
+  HashMap.getKey_insertIfNew (h₁ := h₁)
+
+@[simp]
+theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
+    (m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=
+  HashMap.getKey_erase (h' := h')
+
+theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} :
+    m.get? a = some (m.get a h') :=
+  @HashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
+
+@[simp]
+theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default :=
+  HashMap.getKey!_empty
+
+@[simp]
+theorem get!_emptyc [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default :=
+  HashMap.getKey!_emptyc
+
+theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty = true → m.get! a = default :=
+  HashMap.getKey!_of_isEmpty
+
+theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.insert k).get! a = if k == a ∧ ¬k ∈ m then k else m.get! a :=
+  HashMap.getKey!_insertIfNew
+
+theorem get!_eq_default_of_contains_eq_false [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.contains a = false → m.get! a = default :=
+  HashMap.getKey!_eq_default_of_contains_eq_false
+
+theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
+    ¬a ∈ m → m.get! a = default :=
+  HashMap.getKey!_eq_default
+
+theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
+    (m.erase k).get! a = if k == a then default else m.get! a :=
+  HashMap.getKey!_erase
+
+@[simp]
+theorem get!_erase_self [Inhabited α] [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m.erase k).get! k = default :=
+  HashMap.getKey!_erase_self
+
+theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    {a : α} : m.contains a = true → m.get? a = some (m.get! a) :=
+  HashMap.getKey?_eq_some_getKey!_of_contains
+
+theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    a ∈ m → m.get? a = some (m.get! a) :=
+  HashMap.getKey?_eq_some_getKey!
+
+theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.get! a = (m.get? a).get! :=
+  HashMap.getKey!_eq_get!_getKey?
+
+theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h'} :
+    m.get a h' = m.get! a :=
+  HashMap.getKey_eq_getKey!
+
+@[simp]
+theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback :=
+  HashMap.getKeyD_empty
+
+@[simp]
+theorem getD_emptyc {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback :=
+  HashMap.getKeyD_emptyc
+
+theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.isEmpty = true → m.getD a fallback = fallback :=
+  HashMap.getKeyD_of_isEmpty
+
+theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+    (m.insert k).getD a fallback = if k == a ∧ ¬k ∈ m then k else m.getD a fallback :=
+  HashMap.getKeyD_insertIfNew
+
+theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {a fallback : α} :
+    m.contains a = false → m.getD a fallback = fallback :=
+  HashMap.getKeyD_eq_fallback_of_contains_eq_false
+
+theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    ¬a ∈ m → m.getD a fallback = fallback :=
+  HashMap.getKeyD_eq_fallback
+
+theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
+  HashMap.getKeyD_erase
+
+@[simp]
+theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k fallback : α} :
+    (m.erase k).getD k fallback = fallback :=
+  HashMap.getKeyD_erase_self
+
+theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.contains a = true → m.get? a = some (m.getD a fallback) :=
+  HashMap.getKey?_eq_some_getKeyD_of_contains
+
+theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    a ∈ m → m.get? a = some (m.getD a fallback) :=
+  HashMap.getKey?_eq_some_getKeyD
+
+theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a fallback : α} :
+    m.getD a fallback = (m.get? a).getD fallback :=
+  HashMap.getKeyD_eq_getD_getKey?
+
+theorem get_eq_getD [EquivBEq α] [LawfulHashable α] {a fallback : α} {h'} :
+    m.get a h' = m.getD a fallback :=
+  @HashMap.getKey_eq_getKeyD _ _ _ _ _ _ _ _ _ h'
+
+theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
+    m.get! a = m.getD a default :=
+  HashMap.getKey!_eq_getKeyD_default
+
 @[simp]
 theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.containsThenInsertIfNew_fst

src/Std/Data/HashSet/Raw.lean

@@ -14,7 +14,7 @@ set with unbundled well-formedness invariant.
 
 This version is safe to use in nested inductive types. The well-formedness predicate is
 available as `Std.Data.HashSet.Raw.WF` and we prove in this file that all operations preserve
-well-formedness. When in doubt, prefer `HashSet` over `DHashSet.Raw`.
+well-formedness. When in doubt, prefer `HashSet` over `HashSet.Raw`.
 
 Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the module
 `Std.Data.HashSet.RawLemmas`.
@@ -113,6 +113,34 @@ instance [BEq α] [Hashable α] {m : Raw α} {a : α} : Decidable (a ∈ m) :=
 @[inline] def size (m : Raw α) : Nat :=
   m.inner.size
 
+/--
+Checks if given key is contained and returns the key if it is, otherwise `none`.
+The result in the `some` case is guaranteed to be pointer equal to the key in the map.
+-/
+@[inline] def get? [BEq α] [Hashable α] (m : Raw α) (a : α) : Option α :=
+  m.inner.getKey? a
+
+/--
+Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
+of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def get [BEq α] [Hashable α] (m : Raw α) (a : α) (h : a ∈ m) : α :=
+  m.inner.getKey a h
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise `fallback`.
+If they key is contained the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def getD [BEq α] [Hashable α] (m : Raw α) (a : α) (fallback : α) : α :=
+  m.inner.getKeyD a fallback
+
+/--
+Checks if given key is contained and returns the key if it is, otherwise panics.
+If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
+-/
+@[inline] def get! [BEq α] [Hashable α] [Inhabited α] (m : Raw α) (a : α) : α :=
+  m.inner.getKey! a
+
 /--
 Returns `true` if the hash set contains no elements.
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -122,6 +122,18 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α
     a ∈ m.insert k → (k == a) = false → a ∈ m :=
   HashMap.Raw.mem_of_mem_insertIfNew h.out
 
+/-- This is a restatement of `contains_insert` that is written to exactly match the proof
+obligation in the statement of `get_insert`. -/
+theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.insert k).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
+  HashMap.Raw.contains_of_contains_insertIfNew' h.out
+
+/-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
+in the statement of `get_insertIfNew`. -/
+theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
+  HashMap.Raw.mem_of_mem_insertIfNew' h.out
+
 @[simp]
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).contains k :=
@@ -186,6 +198,162 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     m.size ≤ (m.erase k).size + 1 :=
   HashMap.Raw.size_le_size_erase h.out
 
+@[simp]
+theorem get?_empty {a : α} {c} : (empty c : Raw α).get? a = none :=
+  HashMap.Raw.getKey?_empty
+
+@[simp]
+theorem get?_emptyc {a : α} : (∅ : Raw α).get? a = none :=
+  HashMap.Raw.getKey?_emptyc
+
+theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.get? a = none :=
+  HashMap.Raw.getKey?_of_isEmpty h.out
+
+theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.insert k).get? a = if k == a ∧ ¬k ∈ m then some k else m.get? a :=
+  HashMap.Raw.getKey?_insertIfNew h.out
+
+theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = (m.get? a).isSome :=
+  HashMap.Raw.contains_eq_isSome_getKey? h.out
+
+theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.contains a = false → m.get? a = none :=
+  HashMap.Raw.getKey?_eq_none_of_contains_eq_false h.out
+
+theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    ¬a ∈ m → m.get? a = none :=
+  HashMap.Raw.getKey?_eq_none h.out
+
+theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.erase k).get? a = if k == a then none else m.get? a :=
+  HashMap.Raw.getKey?_erase h.out
+
+theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
+    (m.insert k).get a h₁ =
+      if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
+  HashMap.Raw.getKey_insertIfNew (h₁ := h₁) h.out
+
+@[simp]
+theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
+    (m.erase k).get a h' = m.get a (mem_of_mem_erase h h') :=
+  HashMap.Raw.getKey_erase (h' := h') h.out
+
+theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m} :
+    m.get? a = some (m.get a h') :=
+  @HashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
+
+@[simp]
+theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.erase k).get? k = none :=
+  HashMap.Raw.getKey?_erase_self h.out
+
+@[simp]
+theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default :=
+  HashMap.Raw.getKey!_empty
+
+@[simp]
+theorem get!_emptyc [Inhabited α] {a : α} : (∅ : Raw α).get! a = default :=
+  HashMap.Raw.getKey!_emptyc
+
+theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m.isEmpty = true → m.get! a = default :=
+  HashMap.Raw.getKey!_of_isEmpty h.out
+
+theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.insert k).get! a = if k == a ∧ ¬k ∈ m then k else m.get! a :=
+  HashMap.Raw.getKey!_insertIfNew h.out
+
+theorem get!_eq_default_of_contains_eq_false [Inhabited α] [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {a : α} :
+    m.contains a = false → m.get! a = default :=
+  HashMap.Raw.getKey!_eq_default_of_contains_eq_false h.out
+
+theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    ¬a ∈ m → m.get! a = default :=
+  HashMap.Raw.getKey!_eq_default h.out
+
+theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+    (m.erase k).get! a = if k == a then default else m.get! a :=
+  HashMap.Raw.getKey!_erase h.out
+
+@[simp]
+theorem get!_erase_self [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.erase k).get! k = default :=
+  HashMap.Raw.getKey!_erase_self h.out
+
+theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    (h : m.WF) {a : α} : m.contains a = true → m.get? a = some (m.get! a) :=
+  HashMap.Raw.getKey?_eq_some_getKey!_of_contains h.out
+
+theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    a ∈ m → m.get? a = some (m.get! a) :=
+  HashMap.Raw.getKey?_eq_some_getKey! h.out
+
+theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
+    m.get! a = (m.get? a).get! :=
+  HashMap.Raw.getKey!_eq_get!_getKey? h.out
+
+theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h'} :
+    m.get a h' = m.get! a :=
+  HashMap.Raw.getKey_eq_getKey! h.out
+
+@[simp]
+theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_empty
+
+@[simp]
+theorem getD_emptyc {a fallback : α} : (∅ : Raw α).getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_emptyc
+
+theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    m.isEmpty = true → m.getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_of_isEmpty h.out
+
+theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+    (m.insert k).getD a fallback = if k == a ∧ ¬k ∈ m then k else m.getD a fallback :=
+  HashMap.Raw.getKeyD_insertIfNew h.out
+
+theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {a fallback : α} :
+    m.contains a = false → m.getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false h.out
+
+theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
+    ¬a ∈ m → m.getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_eq_fallback h.out
+
+theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+    (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
+  HashMap.Raw.getKeyD_erase h.out
+
+@[simp]
+theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
+    (m.erase k).getD k fallback = fallback :=
+  HashMap.Raw.getKeyD_erase_self h.out
+
+theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α}
+    {fallback : α} : m.contains a = true → m.get? a = some (m.getD a fallback) :=
+  HashMap.Raw.getKey?_eq_some_getKeyD_of_contains h.out
+
+theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
+    a ∈ m → m.get? a = some (m.getD a fallback) :=
+  HashMap.Raw.getKey?_eq_some_getKeyD h.out
+
+theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
+    m.getD a fallback = (m.get? a).getD fallback :=
+  HashMap.Raw.getKeyD_eq_getD_getKey? h.out
+
+theorem get_eq_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} {h'} :
+    m.get a h' = m.getD a fallback :=
+  @HashMap.Raw.getKey_eq_getKeyD _ _ _ _ _ _ _ h.out _ _ h'
+
+theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
+    {a : α} :
+    m.get! a = m.getD a default :=
+  HashMap.Raw.getKey!_eq_getKeyD_default h.out
+
 @[simp]
 theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.Raw.containsThenInsertIfNew_fst h.out