diff --git a/src/Init/Data/BEq.lean b/src/Init/Data/BEq.lean
index ed1ac94f76..e72f325629 100644
--- a/src/Init/Data/BEq.lean
+++ b/src/Init/Data/BEq.lean
@@ -49,6 +49,14 @@ theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = fal
 theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
   PartialEquivBEq.trans
 
+theorem BEq.congr_left [BEq α] [PartialEquivBEq α] {a b c : α} (h : a == b) :
+    (a == c) = (b == c) :=
+  Bool.eq_iff_iff.mpr ⟨BEq.trans (BEq.symm h), BEq.trans h⟩
+
+theorem BEq.congr_right [BEq α] [PartialEquivBEq α] {a b c : α} (h : b == c) :
+    (a == b) = (a == c) :=
+  Bool.eq_iff_iff.mpr ⟨fun h' => BEq.trans h' h, fun h' => BEq.trans h' (BEq.symm h)⟩
+
 theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
     (a == b) = false → b == c → (a == c) = false :=
   fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 5d68f7b763..790672d486 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -354,7 +354,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α}
 theorem get_eq_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : get m a h = m.get a h := by
   simp_to_model using List.getValue_eq_getValueCast
 
-theorem get_congr [LawfulBEq α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
+theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
     get m a h' = get m b ((contains_congr _ h hab).symm.trans h') := by
   simp_to_model using List.getValue_congr
 
@@ -582,6 +582,19 @@ theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α}
     m.contains a = false → m.getKey? a = none := by
   simp_to_model using List.getKey?_eq_none
 
+theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
+    (m.getKey? a).all (· == a) := by
+  simp_to_model using List.getKey?_beq
+
+theorem getKey?_eq_some [LawfulBEq α] (h : m.1.WF) {a : α} :
+    m.contains a → m.getKey? a = some a := by
+  simp_to_model using List.getKey?_eq_some
+
+theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k k' : α} (h : k == k') :
+    m.getKey? k = m.getKey? k' := by
+  simp_to_model using List.getKey?_congr
+
 theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
     (m.erase k).getKey? a = if k == a then none else m.getKey? a := by
   simp_to_model [erase] using List.getKey?_eraseKey
@@ -607,6 +620,19 @@ theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {
     (m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h') := by
   simp_to_model [erase] using List.getKey_eraseKey
 
+theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} (h' : m.contains a) :
+    m.getKey a h' == a := by
+  simp_to_model using List.getKey_beq
+
+@[simp]
+theorem getKey_eq [LawfulBEq α] (h : m.1.WF) {a : α} (h' : m.contains a) : m.getKey a h' = a := by
+  simp_to_model using List.getKey_eq
+
+theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k k' : α} (h' : k == k') (h'' : m.contains k) :
+    m.getKey k h'' = m.getKey k' ((contains_congr _ h h').symm.trans h'') := by
+  simp_to_model using List.getKey_congr
+
 theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h'} :
     m.getKey? a = some (m.getKey a h') := by
   simp_to_model using List.getKey?_eq_some_getKey
@@ -652,6 +678,14 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
     m.getKey a h = m.getKey! a := by
   simp_to_model using List.getKey_eq_getKey!
 
+theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
+    {k k' : α} (h : k == k') : m.getKey! k = m.getKey! k' := by
+  simp_to_model using List.getKey!_congr
+
+theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.1.WF) {k : α} :
+    m.contains k → m.getKey! k = k := by
+  simp_to_model using List.getKey!_eq_of_containsKey
+
 theorem getKeyD_empty {a : α} {fallback : α} {c} :
     (empty c : Raw₀ α β).getKeyD a fallback = fallback := by
   simp [getKeyD, empty]
@@ -699,6 +733,14 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
     m.getKey! a = m.getKeyD a default := by
   simp_to_model using List.getKey!_eq_getKeyD_default
 
+theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k k' fallback : α} (h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback := by
+  simp_to_model using List.getKeyD_congr
+
+theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.1.WF) {k fallback : α} :
+    m.contains k → m.getKeyD k fallback = k := by
+  simp_to_model using List.getKeyD_eq_of_containsKey
+
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).1.isEmpty = false := by
   simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index c606e41615..b2a979d619 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -334,7 +334,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h} :
 theorem get_eq_get [LawfulBEq α] {a : α} {h} : get m a h = m.get a h :=
   Raw₀.Const.get_eq_get ⟨m.1, _⟩ m.2
 
-theorem get_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
+theorem get_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h'} :
     get m a h' = get m b ((mem_congr hab).1 h') :=
   Raw₀.Const.get_congr ⟨m.1, _⟩ m.2 hab
 
@@ -641,6 +641,21 @@ theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
 theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
   Raw₀.getKey?_erase_self ⟨m.1, _⟩ m.2
 
+theorem getKey?_beq [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m.getKey? k).all (· == k) :=
+  Raw₀.getKey?_beq ⟨m.1, _⟩ m.2
+
+theorem getKey?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
+    m.getKey? k = m.getKey? k' :=
+  Raw₀.getKey?_congr ⟨m.1, _⟩ m.2 h
+
+theorem getKey?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) :
+    m.getKey? k = some k :=
+  Raw₀.getKey?_eq_some ⟨m.1, _⟩ m.2 h
+
+theorem getKey?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey? k = some k := by
+  simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
+
 theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁} :
     (m.insert k v).getKey a h₁ =
       if h₂ : k == a then
@@ -664,6 +679,16 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α}
     m.getKey? a = some (m.getKey a h) :=
   Raw₀.getKey?_eq_some_getKey ⟨m.1, _⟩ m.2
 
+theorem getKey_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.getKey k h == k :=
+  Raw₀.getKey_beq ⟨m.1, _⟩ m.2 h
+
+theorem getKey_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
+    (h₁ : k₁ ∈ m) : m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h).mp h₁) :=
+  Raw₀.getKey_congr ⟨m.1, _⟩ m.2 h h₁
+
+theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
+  Raw₀.getKey_eq ⟨m.1, _⟩ m.2 h
+
 @[simp]
 theorem getKey!_empty [Inhabited α] {a : α} {c} :
     (empty c : DHashMap α β).getKey! a = default :=
@@ -722,6 +747,17 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a :
     m.getKey a h = m.getKey! a :=
   Raw₀.getKey_eq_getKey! ⟨m.1, _⟩ m.2
 
+theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
+    m.getKey! k = m.getKey! k' :=
+  Raw₀.getKey!_congr ⟨m.1, _⟩ m.2 h
+
+theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) :
+    m.getKey! k = k :=
+  Raw₀.getKey!_eq_of_contains ⟨m.1, _⟩ m.2 h
+
+theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.getKey! k = k :=
+  getKey!_eq_of_contains h
+
 @[simp]
 theorem getKeyD_empty {a fallback : α} {c} :
     (empty c : DHashMap α β).getKeyD a fallback = fallback :=
@@ -784,6 +820,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
     m.getKey! a = m.getKeyD a default :=
   Raw₀.getKey!_eq_getKeyD_default ⟨m.1, _⟩ m.2
 
+theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
+    (h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
+  Raw₀.getKeyD_congr ⟨m.1, _⟩ m.2 h
+
+theorem getKeyD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
+    m.getKeyD k fallback = k :=
+  Raw₀.getKeyD_eq_of_contains ⟨m.1, _⟩ m.2 h
+
+theorem getKeyD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) :
+    m.getKeyD k fallback = k :=
+  getKeyD_eq_of_contains h
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     (m.insertIfNew k v).isEmpty = false :=
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index db20deea46..dd1921485e 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -411,7 +411,7 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {
 theorem get_eq_get [LawfulBEq α] (h : m.WF) {a : α} {h} : get m a h = m.get a h := by
   simp_to_raw using Raw₀.Const.get_eq_get
 
-theorem get_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
+theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
     get m a h' = get m b ((mem_congr h hab).1 h') := by
   simp_to_raw using Raw₀.Const.get_congr
 
@@ -719,6 +719,22 @@ theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     (m.erase k).getKey? k = none := by
   simp_to_raw using Raw₀.getKey?_erase_self
 
+theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
+    (m.getKey? a).all (· == a) := by
+  simp_to_raw using Raw₀.getKey?_beq
+
+theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
+    m.getKey? k = m.getKey? k' := by
+  simp_to_raw using Raw₀.getKey?_congr
+
+theorem getKey?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} :
+    m.contains k → m.getKey? k = some k := by
+  simp_to_raw using Raw₀.getKey?_eq_some
+
+theorem getKey?_eq_some [LawfulBEq α] (h : m.WF) {k : α} :
+    k ∈ m → m.getKey? k = some k := by
+  simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
+
 theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁} :
     (m.insert k v).getKey a h₁ =
       if h₂ : k == a then
@@ -741,6 +757,19 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
     m.getKey? a = some (m.getKey a h) := by
   simp_to_raw using Raw₀.getKey?_eq_some_getKey
 
+theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} (h') :
+    m.getKey a h' == a := by
+  simp_to_raw using Raw₀.getKey_beq
+
+theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
+    (h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
+    m.getKey k₁ h₁ = m.getKey k₂ (((mem_congr h h').mp h₁)) := by
+  simp_to_raw using Raw₀.getKey_congr
+
+theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h') :
+    m.getKey k h' = k := by
+  simp_to_raw using Raw₀.getKey_eq
+
 @[simp]
 theorem getKey!_empty [Inhabited α] {a : α} {c} :
     (empty c : Raw α β).getKey! a = default := by
@@ -800,6 +829,18 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
     m.getKey a h = m.getKey! a := by
   simp_to_raw using Raw₀.getKey_eq_getKey!
 
+theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
+    {k₁ k₂ : α} (h' : k₁ == k₂) : m.getKey! k₁ = m.getKey! k₂ := by
+  simp_to_raw using Raw₀.getKey!_congr
+
+theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} :
+    m.contains k → m.getKey! k = k := by
+  simp_to_raw using Raw₀.getKey!_eq_of_contains
+
+theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} :
+    k ∈ m → m.getKey! k = k := by
+  simpa only [mem_iff_contains] using getKey!_eq_of_contains h
+
 @[simp]
 theorem getKeyD_empty {a fallback : α} {c} :
     (empty c : Raw α β).getKeyD a fallback = fallback := by
@@ -864,6 +905,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
     m.getKey! a = m.getKeyD a default := by
   simp_to_raw using Raw₀.getKey!_eq_getKeyD_default
 
+theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ fallback : α}
+    (h' : k₁ == k₂) : m.getKeyD k₁ fallback = m.getKeyD k₂ fallback := by
+  simp_to_raw using Raw₀.getKeyD_congr
+
+theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} :
+    m.contains k → m.getKeyD k fallback = k := by
+  simp_to_raw using Raw₀.getKeyD_eq_of_contains
+
+theorem getKeyD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} :
+    k ∈ m → m.getKeyD k fallback = k := by
+  simpa only [mem_iff_contains] using getKeyD_eq_of_contains h
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
     (m.insertIfNew k v).isEmpty = false := by
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 74c057c54a..6146c65fa1 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -269,7 +269,7 @@ theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] {a : α} {h'
     m[a]? = some (m[a]'h') :=
   @DHashMap.Const.get?_eq_some_get _ _ _ _ _ _ _ _ h'
 
-theorem getElem_congr [LawfulBEq α] {a b : α} (hab : a == b) {h'} :
+theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h'} :
     m[a]'h' = m[b]'((mem_congr hab).1 h') :=
   DHashMap.Const.get_congr hab (h' := h')
 
@@ -434,6 +434,20 @@ theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
 theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none :=
   DHashMap.getKey?_erase_self
 
+theorem getKey?_beq [EquivBEq α] [LawfulHashable α] {k : α} : (m.getKey? k).all (· == k) :=
+  DHashMap.getKey?_beq
+
+theorem getKey?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
+    m.getKey? k = m.getKey? k' :=
+  DHashMap.getKey?_congr h
+
+theorem getKey?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) :
+    m.getKey? k = some k :=
+  DHashMap.getKey?_eq_some h
+
+theorem getKey?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey? k = some k := by
+  simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
+
 theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insert k v)[a]'h₁ =
       if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
@@ -453,6 +467,16 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] {a : α} {h' :
     m.getKey? a = some (m.getKey a h') :=
   @DHashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
 
+theorem getKey_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.getKey k h == k :=
+  DHashMap.getKey_beq h
+
+theorem getKey_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
+    (h₁ : k₁ ∈ m) : m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h).mp h₁) :=
+  DHashMap.getKey_congr h h₁
+
+theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
+  DHashMap.getKey_eq h
+
 @[simp]
 theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default :=
   DHashMap.getKey!_empty
@@ -507,6 +531,17 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a :
     m.getKey a h' = m.getKey! a :=
   @DHashMap.getKey_eq_getKey! _ _ _ _ _ _ _ _ _ h'
 
+theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
+    m.getKey! k = m.getKey! k' :=
+  DHashMap.getKey!_congr h
+
+theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) :
+    m.getKey! k = k :=
+  DHashMap.getKey!_eq_of_contains h
+
+theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.getKey! k = k :=
+  DHashMap.getKey!_eq_of_mem h
+
 @[simp]
 theorem getKeyD_empty {a : α} {fallback : α} {c} :
     (empty c : HashMap α β).getKeyD a fallback = fallback :=
@@ -566,6 +601,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
     m.getKey! a = m.getKeyD a default :=
   DHashMap.getKey!_eq_getKeyD_default
 
+theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
+    (h : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
+  DHashMap.getKeyD_congr h
+
+theorem getKeyD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
+    m.getKeyD k fallback = k :=
+  DHashMap.getKeyD_eq_of_contains h
+
+theorem getKeyD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) :
+    m.getKeyD k fallback = k :=
+  DHashMap.getKeyD_eq_of_mem h
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insertIfNew k v).isEmpty = false :=
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index e0d06f9942..5d48918580 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -282,7 +282,7 @@ theorem getElem?_eq_some_getElem [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
     m[a]? = some (m[a]'h') :=
   @DHashMap.Raw.Const.get?_eq_some_get _ _ _ _ _ _ _ h.out _ h'
 
-theorem getElem_congr [LawfulBEq α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
+theorem getElem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) {h'} :
     m[a]'h' = m[b]'((mem_congr h hab).1 h') :=
   DHashMap.Raw.Const.get_congr h.out hab (h' := h')
 
@@ -448,6 +448,21 @@ theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     (m.erase k).getKey? k = none :=
   DHashMap.Raw.getKey?_erase_self h.out
 
+theorem getKey?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.getKey? k).all (· == k) :=
+  DHashMap.Raw.getKey?_beq h.out
+
+theorem getKey?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
+    m.getKey? k = m.getKey? k' :=
+  DHashMap.Raw.getKey?_congr h.out h'
+
+theorem getKey?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
+    m.getKey? k = some k :=
+  DHashMap.Raw.getKey?_eq_some_of_contains h.out h'
+
+theorem getKey?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) : m.getKey? k = some k :=
+  DHashMap.Raw.getKey?_eq_some h.out h'
+
 theorem getKey_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁} :
     (m.insert k v).getKey a h₁ =
       if h₂ : k == a then k else m.getKey a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
@@ -467,6 +482,19 @@ theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.WF) {a :
     m.getKey? a = some (m.getKey a h') :=
   @DHashMap.Raw.getKey?_eq_some_getKey _ _ _ _ _ _ _ h.out _ h'
 
+theorem getKey_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m) :
+    m.getKey k h' == k :=
+  DHashMap.Raw.getKey_beq h.out h'
+
+theorem getKey_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
+    (h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
+    m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h h').mp h₁) :=
+  DHashMap.Raw.getKey_congr h.out h' h₁
+
+theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
+    m.getKey k h' = k :=
+  DHashMap.Raw.getKey_eq h.out h'
+
 @[simp]
 theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default :=
   DHashMap.Raw.getKey!_empty
@@ -521,6 +549,18 @@ theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h :
     m.getKey a h' = m.getKey! a :=
   DHashMap.Raw.getKey_eq_getKey! h.out
 
+theorem getKey!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k k' : α}
+    (h' : k == k') : m.getKey! k = m.getKey! k' :=
+  DHashMap.Raw.getKey!_congr h.out h'
+
+theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : m.contains k) :
+    m.getKey! k = k :=
+  DHashMap.Raw.getKey!_eq_of_contains h.out h'
+
+theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) :
+    m.getKey! k = k :=
+  DHashMap.Raw.getKey!_eq_of_mem h.out h'
+
 @[simp]
 theorem getKeyD_empty {a fallback : α} {c} :
     (empty c : Raw α β).getKeyD a fallback = fallback :=
@@ -581,6 +621,18 @@ theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited
     m.getKey! a = m.getKeyD a default :=
   DHashMap.Raw.getKey!_eq_getKeyD_default h.out
 
+theorem getKeyD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' fallback : α}
+    (h' : k == k') : m.getKeyD k fallback = m.getKeyD k' fallback :=
+  DHashMap.Raw.getKeyD_congr h.out h'
+
+theorem getKeyD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : m.contains k) :
+    m.getKeyD k fallback = k :=
+  DHashMap.Raw.getKeyD_eq_of_contains h.out h'
+
+theorem getKeyD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m) :
+    m.getKeyD k fallback = k :=
+  DHashMap.Raw.getKeyD_eq_of_mem h.out h'
+
 @[simp]
 theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
     (m.insertIfNew k v).isEmpty = false :=
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index f99363e566..00ca10878e 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -225,6 +225,19 @@ theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
 theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).get? k = none :=
   HashMap.getKey?_erase_self
 
+theorem get?_beq [EquivBEq α] [LawfulHashable α] {k : α} : (m.get? k).all (· == k) :=
+  HashMap.getKey?_beq
+
+theorem get?_congr [EquivBEq α] [LawfulHashable α] {k k' : α} (h : k == k') :
+    m.get? k = m.get? k' :=
+  HashMap.getKey?_congr h
+
+theorem get?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) : m.get? k = some k :=
+  HashMap.getKey?_eq_some_of_contains h
+
+theorem get?_eq_some_of_mem [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k :=
+  HashMap.getKey?_eq_some_of_contains h
+
 theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
     (m.insert k).get a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
@@ -239,6 +252,16 @@ theorem get?_eq_some_get [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈
     m.get? a = some (m.get a h') :=
   @HashMap.getKey?_eq_some_getKey _ _ _ _ _ _ _ _ h'
 
+theorem get_beq [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) : m.get k h == k :=
+  HashMap.getKey_beq h
+
+theorem get_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ == k₂)
+    (h₁ : k₁ ∈ m) : m.get k₁ h₁ = m.get k₂ ((mem_congr h).mp h₁) :=
+  HashMap.getKey_congr h h₁
+
+theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k :=
+  HashMap.getKey_eq h
+
 @[simp]
 theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default :=
   HashMap.getKey!_empty
@@ -288,6 +311,16 @@ theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h
     m.get a h' = m.get! a :=
   HashMap.getKey_eq_getKey!
 
+theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : k == k') :
+    m.get! k = m.get! k' :=
+  HashMap.getKey!_congr h
+
+theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k) : m.get! k = k :=
+  HashMap.getKey!_eq_of_contains h
+
+theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.get! k = k :=
+  HashMap.getKey!_eq_of_mem h
+
 @[simp]
 theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback :=
   HashMap.getKeyD_empty
@@ -342,6 +375,17 @@ theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a
     m.get! a = m.getD a default :=
   HashMap.getKey!_eq_getKeyD_default
 
+theorem getD_congr [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
+    (h : k == k') : m.getD k fallback = m.getD k' fallback :=
+  HashMap.getKeyD_congr h
+
+theorem getD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k) :
+    m.getD k fallback = k :=
+  HashMap.getKeyD_eq_of_contains h
+
+theorem getD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) : m.getD k fallback = k :=
+  HashMap.getKeyD_eq_of_mem h
+
 @[simp]
 theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.containsThenInsertIfNew_fst
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index d2f3401b75..f81592ba7f 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -234,6 +234,22 @@ theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
   HashMap.Raw.getKey?_erase h.out
 
+theorem get?_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    (m.get? k).all (· == k) :=
+  HashMap.Raw.getKey?_beq h.out
+
+theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} (h' : k == k') :
+    m.get? k = m.get? k' :=
+  HashMap.Raw.getKey?_congr h.out h'
+
+theorem get?_eq_some_of_contains [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
+    m.get? k = some k :=
+  HashMap.Raw.getKey?_eq_some_of_contains h.out h'
+
+theorem get?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
+    m.get? k = some k :=
+  HashMap.Raw.getKey?_eq_some h.out h'
+
 theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
     (m.insert k).get a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
@@ -253,6 +269,19 @@ theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.erase k).get? k = none :=
   HashMap.Raw.getKey?_erase_self h.out
 
+theorem get_beq [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} (h' : k ∈ m) :
+    m.get k h' == k :=
+  HashMap.Raw.getKey_beq h.out h'
+
+theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
+    (h' : k₁ == k₂) (h₁ : k₁ ∈ m) :
+    m.get k₁ h₁ = m.get k₂ (((mem_congr h h').mp h₁)) :=
+  HashMap.Raw.getKey_congr h.out h' h₁
+
+theorem get_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
+    m.get k h' = k :=
+  HashMap.Raw.getKey_eq h.out h'
+
 @[simp]
 theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default :=
   HashMap.Raw.getKey!_empty
@@ -303,6 +332,17 @@ theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
     m.get a h' = m.get! a :=
   HashMap.Raw.getKey_eq_getKey! h.out
 
+theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k k' : α}
+    (h' : k == k') : m.get! k = m.get! k' :=
+  HashMap.Raw.getKey!_congr h.out h'
+
+theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : m.contains k) :
+    m.get! k = k :=
+  HashMap.Raw.getKey!_eq_of_contains h.out h'
+
+theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) : m.get! k = k :=
+  HashMap.Raw.getKey!_eq_of_mem h.out h'
+
 @[simp]
 theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback :=
   HashMap.Raw.getKeyD_empty
@@ -358,6 +398,18 @@ theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h
     m.get! a = m.getD a default :=
   HashMap.Raw.getKey!_eq_getKeyD_default h.out
 
+theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' fallback : α}
+    (h' : k == k') : m.getD k fallback = m.getD k' fallback :=
+  HashMap.Raw.getKeyD_congr h.out h'
+
+theorem getD_eq_of_contains [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : m.contains k) :
+    m.getD k fallback = k :=
+  HashMap.Raw.getKeyD_eq_of_contains h.out h'
+
+theorem getD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m) :
+    m.getD k fallback = k :=
+  HashMap.Raw.getKeyD_eq_of_mem h.out h'
+
 @[simp]
 theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.Raw.containsThenInsertIfNew_fst h.out
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index c8fae5881b..0c81715454 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -580,6 +580,21 @@ theorem getKey?_eq_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
     · rw [getEntry?_cons_of_false h, getKey?_cons_of_false h, ih]
     · rw [getEntry?_cons_of_true h, getKey?_cons_of_true h, Option.map_some']
 
+theorem getKey?_beq [BEq α] {l : List ((a : α) × β a)} {a : α} :
+    (getKey? a l).all (· == a) := by
+  induction l using assoc_induction with
+  | nil => rfl
+  | cons k v l ih =>
+    rw [getKey?_cons, cond_eq_if]
+    split <;> assumption
+
+theorem getKey?_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
+    {k k' : α} (h : k == k') : getKey? k l = getKey? k' l := by
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    rw [getKey?_cons, getKey?_cons, BEq.congr_right h, ih]
+
 theorem containsKey_eq_isSome_getKey? [BEq α] {l : List ((a : α) × β a)} {a : α} :
     containsKey a l = (getKey? a l).isSome := by
   simp [containsKey_eq_isSome_getEntry?, getKey?_eq_getEntry?]
@@ -613,6 +628,23 @@ theorem getKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
   · rfl
   · exact getKey?_eq_some_getKey _
 
+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)
+
+@[simp]
+theorem getKey_eq [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} (h : containsKey a l) :
+    getKey a l h = a := by
+  simpa only [beq_iff_eq] using getKey_beq h
+
+theorem getKey?_eq_some [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
+    (h : containsKey a l) : getKey? a l = some a := by
+  simp only [getKey?_eq_some_getKey h, getKey_eq]
+
+theorem getKey_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
+    {k k' : α} (h : k == k') {h'} {h''} : getKey k l h' = getKey k' l h'' := by
+  simpa only [getKey?_eq_some_getKey, h', h'', Option.some.injEq] using getKey?_congr (l := l) h
+
 /-- Internal implementation detail of the hash map -/
 def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
   (getKey? a l).getD fallback
@@ -635,6 +667,15 @@ theorem getKey_eq_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {
     getKey a l h = getKeyD a l fallback := by
   rw [getKeyD_eq_getKey?, getKey, Option.get_eq_getD]
 
+theorem getKeyD_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
+    {k k' fallback : α} (h : k == k') : getKeyD k l fallback = getKeyD k' l fallback := by
+  simp only [getKeyD_eq_getKey?, getKey?_congr h]
+
+theorem getKeyD_eq_of_containsKey [BEq α] [LawfulBEq α]
+    {l : List ((a : α) × β a)} {k fallback : α} (h : containsKey k l) :
+    getKeyD k l fallback = k := by
+  simp only [← getKey_eq_getKeyD h, getKey_eq]
+
 theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
     (h : containsKey a l = true) :
     getKey? a l = some (getKeyD a l fallback) := by
@@ -661,6 +702,15 @@ theorem getKey_eq_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)}
     (h : containsKey a l = true) : getKey a l h = getKey! a l := by
   rw [getKey!_eq_getKey?, getKey, Option.get_eq_get!]
 
+theorem getKey!_congr [BEq α] [EquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
+    {k k' : α} (h : k == k') : getKey! k l = getKey! k' l := by
+  simp only [getKey!_eq_getKey?, getKey?_congr h]
+
+theorem getKey!_eq_of_containsKey [BEq α] [LawfulBEq α] [Inhabited α]
+    {l : List ((a : α) × β a)} {k : α} (h : containsKey k l) :
+    getKey! k l = k := by
+  simp only [← getKey_eq_getKey! h, getKey_eq]
+
 theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
     (h : containsKey a l = true) :
     getKey? a l = some (getKey! a l) := by
@@ -3260,7 +3310,7 @@ theorem getKey!_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Optio
   · next heq =>
     rfl
 
-theorem getKey_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
+theorem getKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)}
     (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
     getKey k' (alterKey k f l) hc =
       if heq : k == k' then
@@ -3533,7 +3583,7 @@ theorem getKey!_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β
         getKey! k' l := by
   simp [hl, getKey!_eq_getKey?, getKey?_alterKey, apply_ite Option.get!]
 
-theorem getKey_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β}
+theorem getKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β}
     (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
     getKey k' (alterKey k f l) hc =
       if heq : k == k' then
@@ -3719,7 +3769,7 @@ theorem getKey!_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {
     getKey! k (modifyKey k f l) = if containsKey k l then k else default := by
   simp [getKey!_modifyKey, hl]
 
-theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
+theorem getKey_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k}
     (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
     getKey k' (modifyKey k f l) h =
       if k == k' then
@@ -3727,13 +3777,13 @@ theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f :
       else
         haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h
         getKey k' l h' := by
-  simp [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite]
+  simp only [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite]
 
 @[simp]
-theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
-    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
+theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k}
+    (l : List ((a : α) × β a)) (_ : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
     getKey k (modifyKey k f l) h = k := by
-  simp [getKey_modifyKey, hl]
+  simp only [getKey_eq]
 
 theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k}
     (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
@@ -3744,7 +3794,7 @@ theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k
         getKeyD k' l fallback := by
   simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValueCast?, hl]
 
-theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k}
+theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] {k fallback : α} {f : β k → β k}
     (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
     getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by
   simp [getKeyD_modifyKey, hl]
@@ -3884,7 +3934,7 @@ theorem getKey!_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β →
     getKey! k (modifyKey k f l) = if containsKey k l then k else default := by
   simp [getKey!_modifyKey, hl]
 
-theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
+theorem getKey_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
     (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
     getKey k' (modifyKey k f l) h =
       if k == k' then
@@ -3892,11 +3942,11 @@ theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β
       else
         haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h
         getKey k' l h' := by
-  simp [modifyKey_eq_alterKey, getKey_alterKey, hl]
+  simp only [modifyKey_eq_alterKey, getKey_alterKey, hl]
   rfl
 
 @[simp]
-theorem getKey_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β}
+theorem getKey_modifyKey_self [EquivBEq α] {k : α} {f : β → β}
     (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
     getKey k (modifyKey k f l) h = k := by
   simp [getKey_modifyKey, hl]
@@ -3910,7 +3960,7 @@ theorem getKeyD_modifyKey [EquivBEq α] {k k' fallback : α} {f : β → β} (l
         getKeyD k' l fallback := by
   simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValue?, hl]
 
-theorem getKeyD_modifyKey_self [EquivBEq α] [Inhabited α] {k fallback : α} {f : β → β}
+theorem getKeyD_modifyKey_self [EquivBEq α] {k fallback : α} {f : β → β}
     (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
     getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by
   simp [getKeyD_modifyKey, hl]