diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 7391079fa2..6ba7d48146 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -49,12 +49,18 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
 theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
+-- While setting up the API, often use this in the reverse direction,
+-- but prefer this direction for users.
+@[simp]
+theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
+  Iff.rfl
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   Raw₀.contains_congr _ m.2 hab
 
 theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by
-  simp [mem_iff_contains, contains_congr hab]
+  simp [← contains_iff_mem, contains_congr hab]
 
 @[simp]
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false :=
@@ -83,7 +89,7 @@ theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
 
 theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty → ¬a ∈ m := by
-  simpa [mem_iff_contains] using contains_of_isEmpty
+  simpa [← contains_iff_mem] using contains_of_isEmpty
 
 theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
     m.isEmpty = false ↔ ∃ a, m.contains a = true :=
@@ -91,7 +97,7 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
 
 theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
     m.isEmpty = false ↔ ∃ a, a ∈ m := by
-  simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true
+  simpa [← contains_iff_mem] using isEmpty_eq_false_iff_exists_contains_eq_true
 
 theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
     m.isEmpty = true ↔ ∀ a, m.contains a = false :=
@@ -99,7 +105,7 @@ theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
 
 theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
     m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
-  simpa [mem_iff_contains] using isEmpty_iff_forall_contains
+  simpa [← contains_iff_mem] using isEmpty_iff_forall_contains
 
 @[simp] theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p m = m.insert p.1 p.2 := rfl
 
@@ -115,7 +121,7 @@ theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k}
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
-  simp [mem_iff_contains, contains_insert]
+  simp [← contains_iff_mem, contains_insert]
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     (m.insert k v).contains a → (k == a) = false → m.contains a :=
@@ -123,7 +129,7 @@ theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α}
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insert k v → (k == a) = false → a ∈ m := by
-  simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
+  simpa [← contains_iff_mem, -contains_insert] using contains_of_contains_insert
 
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insert k v).contains k := by simp
@@ -182,7 +188,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
-  simp [mem_iff_contains, contains_erase]
+  simp [← contains_iff_mem, contains_erase]
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).contains a → m.contains a :=
@@ -246,15 +252,23 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
 theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
   Raw₀.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
 
+@[simp]
+theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isSome :=
   Bool.eq_iff_iff.mp contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 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
 
 theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
@@ -297,15 +311,24 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (get? m a).isSome :=
   Raw₀.Const.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (get? m a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ (get? m a).isSome :=
   Bool.eq_iff_iff.mp contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : (get? m a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 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
 
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     Const.get? (m.erase k) a = if k == a then none else get? m a :=
@@ -426,7 +449,7 @@ theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] {a : α} [Inhabited
 
 theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
     ¬a ∈ m → m.get! a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
+  simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
     (m.erase k).get! a = if k == a then default else m.get! a :=
@@ -443,7 +466,7 @@ theorem get?_eq_some_get!_of_contains [LawfulBEq α] {a : α} [Inhabited (β a)]
 
 theorem get?_eq_some_get! [LawfulBEq α] {a : α} [Inhabited (β a)] :
     a ∈ m → m.get? a = some (m.get! a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains
+  simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains
 
 theorem get!_eq_get!_get? [LawfulBEq α] {a : α} [Inhabited (β a)] :
     m.get! a = (m.get? a).get! :=
@@ -489,7 +512,7 @@ theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [
 
 theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     ¬a ∈ m → get! m a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
+  simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
     get! (m.erase k) a = if k == a then default else get! m a :=
@@ -506,7 +529,7 @@ theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabit
 
 theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     a ∈ m → get? m a = some (get! m a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains
+  simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains
 
 theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     get! m a = (get? m a).get! :=
@@ -560,7 +583,7 @@ theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] {a : α} {fallback
 
 theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
     ¬a ∈ m → m.getD a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
+  simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
@@ -577,7 +600,7 @@ theorem get?_eq_some_getD_of_contains [LawfulBEq α] {a : α} {fallback : β a}
 
 theorem get?_eq_some_getD [LawfulBEq α] {a : α} {fallback : β a} :
     a ∈ m → m.get? a = some (m.getD a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains
+  simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains
 
 theorem getD_eq_getD_get? [LawfulBEq α] {a : α} {fallback : β a} :
     m.getD a fallback = (m.get? a).getD fallback :=
@@ -628,7 +651,7 @@ theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
 
 theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     ¬a ∈ m → getD m a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
+  simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
     getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback :=
@@ -645,7 +668,7 @@ theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] {a : α}
 
 theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     a ∈ m → get? m a = some (getD m a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains
+  simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains
 
 theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     getD m a fallback = (get? m a).getD fallback :=
@@ -698,10 +721,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.getKey? a).isSome :=
   Raw₀.contains_eq_isSome_getKey? ⟨m.1, _⟩ m.2
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.getKey? a).isSome :=
   Bool.eq_iff_iff.mp contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_getKey?.symm
+
 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
@@ -711,7 +744,7 @@ theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {
   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
+  simpa [← contains_iff_mem] 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 :=
@@ -812,7 +845,7 @@ theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α
 
 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
+  simpa [← contains_iff_mem] 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 :=
@@ -829,7 +862,7 @@ theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [I
 
 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
+  simpa [← contains_iff_mem] using getKey?_eq_some_getKey!_of_contains
 
 theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
     m.getKey! a = (m.getKey? a).get! :=
@@ -885,7 +918,7 @@ theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable 
 
 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
+  simpa [← contains_iff_mem] 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 :=
@@ -902,7 +935,7 @@ theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] {a
 
 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
+  simpa [← contains_iff_mem] 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 :=
@@ -941,7 +974,7 @@ theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : 
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
-  simp [mem_iff_contains, contains_insertIfNew]
+  simp [← contains_iff_mem, contains_insertIfNew]
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insertIfNew k v).contains k :=
@@ -949,7 +982,7 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v
 
 theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     k ∈ m.insertIfNew k v := by
-  simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self
+  simpa [← contains_iff_mem, -contains_insertIfNew] using contains_insertIfNew_self
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     (m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
@@ -957,7 +990,7 @@ theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
-  simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew
+  simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew
 
 /-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `get_insertIfNew`. -/
@@ -969,7 +1002,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a
 in the statement of `get_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
-  simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
+  simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
@@ -1037,24 +1070,24 @@ 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]
+  simp [← contains_iff_mem, 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]
+  simp [← contains_iff_mem, 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]
+  simp [← contains_iff_mem, 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]
+  simp [← contains_iff_mem, contains_insertIfNew]
   exact Raw₀.getKeyD_insertIfNew ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -1380,7 +1413,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
     k ∈ m.insertMany l ↔ k ∈ m ∨ (l.map Sigma.fst).contains k := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
 
 theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} (mem : k ∈ m.insertMany l)
@@ -1574,7 +1607,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
 
 theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} (mem : k ∈ insertMany m l)
@@ -1764,7 +1797,7 @@ theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
 theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
 
 theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 861f532b1b..8f5bb01023 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -102,13 +102,17 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
 theorem mem_iff_contains {m : Raw α β} {a : α} :
     a ∈ m ↔ m.contains a := Iff.rfl
 
+@[simp]
+theorem contains_iff_mem {m : Raw α β} {a : α} :
+    m.contains a ↔ a ∈ m := Iff.rfl
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
     m.contains a = m.contains b := by
   simp_to_raw using Raw₀.contains_congr
 
 theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
     a ∈ m ↔ b ∈ m := by
-  simp [mem_iff_contains, contains_congr h hab]
+  simp [← contains_iff_mem, contains_congr h hab]
 
 @[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := by
   simp_to_raw using Raw₀.contains_emptyWithCapacity
@@ -136,7 +140,7 @@ theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α
 
 theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty → ¬a ∈ m := by
-  simpa [mem_iff_contains] using contains_of_isEmpty h
+  simpa [← contains_iff_mem] using contains_of_isEmpty h
 
 theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.isEmpty = false ↔ ∃ a, m.contains a = true := by
@@ -144,7 +148,7 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
 
 theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.isEmpty = false ↔ ∃ a, a ∈ m := by
-  simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h
+  simpa [← contains_iff_mem] using isEmpty_eq_false_iff_exists_contains_eq_true h
 
 theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.isEmpty = true ↔ ∀ a, m.contains a = false := by
@@ -152,7 +156,7 @@ theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.WF)
 
 theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
-  simpa [mem_iff_contains] using isEmpty_iff_forall_contains h
+  simpa [← contains_iff_mem] using isEmpty_iff_forall_contains h
 
 @[simp] theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p m = m.insert p.1 p.2 := rfl
 
@@ -168,7 +172,7 @@ theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α}
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
-  simp [mem_iff_contains, contains_insert h]
+  simp [← contains_iff_mem, contains_insert h]
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} :
     (m.insert k v).contains a → (k == a) = false → m.contains a := by
@@ -176,7 +180,7 @@ theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF)
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insert k v → (k == a) = false → a ∈ m := by
-  simpa [mem_iff_contains] using contains_of_contains_insert h
+  simpa [← contains_iff_mem] using contains_of_contains_insert h
 
 @[simp]
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
@@ -227,7 +231,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
-  simp [mem_iff_contains, contains_erase h]
+  simp [← contains_iff_mem, contains_erase h]
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.erase k).contains a → m.contains a := by
@@ -235,7 +239,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF)
 
 theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     a ∈ m.erase k → a ∈ m := by
-  simpa [mem_iff_contains] using contains_of_contains_erase h
+  simpa [← contains_iff_mem] using contains_of_contains_erase h
 
 theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.erase k).size = if k ∈ m then m.size - 1 else m.size := by
@@ -298,17 +302,26 @@ theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
     m.contains a = (m.get? a).isSome := by
   simp_to_raw using Raw₀.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_eq_contains [LawfulBEq α] (h : m.WF) {a : α} :
+    (m.get? a).isSome = m.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 theorem mem_iff_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
     a ∈ m ↔ (m.get? a).isSome := by
   simp only [mem_iff_contains, Bool.coe_iff_coe]
   simp_to_raw using Raw₀.contains_eq_isSome_get?
 
+@[simp]
+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_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
 
 theorem get?_eq_none [LawfulBEq α] (h : m.WF) {a : α} : ¬a ∈ m → m.get? a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [LawfulBEq α] (h : m.WF) {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a := by
@@ -351,18 +364,28 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
     m.contains a = (get? m a).isSome := by
   simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    (get? m a).isSome = m.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     a ∈ m ↔ (get? m a).isSome := by
   simp only [mem_iff_contains, Bool.coe_iff_coe]
   simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
 
+@[simp]
+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_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
 
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     ¬a ∈ m → get? m a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     Const.get? (m.erase k) a = if k == a then none else get? m a := by
@@ -484,7 +507,7 @@ theorem get!_eq_default_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α}
 
 theorem get!_eq_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
     ¬a ∈ m → m.get! a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
+  simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] :
     (m.erase k).get! a = if k == a then default else m.get! a := by
@@ -501,7 +524,7 @@ theorem get?_eq_some_get!_of_contains [LawfulBEq α] (h : m.WF) {a : α} [Inhabi
 
 theorem get?_eq_some_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
     a ∈ m → m.get? a = some (m.get! a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
+  simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains h
 
 theorem get!_eq_get!_get? [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
     m.get! a = (m.get? a).get! := by
@@ -547,7 +570,7 @@ theorem get!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [
 
 theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
     ¬a ∈ m → get! m a = default := by
-  simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
+  simpa [← contains_iff_mem] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k a : α} :
     get! (m.erase k) a = if k == a then default else get! m a := by
@@ -564,7 +587,7 @@ theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabit
 
 theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
     a ∈ m → get? m a = some (get! m a) := by
-  simpa [mem_iff_contains] using get?_eq_some_get!_of_contains h
+  simpa [← contains_iff_mem] using get?_eq_some_get!_of_contains h
 
 theorem get!_eq_get!_get? [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
     get! m a = (get? m a).get! := by
@@ -618,7 +641,7 @@ theorem getD_eq_fallback_of_contains_eq_false [LawfulBEq α] (h : m.WF) {a : α}
 
 theorem getD_eq_fallback [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
     ¬a ∈ m → m.getD a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
+  simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by
@@ -635,7 +658,7 @@ theorem get?_eq_some_getD_of_contains [LawfulBEq α] (h : m.WF) {a : α} {fallba
 
 theorem get?_eq_some_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
     a ∈ m → m.get? a = some (m.getD a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
+  simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains h
 
 theorem getD_eq_getD_get? [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
     m.getD a fallback = (m.get? a).getD fallback := by
@@ -685,7 +708,7 @@ theorem getD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
 
 theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
     ¬a ∈ m → getD m a fallback = fallback := by
-  simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
+  simpa [← contains_iff_mem] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback : β} :
     getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by
@@ -702,7 +725,7 @@ theorem get?_eq_some_getD_of_contains [EquivBEq α] [LawfulHashable α] (h : m.W
 
 theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
     a ∈ m → get? m a = some (getD m a fallback) := by
-  simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h
+  simpa [← contains_iff_mem] using get?_eq_some_getD_of_contains h
 
 theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
     getD m a fallback = (get? m a).getD fallback := by
@@ -756,15 +779,25 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF)
     m.contains a = (m.getKey? a).isSome := by
   simp_to_raw using Raw₀.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  (contains_eq_isSome_getKey? h).symm
+
 theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     a ∈ m ↔ (m.getKey? a).isSome := by
   simp only [mem_iff_contains, Bool.coe_iff_coe]
   simp_to_raw using Raw₀.contains_eq_isSome_getKey?
 
+@[simp]
+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) :
     m.getKey? a = some a' → a' ∈ m := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.contains_of_getKey?_eq_some
 
 theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
@@ -773,7 +806,7 @@ theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (
 
 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
+  simpa [← contains_iff_mem] 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
@@ -879,7 +912,7 @@ theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α
 
 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
+  simpa [← contains_iff_mem] 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
@@ -897,7 +930,7 @@ theorem getKey?_eq_some_getKey!_of_contains [EquivBEq α] [LawfulHashable α] [I
 
 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
+  simpa [← contains_iff_mem] 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
@@ -954,7 +987,7 @@ theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable 
 
 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
+  simpa [← contains_iff_mem] 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
@@ -972,7 +1005,7 @@ theorem getKey?_eq_some_getKeyD_of_contains [EquivBEq α] [LawfulHashable α] (h
 
 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
+  simpa [← contains_iff_mem] 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
@@ -1012,7 +1045,7 @@ theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a :
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
-  simp [mem_iff_contains, contains_insertIfNew h]
+  simp [← contains_iff_mem, contains_insertIfNew h]
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).contains k := by
@@ -1020,7 +1053,7 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {
 
 theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
     k ∈ m.insertIfNew k v := by
-  simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h
+  simpa [← contains_iff_mem, -contains_insertIfNew] using contains_insertIfNew_self h
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
     {v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
@@ -1028,7 +1061,7 @@ theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h :
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
-  simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
+  simpa [← contains_iff_mem, -contains_insertIfNew] using contains_of_contains_insertIfNew h
 
 /-- This is a restatement of `contains_of_contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `get_insertIfNew`. -/
@@ -1041,7 +1074,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h :
 in the statement of `get_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
-  simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
+  simpa [← contains_iff_mem] using contains_of_contains_insertIfNew' h
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := by
@@ -1185,7 +1218,7 @@ theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
 
 theorem mem_of_mem_keys [EquivBEq α] [LawfulHashable α] {k : α}
     (h : m.WF) (h' : k ∈ m.keys) : k ∈ m := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.contains_of_mem_keys
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
@@ -1482,7 +1515,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List ((a : α) × β a)} {k : α} :
     k ∈ (m.insertMany l) ↔ k ∈ m ∨ (l.map Sigma.fst).contains k := by
-  simp [mem_iff_contains, contains_insertMany_list h]
+  simp [← contains_iff_mem, contains_insertMany_list h]
 
 theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List ((a : α) × β a)} {k : α} :
@@ -1685,7 +1718,7 @@ theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List (α × β)} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k := by
-  simp [mem_iff_contains, contains_insertMany_list h]
+  simp [← contains_iff_mem, contains_insertMany_list h]
 
 theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List (α × β)} {k : α} :
@@ -1762,7 +1795,7 @@ theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (∀ (a : α), a ∈ m → (l.map Prod.fst).contains a = false) →
       (insertMany m l).size = m.size + l.length := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.Const.size_insertMany_list
 
 theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
@@ -1882,12 +1915,12 @@ theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h :
 theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} {k : α} :
     k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k := by
-  simp [mem_iff_contains, contains_insertManyIfNewUnit_list h]
+  simp [← contains_iff_mem, contains_insertManyIfNewUnit_list h]
 
 theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
     k ∈ insertManyIfNewUnit m l → k ∈ m := by
-  simp only [mem_iff_contains]
+  simp only [← contains_iff_mem]
   simp_to_raw using Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list
 
 theorem mem_insertManyIfNewUnit_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
@@ -2470,7 +2503,7 @@ theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (
 
 theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) :
     k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m := by
-  simp [mem_iff_contains, contains_alter h]
+  simp [← contains_iff_mem, contains_alter h]
 
 theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF)
     (he : k == k') : k' ∈ m.alter k f ↔ (f (m.get? k)).isSome := by
@@ -3584,7 +3617,7 @@ theorem isSome_apply_of_mem_filterMap [EquivBEq α] [LawfulHashable α]
     ∀ (h' : k ∈ m.filterMap f),
       (f (m.getKey k (mem_of_mem_filterMap h h'))
         (Const.get m k (mem_of_mem_filterMap h h'))).isSome := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.Const.isSome_apply_of_contains_filterMap
 
 @[simp]
@@ -3750,7 +3783,7 @@ theorem filter_equiv_self_iff [LawfulBEq α]
 theorem filter_key_equiv_self_iff [EquivBEq α] [LawfulHashable α]
     {f : (a : α) → Bool} (h : m.WF) :
     m.filter (fun k _ => f k) ~m m ↔ ∀ k h, f (m.getKey k h) = true := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.filter_key_equiv_self_iff
 
 theorem size_filter_key_eq_size_iff [EquivBEq α] [LawfulHashable α]
@@ -3869,7 +3902,7 @@ theorem filter_equiv_self_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} (h : m.WF) :
     m.filter f ~m m ↔ ∀ (a : α) (h : a ∈ m),
       f (m.getKey a h) (Const.get m a h) := by
-  simp [mem_iff_contains]
+  simp [← contains_iff_mem]
   simp_to_raw using Raw₀.Const.filter_equiv_self_iff
 
 theorem get?_filter [EquivBEq α] [LawfulHashable α]
diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean
index e0f5a40b17..ef5b7e56fd 100644
--- a/src/Std/Data/DTreeMap/Internal/Queries.lean
+++ b/src/Std/Data/DTreeMap/Internal/Queries.lean
@@ -42,6 +42,9 @@ instance [Ord α] : Membership α (Impl α β) where
 theorem mem_iff_contains {_ : Ord α} {t : Impl α β} {k : α} : k ∈ t ↔ t.contains k :=
   Iff.rfl
 
+theorem contains_iff_mem {_ : Ord α} {t : Impl α β} {k : α} : t.contains k ↔ k ∈ t :=
+  Iff.rfl
+
 instance [Ord α] {m : Impl α β} {a : α} : Decidable (a ∈ m) :=
   inferInstanceAs <| Decidable (m.contains a)
 
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index d0e46cc08f..5d46d35fd6 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -41,6 +41,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   Impl.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  Impl.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   Impl.contains_congr t.wf hab
@@ -231,10 +235,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   Impl.contains_eq_isSome_get? t.wf
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
+    (t.get? a).isSome = t.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     a ∈ t ↔ (t.get? a).isSome :=
   Impl.mem_iff_isSome_get? t.wf
 
+@[simp]
+theorem isSome_get?_iff_mem [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
+    (t.get? a).isSome ↔ a ∈ t :=
+  mem_iff_isSome_get?.symm
+
 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
@@ -279,10 +293,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
     t.contains a = (get? t a).isSome :=
   Impl.Const.contains_eq_isSome_get? t.wf
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
+    (get? t a).isSome = t.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} :
     a ∈ t ↔ (get? t a).isSome :=
   Impl.Const.mem_iff_isSome_get? t.wf
 
+@[simp]
+theorem isSome_get?_iff_mem [TransCmp cmp] {a : α} :
+    (get? t a).isSome ↔ a ∈ t :=
+  mem_iff_isSome_get?.symm
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → get? t a = none :=
   Impl.Const.get?_eq_none_of_contains_eq_false t.wf
@@ -631,10 +655,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
     t.contains a = (t.getKey? a).isSome :=
   Impl.contains_eq_isSome_getKey? t.wf
 
+@[simp]
+theorem isSome_getKey?_eq_contains [TransCmp cmp] {a : α} :
+    (t.getKey? a).isSome = t.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
     a ∈ t ↔ (t.getKey? a).isSome :=
   Impl.mem_iff_isSome_getKey? t.wf
 
+@[simp]
+theorem isSome_getKey?_iff_mem [TransCmp cmp] {a : α} :
+    (t.getKey? a).isSome ↔ a ∈ t :=
+  mem_iff_isSome_getKey?.symm
+
 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
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index fa7110e3d0..0e1a2b652e 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -42,6 +42,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   Impl.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  Impl.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   Impl.contains_congr h hab
@@ -232,10 +236,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a :
     t.contains a = (t.get? a).isSome :=
   Impl.contains_eq_isSome_get? h
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
+    (t.get? a).isSome = t.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ (t.get? a).isSome :=
   Impl.mem_iff_isSome_get? h
 
+@[simp]
+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_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
@@ -280,10 +294,20 @@ theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = (get? t a).isSome :=
   Impl.Const.contains_eq_isSome_get? h
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
+    (get? t a).isSome = t.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 theorem mem_iff_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ (get? t a).isSome :=
   Impl.Const.mem_iff_isSome_get? h
 
+@[simp]
+theorem isSome_get?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
+    (get? t a).isSome ↔ a ∈ t :=
+  (mem_iff_isSome_get? h).symm
+
 theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = false → get? t a = none :=
   Impl.Const.get?_eq_none_of_contains_eq_false h
@@ -634,10 +658,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = (t.getKey? a).isSome :=
   Impl.contains_eq_isSome_getKey? h
 
+@[simp]
+theorem isSome_getKey?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
+    (t.getKey? a).isSome = t.contains a :=
+  (contains_eq_isSome_getKey? h).symm
+
 theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ (t.getKey? a).isSome :=
   Impl.mem_iff_isSome_getKey? h
 
+@[simp]
+theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
+    (t.getKey? a).isSome ↔ a ∈ t :=
+  (mem_iff_isSome_getKey? h).symm
+
 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
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index 3c76244430..e00a86c35f 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -51,6 +51,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
+@[simp]
+theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
+  Iff.rfl
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
   m.inductionOn fun _ => DHashMap.contains_congr hab
 
@@ -140,7 +144,7 @@ theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
-  simp [mem_iff_contains, contains_erase]
+  simp [← contains_iff_mem, contains_erase]
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).contains a → m.contains a :=
@@ -193,15 +197,23 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
 theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
   m.inductionOn fun _ => DHashMap.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [LawfulBEq α] {a : α} : a ∈ m ↔ (m.get? a).isSome :=
   m.inductionOn fun _ => DHashMap.mem_iff_isSome_get?
 
+@[simp]
+theorem isSome_get?_iff_mem [LawfulBEq α] {a : α} : (m.get? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 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
 
 theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
@@ -232,15 +244,25 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (get? m a).isSome :=
   m.inductionOn fun _ => DHashMap.Const.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (get? m a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ (get? m a).isSome :=
   m.inductionOn fun _ => DHashMap.Const.mem_iff_isSome_get?
 
+@[simp]
+theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (get? m a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 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
 
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → get? m a = none := by
-  simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
+  simpa [← contains_iff_mem] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     Const.get? (m.erase k) a = if k == a then none else get? m a :=
@@ -569,10 +591,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.getKey? a).isSome :=
   m.inductionOn fun _ => DHashMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.getKey? a).isSome :=
   m.inductionOn fun _ => DHashMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_getKey?.symm
+
 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
diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
index 01370e6545..c1a4f5a95b 100644
--- a/src/Std/Data/ExtHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -55,6 +55,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   ExtDHashMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
+  Iff.rfl
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   ExtDHashMap.contains_congr hab
@@ -204,10 +208,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = m[a]?.isSome :=
   ExtDHashMap.Const.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    m[a]?.isSome = m.contains a :=
+  contains_eq_isSome_getElem?.symm
+
 theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ m[a]?.isSome :=
   ExtDHashMap.Const.mem_iff_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    m[a]?.isSome ↔ a ∈ m :=
+  mem_iff_isSome_getElem?.symm
+
 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
@@ -381,10 +395,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.getKey? a).isSome :=
   ExtDHashMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.getKey? a).isSome :=
   ExtDHashMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_getKey?.symm
+
 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
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
index 6fa412b893..178efcab54 100644
--- a/src/Std/Data/ExtHashSet/Lemmas.lean
+++ b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -55,6 +55,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   ExtHashMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
+  ExtHashMap.contains_iff_mem
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   ExtHashMap.contains_congr hab
@@ -184,10 +188,20 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.get? a).isSome :=
   ExtHashMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.get? a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.get? a).isSome :=
   ExtHashMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.get? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = false → m.get? a = none :=
   ExtHashMap.getKey?_eq_none_of_contains_eq_false
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 72b21d8d3f..a8f0af8d3a 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -52,6 +52,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
 theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
   DHashMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
+  DHashMap.contains_iff_mem
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   DHashMap.contains_congr hab
@@ -258,10 +262,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = m[a]?.isSome :=
   DHashMap.Const.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    m[a]?.isSome = m.contains a :=
+  contains_eq_isSome_getElem?.symm
+
 theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ m[a]?.isSome :=
   DHashMap.Const.mem_iff_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    m[a]?.isSome ↔ a ∈ m :=
+  mem_iff_isSome_getElem?.symm
+
 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
@@ -469,10 +483,20 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.getKey? a).isSome :=
   DHashMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.getKey? a).isSome :=
   DHashMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.getKey? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_getKey?.symm
+
 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
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 866a20ec03..9dc2564e24 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -68,6 +68,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
 theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
   DHashMap.Raw.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
+  DHashMap.Raw.contains_iff_mem
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   DHashMap.Raw.contains_congr h.out hab
@@ -274,10 +278,20 @@ theorem contains_eq_isSome_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF)
     m.contains a = m[a]?.isSome :=
   DHashMap.Raw.Const.contains_eq_isSome_get? h.out
 
+@[simp]
+theorem isSome_getElem?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    m[a]?.isSome = m.contains a :=
+  (contains_eq_isSome_getElem? h).symm
+
 theorem mem_iff_isSome_getElem? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     a ∈ m ↔ (m[a]?).isSome :=
   DHashMap.Raw.Const.mem_iff_isSome_get? h.out
 
+@[simp]
+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_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
@@ -487,6 +501,11 @@ theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF)
     m.contains a = (m.getKey? a).isSome :=
   DHashMap.Raw.contains_eq_isSome_getKey? h.out
 
+@[simp]
+theorem isSome_getKey?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    (m.getKey? a).isSome = m.contains a :=
+  (contains_eq_isSome_getKey? h).symm
+
 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
@@ -533,6 +552,11 @@ theorem mem_iff_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
     a ∈ m ↔ (m.getKey? a).isSome :=
   DHashMap.Raw.mem_iff_isSome_getKey? h.out
 
+@[simp]
+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) :
     m.getKey? a = some a' → a' ∈ m :=
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 51fb5917e4..da9ed00492 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -50,6 +50,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a)
 theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
   HashMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
+  HashMap.contains_iff_mem
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   HashMap.contains_congr hab
@@ -235,10 +239,20 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.get? a).isSome :=
   HashMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.get? a).isSome = m.contains a :=
+  contains_eq_isSome_get?.symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     a ∈ m ↔ (m.get? a).isSome :=
   HashMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_get?_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} :
+    (m.get? a).isSome ↔ a ∈ m :=
+  mem_iff_isSome_get?.symm
+
 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
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index a220b40a56..4188f5a0f4 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -68,6 +68,10 @@ theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
 theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
   HashMap.Raw.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
+  HashMap.Raw.contains_iff_mem
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   HashMap.Raw.contains_congr h.out hab
@@ -246,10 +250,20 @@ 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
 
+@[simp]
+theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    (m.get? a).isSome = m.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 theorem mem_iff_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     a ∈ m ↔ (m.get? a).isSome :=
   HashMap.Raw.mem_iff_isSome_getKey? h.out
 
+@[simp]
+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_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
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index dea6db9163..bea3fed741 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -38,6 +38,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   DTreeMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  DTreeMap.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   DTreeMap.contains_congr hab
@@ -231,10 +235,20 @@ theorem contains_eq_isSome_getElem? [TransCmp cmp] {a : α} :
     t.contains a = t[a]?.isSome :=
   DTreeMap.Const.contains_eq_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_eq_contains [TransCmp cmp] {a : α} :
+    t[a]?.isSome = t.contains a :=
+  contains_eq_isSome_getElem?.symm
+
 theorem mem_iff_isSome_getElem? [TransCmp cmp] {a : α} :
     a ∈ t ↔ t[a]?.isSome :=
   DTreeMap.Const.mem_iff_isSome_get?
 
+@[simp]
+theorem isSome_getElem?_iff_mem [TransCmp cmp] {a : α} :
+    t[a]?.isSome ↔ a ∈ t :=
+  mem_iff_isSome_getElem?.symm
+
 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
@@ -423,10 +437,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] {a : α} :
     t.contains a = (t.getKey? a).isSome :=
   DTreeMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_eq_contains [TransCmp cmp] {a : α} :
+    (t.getKey? a).isSome = t.contains a :=
+  contains_eq_isSome_getKey?.symm
+
 theorem mem_iff_isSome_getKey? [TransCmp cmp] {a : α} :
     a ∈ t ↔ (t.getKey? a).isSome :=
   DTreeMap.mem_iff_isSome_getKey?
 
+@[simp]
+theorem isSome_getKey?_iff_mem [TransCmp cmp] {a : α} :
+    (t.getKey? a).isSome ↔ a ∈ t :=
+  mem_iff_isSome_getKey?.symm
+
 theorem getKey?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} :
     t.contains a = false → t.getKey? a = none :=
   DTreeMap.getKey?_eq_none_of_contains_eq_false
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index e6c79a8087..8f1747c0c5 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -39,6 +39,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   DTreeMap.Raw.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  DTreeMap.Raw.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   DTreeMap.Raw.contains_congr h hab
@@ -232,10 +236,20 @@ theorem contains_eq_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = t[a]?.isSome :=
   DTreeMap.Raw.Const.contains_eq_isSome_get? h
 
+@[simp]
+theorem isSome_getElem?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
+    t[a]?.isSome = t.contains a :=
+  (contains_eq_isSome_getElem? h).symm
+
 theorem mem_iff_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ t[a]?.isSome :=
   DTreeMap.Raw.Const.mem_iff_isSome_get? h
 
+@[simp]
+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_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
@@ -424,10 +438,20 @@ theorem contains_eq_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = (t.getKey? a).isSome :=
   DTreeMap.Raw.contains_eq_isSome_getKey? h
 
+@[simp]
+theorem isSome_getKey?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
+    (t.getKey? a).isSome = t.contains a :=
+  (contains_eq_isSome_getKey? h).symm
+
 theorem mem_iff_isSome_getKey? [TransCmp cmp] (h : t.WF) {a : α} :
     a ∈ t ↔ (t.getKey? a).isSome :=
   DTreeMap.Raw.mem_iff_isSome_getKey? h
 
+@[simp]
+theorem isSome_getKey?_iff_mem [TransCmp cmp] (h : t.WF) {a : α} :
+    (t.getKey? a).isSome ↔ a ∈ t :=
+  (mem_iff_isSome_getKey? h).symm
+
 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
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index bf095ef6e5..b3d3cc8511 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -38,6 +38,10 @@ theorem isEmpty_insert [TransCmp cmp] {k : α} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   TreeMap.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  TreeMap.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   TreeMap.contains_congr hab
@@ -207,6 +211,11 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   TreeMap.contains_eq_isSome_getKey?
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
+    (t.get? a).isSome = t.contains a :=
+  contains_eq_isSome_get?.symm
+
 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
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index b1e832deb0..c7a97897bf 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -39,6 +39,10 @@ theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} :
 theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
   TreeMap.Raw.mem_iff_contains
 
+@[simp]
+theorem contains_iff_mem {k : α} : t.contains k ↔ k ∈ t :=
+  TreeMap.Raw.contains_iff_mem
+
 theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   TreeMap.Raw.contains_congr h hab
@@ -208,6 +212,11 @@ theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = (t.get? a).isSome :=
   TreeMap.Raw.contains_eq_isSome_getKey? h
 
+@[simp]
+theorem isSome_get?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
+    (t.get? a).isSome = t.contains a :=
+  (contains_eq_isSome_get? h).symm
+
 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