feat: add missing lemmas about insertMany and get? for container types (#10247)

This PR adds missing the lemmas `ofList_eq_insertMany_empty`,
`get?_eq_some_iff`, `getElem?_eq_some_iff` and `getKey?_eq_some_iff` to
all container types.

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

@@ -334,6 +334,10 @@ theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.1.WF) {a : α} :
     m.contains a = (m.get? a).isSome := by
   simp_to_model [contains, get?] using List.containsKey_eq_isSome_getValueCast?
 
+theorem get?_eq_some_iff [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
+    m.get? k = some v ↔ ∃ h : m.contains k, m.get k h = v := by
+  simp_to_model [contains, get?, get] using List.getValueCast?_eq_some_iff
+
 theorem get?_eq_none [LawfulBEq α] (h : m.1.WF) {a : α} :
     m.contains a = false → m.get? a = none := by
   simp_to_model [contains, get?] using List.getValueCast?_eq_none
@@ -373,6 +377,10 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {
     m.contains a = (get? m a).isSome := by
   simp_to_model [contains, Const.get?] using List.containsKey_eq_isSome_getValue?
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
+    get? m k = some v ↔ ∃ h : m.contains k, get m k h = v := by
+  simp_to_model [contains, Const.get?, Const.get] using List.getValue?_eq_some_iff
+
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
     m.contains a = false → get? m a = none := by
   simp_to_model [contains, Const.get?] using List.getValue?_eq_none.2
@@ -701,6 +709,10 @@ theorem getKey?_eq_some [LawfulBEq α] (h : m.1.WF) {a : α} :
     m.contains a → m.getKey? a = some a := by
   simp_to_model [getKey?, contains] using List.getKey?_eq_some
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} :
+    m.getKey? k = some k' ↔ ∃ h : m.contains k, m.getKey k h = k' := by
+  simp_to_model [contains, getKey?, getKey] using List.getKey?_eq_some_iff'
+
 theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {k k' : α} (h : k == k') :
     m.getKey? k = m.getKey? k' := by

src/Std/Data/DHashMap/Lemmas.lean

@@ -272,6 +272,10 @@ theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isS
 theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [LawfulBEq α] {k : α} {v : β k} :
+    m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v :=
+  Raw₀.get?_eq_some_iff ⟨m.1, _⟩ m.2
+
 theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} :
     m.contains a = false → m.get? a = none :=
   Raw₀.get?_eq_none ⟨m.1, _⟩ m.2
@@ -332,6 +336,10 @@ theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m
 theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (get? m a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v :=
+  Raw₀.Const.get?_eq_some_iff ⟨m.1, _⟩ m.2
+
 theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → get? m a = none :=
   Raw₀.Const.get?_eq_none ⟨m.1, _⟩ m.2
@@ -748,6 +756,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.getKey? k = some k') : k' ∈ m :=
   Raw₀.contains_of_getKey?_eq_some ⟨m.1, _⟩ m.2 h
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' :=
+  Raw₀.getKey?_eq_some_iff ⟨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

src/Std/Data/DHashMap/RawLemmas.lean

@@ -322,6 +322,11 @@ theorem mem_iff_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
 theorem isSome_get?_iff_mem [LawfulBEq α] (h : m.WF) {a : α} : (m.get? a).isSome ↔ a ∈ m :=
   (mem_iff_isSome_get? h).symm
 
+theorem get?_eq_some_iff [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
+    m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v := by
+  simp only [mem_iff_contains]
+  simp_to_raw using Raw₀.get?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α} :
     m.contains a = false → m.get? a = none := by
   simp_to_raw using Raw₀.get?_eq_none
@@ -385,6 +390,11 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α
     (get? m a).isSome ↔ a ∈ m :=
   (mem_iff_isSome_get? h).symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
+    get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v := by
+  simp only [mem_iff_contains]
+  simp_to_raw using Raw₀.Const.get?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.contains a = false → get? m a = none := by
   simp_to_raw using Raw₀.Const.get?_eq_none
@@ -800,12 +810,16 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
     (m.getKey? a).isSome ↔ a ∈ m :=
   (mem_iff_isSome_getKey? h).symm
 
-theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
-    {a a' : α} (h : m.WF) :
+theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {a a' : α} (h : m.WF) :
     m.getKey? a = some a' → a' ∈ m := by
   simp [← contains_iff_mem]
   simp_to_raw using Raw₀.contains_of_getKey?_eq_some
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.WF) :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' := by
+  simp [← contains_iff_mem]
+  simp_to_raw using Raw₀.getKey?_eq_some_iff
+
 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

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -535,6 +535,10 @@ theorem mem_iff_isSome_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} :
     a ∈ t ↔ (t.get? a).isSome := by
   simpa [mem_iff_contains] using contains_eq_isSome_get? h
 
+theorem get?_eq_some_iff [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    t.get? k = some v ↔ ∃ h, t.get k h = v := by
+  simp_to_model [contains, get?, get] using List.getValueCast?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} :
     t.contains a = false → t.get? a = none := by
   simp_to_model [contains, get?] using List.getValueCast?_eq_none
@@ -596,6 +600,10 @@ theorem mem_iff_isSome_get? [TransOrd α] (h : t.WF) {a : α} :
     a ∈ t ↔ (get? t a).isSome := by
   simpa [mem_iff_contains] using contains_eq_isSome_get? h
 
+theorem get?_eq_some_iff [TransOrd α] (h : t.WF) {k : α} {v : β} :
+    get? t k = some v ↔ ∃ h, get t k h = v := by
+  simp_to_model [contains, Const.get?, Const.get] using List.getValue?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} :
     t.contains a = false → get? t a = none := by
   simp_to_model [Const.get?, contains] using List.getValue?_eq_none.mpr
@@ -1051,6 +1059,10 @@ theorem mem_of_getKey?_eq_some [TransOrd α] {a a' : α} (h : t.WF) :
     t.getKey? a = some a' → a' ∈ t := by
   simp_to_model [getKey?, contains] using List.containsKey_of_getKey?_eq_some
 
+theorem getKey?_eq_some_iff [TransOrd α] {k k' : α} (h : t.WF) :
+    t.getKey? k = some k' ↔ ∃ h, t.getKey k h = k' := by
+  simp_to_model [getKey?, contains, getKey] using List.getKey?_eq_some_iff'
+
 theorem getKey?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} :
     t.contains a = false → t.getKey? a = none := by
   simp_to_model [contains, getKey?] using List.getKey?_eq_none

src/Std/Data/DTreeMap/Lemmas.lean

@@ -254,6 +254,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (t.get? a).isSome ↔ a ∈ t :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
+    t.get? k = some v ↔ ∃ h, t.get k h = v :=
+  Impl.get?_eq_some_iff t.wf
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     t.contains a = false → t.get? a = none :=
   Impl.get?_eq_none_of_contains_eq_false t.wf
@@ -307,6 +311,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} :
     a ∈ t ↔ (get? t a).isSome :=
   Impl.Const.mem_iff_isSome_get? t.wf
 
+theorem get?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
+    get? t k = some v ↔ ∃ h, get t k h = v :=
+  Impl.Const.get?_eq_some_iff t.wf
+
 @[simp]
 theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} :
     (get? t a).isSome ↔ a ∈ t :=
@@ -694,6 +702,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} :
     t.getKey? k = some k' → k' ∈ t :=
   Impl.mem_of_getKey?_eq_some t.wf
 
+theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  Impl.getKey?_eq_some_iff t.wf
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.getKey? a = none :=
   Impl.getKey?_eq_none_of_contains_eq_false t.wf

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -255,6 +255,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α}
     (t.get? a).isSome ↔ a ∈ t :=
   (mem_iff_isSome_get? h).symm
 
+theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    t.get? k = some v ↔ ∃ h, t.get k h = v :=
+  Impl.get?_eq_some_iff h
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → t.get? a = none :=
   Impl.get?_eq_none_of_contains_eq_false h
@@ -308,6 +312,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ (get? t a).isSome :=
   Impl.Const.mem_iff_isSome_get? h
 
+theorem get?_eq_some_iff [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    get? t k = some v ↔ ∃ h, get t k h = v :=
+  Impl.Const.get?_eq_some_iff h
+
 @[simp]
 theorem isSome_get?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
     (get? t a).isSome ↔ a ∈ t :=
@@ -697,6 +705,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] (h : t.WF) {k k' : α} :
     t.getKey? k = some k' → k' ∈ t :=
   Impl.mem_of_getKey?_eq_some h
 
+theorem getKey?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  Impl.getKey?_eq_some_iff h
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → t.getKey? a = none :=
   Impl.getKey?_eq_none_of_contains_eq_false h

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -214,6 +214,10 @@ theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isS
 theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [LawfulBEq α] {k : α} {v : β k} :
+    m.get? k = some v ↔ ∃ h : k ∈ m, m.get k h = v :=
+  m.inductionOn fun _ => DHashMap.get?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [LawfulBEq α] {a : α} :
     m.contains a = false → m.get? a = none :=
   m.inductionOn fun _ => DHashMap.get?_eq_none_of_contains_eq_false
@@ -263,6 +267,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     (get? m a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    get? m k = some v ↔ ∃ h : k ∈ m, get m k h = v :=
+  m.inductionOn fun _ => DHashMap.Const.get?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → get? m a = none :=
   m.inductionOn fun _ => DHashMap.Const.get?_eq_none_of_contains_eq_false
@@ -611,6 +619,10 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     (m.getKey? a).isSome ↔ a ∈ m :=
   mem_iff_isSome_getKey?.symm
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' :=
+  m.inductionOn fun _ => DHashMap.getKey?_eq_some_iff
+
 theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.getKey? k = some k') : k' ∈ m :=
   m.inductionOn (fun _ h => DHashMap.mem_of_getKey?_eq_some h) h

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -234,6 +234,10 @@ theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (t.get? a).isSome ↔ a ∈ t :=
   t.inductionOn fun _ => DTreeMap.isSome_get?_iff_mem
 
+theorem get?_eq_some_iff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
+    t.get? k = some v ↔ ∃ h, t.get k h = v :=
+  t.inductionOn fun _ => DTreeMap.get?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     t.contains a = false → t.get? a = none :=
   t.inductionOn fun _ => DTreeMap.get?_eq_none_of_contains_eq_false
@@ -283,6 +287,10 @@ theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} :
     a ∈ t ↔ (get? t a).isSome :=
   t.inductionOn fun _ => DTreeMap.Const.mem_iff_isSome_get?
 
+theorem get?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
+    get? t k = some v ↔ ∃ h, get t k h = v :=
+  t.inductionOn fun _ => DTreeMap.Const.get?_eq_some_iff
+
 @[simp]
 theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} :
     (get? t a).isSome ↔ a ∈ t :=
@@ -650,6 +658,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} :
     t.getKey? k = some k' → k' ∈ t :=
   t.inductionOn fun _ => DTreeMap.mem_of_getKey?_eq_some
 
+theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  t.inductionOn fun _ => DTreeMap.getKey?_eq_some_iff
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.getKey? a = none :=
   t.inductionOn fun _ => DTreeMap.getKey?_eq_none_of_contains_eq_false

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -229,6 +229,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     m[a]?.isSome ↔ a ∈ m :=
   mem_iff_isSome_getElem?.symm
 
+theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v :=
+  ExtDHashMap.Const.get?_eq_some_iff
+
 theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → m[a]? = none :=
   ExtDHashMap.Const.get?_eq_none_of_contains_eq_false
@@ -421,6 +425,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.getKey? k = some k') : k' ∈ m :=
   ExtDHashMap.mem_of_getKey?_eq_some h
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' :=
+  ExtDHashMap.getKey?_eq_some_iff
+
 theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → m.getKey? a = none :=
   ExtDHashMap.getKey?_eq_none_of_contains_eq_false

src/Std/Data/ExtHashSet/Lemmas.lean

@@ -209,6 +209,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     (m.get? a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' :=
+  ExtHashMap.getKey?_eq_some_iff
+
 theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.get? k = some k') : k' ∈ m :=
   ExtHashMap.mem_of_getKey?_eq_some h

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -243,6 +243,10 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} :
     t[a]?.isSome ↔ a ∈ t :=
   mem_iff_isSome_getElem?.symm
 
+theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
+    t[k]? = some v ↔ ∃ h, t[k] = v :=
+  ExtDTreeMap.Const.get?_eq_some_iff
+
 theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t[a]? = none :=
   ExtDTreeMap.Const.get?_eq_none_of_contains_eq_false
@@ -445,6 +449,10 @@ theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α} :
     t.getKey? k = some k' → k' ∈ t :=
   ExtDTreeMap.mem_of_getKey?_eq_some
 
+theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  ExtDTreeMap.getKey?_eq_some_iff
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.getKey? a = none :=
   ExtDTreeMap.getKey?_eq_none_of_contains_eq_false
@@ -757,10 +765,6 @@ instance [TransCmp cmp] : LawfulGetElem (ExtTreeMap α β cmp) α β (fun m a =>
     rw [getElem!_eq_get!_getElem?]
     split <;> simp_all
 
-theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
-    t[k]? = some v ↔ ∃ h : k ∈ t, t[k] = v :=
-  _root_.getElem?_eq_some_iff
-
 @[simp, grind =]
 theorem length_keys [TransCmp cmp] :
     t.keys.length = t.size :=

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -225,6 +225,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] {k k' : α}
     (h : t.get? k = some k') : k' ∈ t :=
   ExtTreeMap.mem_of_getKey?_eq_some h
 
+theorem get?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    t.get? k = some k' ↔ ∃ h, t.get k h = k' :=
+  ExtTreeMap.getKey?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.get? a = none :=
   ExtTreeMap.getKey?_eq_none_of_contains_eq_false

src/Std/Data/HashMap/Lemmas.lean

@@ -284,6 +284,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     m[a]?.isSome ↔ a ∈ m :=
   mem_iff_isSome_getElem?.symm
 
+theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v :=
+  DHashMap.Const.get?_eq_some_iff
+
 theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → m[a]? = none :=
   DHashMap.Const.get?_eq_none_of_contains_eq_false
@@ -509,6 +513,10 @@ theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.getKey? k = some k') : k' ∈ m :=
   DHashMap.mem_of_getKey?_eq_some h
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' :=
+  DHashMap.getKey?_eq_some_iff
+
 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
@@ -828,10 +836,6 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     rw [getElem!_eq_get!_getElem?]
     split <;> simp_all
 
-theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v :=
-  _root_.getElem?_eq_some_iff
-
 @[simp, grind =]
 theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=

src/Std/Data/HashMap/RawLemmas.lean

@@ -298,6 +298,10 @@ theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
     (m[a]?).isSome ↔ a ∈ m :=
   (mem_iff_isSome_getElem? h).symm
 
+theorem getElem?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ h : k ∈ m, m[k] = v :=
+  DHashMap.Raw.Const.get?_eq_some_iff h.out
+
 theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.contains a = false → m[a]? = none :=
   DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false h.out
@@ -563,11 +567,14 @@ theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
     (m.getKey? a).isSome ↔ a ∈ m :=
   (mem_iff_isSome_getKey? h).symm
 
-theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
-    {a a' : α} (h : m.WF) :
+theorem mem_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] {a a' : α} (h : m.WF) :
     m.getKey? a = some a' → a' ∈ m :=
   DHashMap.Raw.mem_of_getKey?_eq_some h.out
 
+theorem getKey?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.WF) :
+    m.getKey? k = some k' ↔ ∃ h : k ∈ m, m.getKey k h = k' :=
+  DHashMap.Raw.getKey?_eq_some_iff h.out
+
 @[simp, grind =]
 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') :=

src/Std/Data/HashSet/Lemmas.lean

@@ -257,6 +257,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
     (m.get? a).isSome ↔ a ∈ m :=
   mem_iff_isSome_get?.symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] {k k' : α} :
+    m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' :=
+  HashMap.getKey?_eq_some_iff
+
 theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α}
     (h : m.get? k = some k') : k' ∈ m :=
   HashMap.mem_of_getKey?_eq_some h

src/Std/Data/HashSet/RawLemmas.lean

@@ -269,6 +269,10 @@ theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α
     (m.get? a).isSome ↔ a ∈ m :=
   (mem_iff_isSome_get? h).symm
 
+theorem get?_eq_some_iff [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} :
+    m.get? k = some k' ↔ ∃ h : k ∈ m, m.get k h = k' :=
+  HashMap.Raw.getKey?_eq_some_iff h.out
+
 theorem mem_of_get?_eq_some [EquivBEq α] [LawfulHashable α] (h : m.WF) {a a' : α} :
     m.get? a = some a' → a' ∈ m :=
   HashMap.Raw.mem_of_getKey?_eq_some h.out
@@ -784,6 +788,12 @@ theorem ofList_cons {hd : α} {tl : List α} :
     ofList (hd :: tl) = insertMany ((∅ : Raw α).insert hd) tl :=
   ext HashMap.Raw.unitOfList_cons
 
+theorem ofList_eq_insertMany_empty {l : List α} :
+    ofList l = insertMany (∅ : Raw α) l :=
+  match l with
+  | [] => by simp [insertMany_nil .empty]
+  | hd :: tl => by simp [ofList_cons, insertMany_cons .empty]
+
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :

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

@@ -547,6 +547,12 @@ theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α}
     getValue? a l = some (getValue a l h) := by
   simp [getValue]
 
+theorem getValue?_eq_some_iff [BEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
+    getValue? k l = some v ↔ ∃ h : containsKey k l, getValue k l h = v := by
+  by_cases h : containsKey k l
+  · simp [h, getValue?_eq_some_getValue]
+  · simp [getValue?_eq_none.mpr (Bool.not_eq_true _ ▸ h), h]
+
 theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
     getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq h) = v := by
   simp [getValue, getValue?_cons_of_true h]
@@ -603,6 +609,12 @@ theorem getValueCast?_eq_some_getValueCast [BEq α] [LawfulBEq α] {l : List ((a
     (h : containsKey a l) : getValueCast? a l = some (getValueCast a l h) := by
   simp [getValueCast]
 
+theorem getValueCast?_eq_some_iff [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
+    getValueCast? k l = some v ↔ ∃ h : containsKey k l, getValueCast k l h = v := by
+  by_cases h : containsKey k l
+  · simp [h, getValueCast?_eq_some_getValueCast]
+  · simp [getValueCast?_eq_none (Bool.not_eq_true _ ▸ h), h]
+
 theorem getValueCast_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
     (h : containsKey a (⟨k, v⟩ :: l)) :
     getValueCast a (⟨k, v⟩ :: l) h =
@@ -884,6 +896,15 @@ theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
   · rfl
   · exact getKey?_eq_some_getKey _
 
+theorem getKey?_eq_some_iff' [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k'} :
+    getKey? k l = some k' ↔ ∃ h, getKey k l h = k' := by
+  by_cases h : containsKey k l
+  · simp [h, getKey?_eq_some_getKey]
+  · simp only [h]
+    simp only [containsKey_eq_isSome_getKey?, Bool.not_eq_true, Option.isSome_eq_false_iff,
+      Option.isNone_iff_eq_none] at h
+    simp [h]
+
 theorem getKey_beq [BEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
     getKey a l h == a := by
   simpa only [getKey?_eq_some_getKey h] using getKey?_beq (l := l) (a := a)

src/Std/Data/TreeMap/Lemmas.lean

@@ -255,10 +255,18 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} :
     t[a]?.isSome ↔ a ∈ t :=
   mem_iff_isSome_getElem?.symm
 
+theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
+    t[k]? = some v ↔ ∃ h, t[k] = v :=
+  DTreeMap.Const.get?_eq_some_iff
+
 theorem mem_of_getKey?_eq_some [TransCmp cmp] {k k' : α}
     (h : t.getKey? k = some k') : k' ∈ t :=
   DTreeMap.mem_of_getKey?_eq_some h
 
+theorem getKey?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  DTreeMap.getKey?_eq_some_iff
+
 theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t[a]? = none :=
   DTreeMap.Const.get?_eq_none_of_contains_eq_false
@@ -789,10 +797,6 @@ instance [TransCmp cmp] : LawfulGetElem (TreeMap α β cmp) α β (fun m a => a
     rw [getElem!_eq_get!_getElem?]
     split <;> simp_all
 
-theorem getElem?_eq_some_iff [TransCmp cmp] {k : α} {v : β} :
-    t[k]? = some v ↔ ∃ h : k ∈ t, t[k] = v :=
-  _root_.getElem?_eq_some_iff
-
 @[simp, grind =]
 theorem length_keys [TransCmp cmp] :
     t.keys.length = t.size :=

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -255,6 +255,10 @@ theorem isSome_getElem?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
     t[a]?.isSome ↔ a ∈ t :=
   (mem_iff_isSome_getElem? h).symm
 
+theorem getElem?_eq_some_iff [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    t[k]? = some v ↔ ∃ h, t[k] = v :=
+  DTreeMap.Raw.Const.get?_eq_some_iff h
+
 theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → t[a]? = none :=
   DTreeMap.Raw.Const.get?_eq_none_of_contains_eq_false h
@@ -465,10 +469,14 @@ theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
     (t.getKey? a).isSome ↔ a ∈ t :=
   (mem_iff_isSome_getKey? h).symm
 
-theorem mem_of_getKey?_eq_some [TransCmp cmp] {a a' : α} (h : t.WF) :
+theorem mem_of_getKey?_eq_some [TransCmp cmp] (h : t.WF) {a a' : α} :
     t.getKey? a = some a' → a' ∈ t :=
   DTreeMap.Raw.mem_of_getKey?_eq_some h
 
+theorem getKey?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} :
+    getKey? t k = some k' ↔ ∃ h, getKey t k h = k' :=
+  DTreeMap.Raw.getKey?_eq_some_iff h
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → t.getKey? a = none :=
   DTreeMap.Raw.getKey?_eq_none_of_contains_eq_false h

src/Std/Data/TreeSet/Lemmas.lean

@@ -238,6 +238,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] {k k' : α}
     (h : t.get? k = some k') : k' ∈ t :=
   TreeMap.mem_of_getKey?_eq_some h
 
+theorem get?_eq_some_iff [TransCmp cmp] {k k' : α} :
+    t.get? k = some k' ↔ ∃ h, t.get k h = k' :=
+  TreeMap.getKey?_eq_some_iff
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.get? a = none :=
   TreeMap.getKey?_eq_none_of_contains_eq_false

src/Std/Data/TreeSet/Raw/Lemmas.lean

@@ -236,6 +236,10 @@ theorem mem_of_get?_eq_some [TransCmp cmp] (h : t.WF) {a a' : α} :
     t.get? a = some a' → a' ∈ t :=
   TreeMap.Raw.mem_of_getKey?_eq_some h
 
+theorem get?_eq_some_iff [TransCmp cmp] (h : t.WF) {k k' : α} :
+    t.get? k = some k' ↔ ∃ h, t.get k h = k' :=
+  TreeMap.Raw.getKey?_eq_some_iff h
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → t.get? a = none :=
   TreeMap.Raw.getKey?_eq_none_of_contains_eq_false h