diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 1ca34b04a8..5aea65e37f 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -240,6 +240,9 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
   getElem?_eq_some_iff.mp h
 
+theorem of_getElem_eq [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] {h} (_ : c[i] = e) : dom c i := h
+
 @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
     (some c[i] = c[i]?) ↔ True := by
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 955e723274..e5ee617497 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1115,6 +1115,8 @@ theorem getThenInsertIfNew?_snd [LawfulBEq α] {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v :=
   ext <| congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _ (k := k))
 
+theorem mem_of_get_eq [LawfulBEq α] {k : α} {v : β k} {w} (_ : m.get k w = v) : k ∈ m := w
+
 namespace Const
 
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 014cec081d..c035560fa9 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1181,6 +1181,8 @@ theorem getThenInsertIfNew?_snd [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v := by
   simp_to_raw using congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _)
 
+theorem mem_of_get_eq [LawfulBEq α] {k : α} {v : β k} {w} (_ : m.get k w = v) : k ∈ m := w
+
 namespace Const
 
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index 453d977b49..59155fa5c0 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -1058,6 +1058,8 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : 
     (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v :=
   ext <| Impl.getThenInsertIfNew?_snd t.wf
 
+theorem mem_of_get_eq [LawfulEqCmp cmp] {k : α} {v : β k} {w} (_ : t.get k w = v) : k ∈ t := w
+
 namespace Const
 
 variable {β : Type v} {t : DTreeMap α β cmp}
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 58c576c503..ced03cacb0 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -1068,6 +1068,8 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k :
     (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v :=
   ext <| Impl.getThenInsertIfNew?!_snd h
 
+theorem mem_of_get_eq [LawfulEqCmp cmp] {k : α} {v : β k} {w} (_ : t.get k w = v) : k ∈ t := w
+
 namespace Const
 
 variable {β : Type v} {t : Raw α β cmp}
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index 46b894f590..29e731261a 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -951,6 +951,8 @@ theorem getThenInsertIfNew?_snd [LawfulBEq α] {k : α} {v : β k} :
     (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v :=
   m.inductionOn fun _ => congrArg mk DHashMap.getThenInsertIfNew?_snd
 
+theorem mem_of_get_eq [LawfulBEq α] {k : α} {v : β k} {w} (_ : m.get k w = v) : k ∈ m := w
+
 namespace Const
 
 variable {β : Type v} {m : ExtDHashMap α (fun _ => β)}
diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean
index 0eaabe5210..97fb8e9d7e 100644
--- a/src/Std/Data/ExtDTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean
@@ -1004,6 +1004,8 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : 
     (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v :=
   t.inductionOn fun _ => congrArg mk DTreeMap.getThenInsertIfNew?_snd
 
+theorem mem_of_get_eq [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} {w} (_ : t.get k w = v) : k ∈ t := w
+
 namespace Const
 
 variable {β : Type v} {t : ExtDTreeMap α β cmp}
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
index ddf512a061..2824eaa0c3 100644
--- a/src/Std/Data/ExtHashSet/Lemmas.lean
+++ b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -123,6 +123,8 @@ theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k := by
   simp
 
+theorem mem_of_get_eq [LawfulBEq α] (m : ExtHashSet α) {k v : α} {w} (_ : m.get k w = v) : k ∈ m := w
+
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
 @[simp, grind =]
diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean
index f835605b93..468a368305 100644
--- a/src/Std/Data/ExtTreeSet/Lemmas.lean
+++ b/src/Std/Data/ExtTreeSet/Lemmas.lean
@@ -107,6 +107,8 @@ theorem contains_insert_self [TransCmp cmp] {k : α} :
     (t.insert k).contains k :=
   ExtTreeMap.contains_insertIfNew_self
 
+theorem mem_of_get_eq [TransCmp cmp] {k v : α} {w} (_ : t.get k w = v) : k ∈ t := w
+
 theorem mem_insert_self [TransCmp cmp] {k : α} :
     k ∈ t.insert k :=
   ExtTreeMap.mem_insertIfNew_self
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 554babd22c..026824df69 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -140,6 +140,8 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.ins
 
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
+theorem mem_of_get_eq {k v : α} {w} (_ : m.get k w = v) : k ∈ m := w
+
 @[simp, grind =]
 theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).size = 0 :=
   HashMap.size_emptyWithCapacity
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 1ca8451b58..eeda79bc08 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -167,6 +167,8 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : 
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : k ∈ m.insert k :=
   HashMap.Raw.mem_insertIfNew_self h.out
 
+theorem mem_of_get_eq {k v : α} {w} (_ : m.get k w = v) : k ∈ m := w
+
 @[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.Raw.size_insertIfNew h.out
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index 2de31e600c..f909cc34db 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -114,6 +114,8 @@ theorem contains_insert_self [TransCmp cmp] {k : α} :
     (t.insert k).contains k :=
   TreeMap.contains_insertIfNew_self
 
+theorem mem_of_get_eq  {k v : α} {w} (_ : t.get k w = v) : k ∈ t := w
+
 theorem mem_insert_self [TransCmp cmp] {k : α} :
     k ∈ t.insert k :=
   TreeMap.mem_insertIfNew_self
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index b54ebe2371..c8467c8bb7 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -116,6 +116,8 @@ theorem contains_insert_self [TransCmp cmp] (h : t.WF) {k : α} :
     (t.insert k).contains k :=
   TreeMap.Raw.contains_insertIfNew_self h
 
+theorem mem_of_get_eq  {k v : α} {w} (_ : t.get k w = v) : k ∈ t := w
+
 theorem mem_insert_self [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.insert k :=
   TreeMap.Raw.mem_insertIfNew_self h