chore: fix statements of HashMap.getKey_insert

src/Std/Data/ExtHashMap/Lemmas.lean

diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
index 01370e6..f9a5b8d 100644
--- a/src/Std/Data/ExtHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -419,9 +419,9 @@
   simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
 
 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₂)) :=
-  ExtDHashMap.Const.get_insert (h₁ := h₁)
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then k else m.getKey a ((mem_of_mem_insert h₁ (by simpa using h₂))) :=
+  ExtDHashMap.getKey_insert (h₁ := h₁)
 
 @[simp]
 theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :

src/Std/Data/HashMap/Lemmas.lean

diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 72b21d8..3717b63 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -507,9 +507,9 @@
   simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
 
 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₁)
+    (m.insert k v).getKey a h₁ =
+      if h₂ : k == a then k else m.getKey a (mem_of_mem_insert h₁ (by simpa using h₂)) :=
+  DHashMap.getKey_insert (h₁ := h₁)
 
 @[simp]
 theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :