diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index 98d9814bf1ae..e4cc4bdfa4fd 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -222,39 +222,13 @@ variable {β : Type v}
 
 theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
     {l : AssocList α (fun _ => β)} : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by
-  rw [Const.alterKey]
-  split
-  · next heq =>
-    induction l
-    · simp only [toList_nil, getValue?_nil] at heq
-      simp only [alter, heq, toList_nil, eraseKey_nil]
-      exact .nil
-    · next ih =>
-      simp only [toList_cons, getValue?_cons, cond_eq_if] at heq
-      split at heq
-      · next heq₂ =>
-        simp only [alter, if_pos heq₂, heq, toList_cons, eraseKey_cons_of_beq heq₂]
-        exact Perm.rfl
-      · next heq₂ =>
-        simp only [alter, if_neg heq₂, toList_cons]
-        simp only [eraseKey_cons_of_false (Bool.not_eq_true _ ▸ heq₂), true_and]
-        exact Perm.cons _ <| ih heq
-  · next heq =>
-    induction l
-    · rw [toList_nil, getValue?_nil] at heq
-      simp only [alter, heq, toList_cons, toList_nil, insertEntry_nil]
-      exact Perm.rfl
-    · next ih =>
-      simp only [toList_cons, getValue?_cons, cond_eq_if] at heq
-      split at heq
-      · next heq₂ =>
-        simp only [alter, heq, if_pos heq₂, toList_cons, insertEntry_cons_of_beq heq₂,
-          List.cons.injEq, and_true]
-        rfl
-      · next heq₂ =>
-        simp only [alter, if_neg heq₂, toList_cons]
-        refine insertEntry_cons_of_false (Bool.not_eq_true _ ▸ heq₂) |>.symm |> Perm.trans ?_
-        exact Perm.cons _ <| ih heq
+  induction l
+  · simp only [alter, toList_nil, alterKey_nil]
+    split <;> simp_all
+  · rw [toList]
+    refine Perm.trans ?_ Const.alterKey_cons_perm.symm
+    rw [alter]
+    split <;> (try split) <;> simp_all
 
 theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β)} :
     modify a f l = alter a (·.map f) l := by
diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 91f38371a645..b2050477d1b4 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -1903,7 +1903,7 @@ theorem alterKey_nil [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Opt
     | none => []
     | some b => [⟨a, b⟩] := rfl
 
-theorem containsKey_alterKey [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
+theorem containsKey_alterKey_self [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)}
     {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
     containsKey a (alterKey a f l) = (f (getValueCast? a l)).isSome := by
   match l with
@@ -1991,8 +1991,8 @@ theorem length_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k)
     simp only [modifyKey]
     split <;> next h => simp only [length_replaceEntry, List.length_cons]
 
-theorem containsKey_modifyKey_iff [BEq α] [LawfulBEq α] (k : α) (f : β k → β k)
-    (l : List ((a : α) × β a)) : containsKey k (modifyKey k f l) ↔ containsKey k l := by
+theorem containsKey_modifyKey_self [BEq α] [LawfulBEq α] (k : α) (f : β k → β k)
+    (l : List ((a : α) × β a)) : containsKey k (modifyKey k f l) = containsKey k l := by
   induction l
   · simp only [modifyKey, getValueCast?_nil, eraseKey_nil, containsKey_nil, Bool.false_eq_true]
   · simp only [modifyKey, Bool.coe_iff_coe]
@@ -2021,6 +2021,26 @@ theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Optio
   cases h : getValue? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry,
     containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none]
 
+theorem alterKey_cons_perm [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β}
+    {k' : α} {v' : β} {l : List ((a : α) × β)} :
+      Perm (alterKey k f (⟨k', v'⟩ :: l)) (if k' == k then
+        match f (some v') with
+          | none => l
+          | some v => ⟨k, v⟩ :: l
+        else
+          ⟨k', v'⟩ :: alterKey k f l) := by
+  rw [alterKey]
+  by_cases hk' : k' == k
+  · simp only [hk', ↓reduceDIte]
+    rw [getValue?_cons_of_true hk', eraseKey_cons_of_beq hk']
+    simp [insertEntry_cons_of_beq hk']
+  · simp only [hk', Bool.false_eq_true, ↓reduceDIte]
+    rw [Bool.not_eq_true] at hk'
+    rw [getValue?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey]
+    split
+    · rfl
+    · simp [insertEntry_cons_of_false hk']
+
 theorem alterKey_of_perm [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
     {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hp : Perm l l') :
     Perm (alterKey a f l) (alterKey a f l') := by
@@ -2042,7 +2062,7 @@ theorem alterKey_nil [BEq α] [EquivBEq α] {a : α} {f : Option β → Option 
     | none => []
     | some b => [⟨a, b⟩] := rfl
 
-theorem containsKey_alterKey_iff [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
+theorem containsKey_alterKey_self [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β}
     {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
     containsKey a (alterKey a f l) ↔ (f (getValue? a l)).isSome := by
   match l with
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index 1b35bf032818..8384a6976db0 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -466,7 +466,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β)
       simp only [AssocList.contains_eq] at h
       simp only [AssocList.modify_eq_alter, Array.set_set, AssocList.contains_eq,
         containsKey_of_perm AssocList.toList_alter, ← modifyKey_eq_alterKey,
-        containsKey_modifyKey_iff, h, ↓reduceIte]
+        containsKey_modifyKey_self, h, ↓reduceIte]
     · rfl
 
 theorem modify_eq_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 015dbb420c52..80287e48ac8d 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -563,7 +563,7 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
       simp only [buckets_withComputedSize]
       simp only [containsKey_of_perm <| toListModel_updateBucket_alter h]
       rw [← getValueCast?_eq_some_getValueCast h₁]
-      conv => lhs; congr; rw [containsKey_alterKey h.distinct];
+      conv => lhs; congr; rw [containsKey_alterKey_self h.distinct];
     · next h₁ =>
       rw [containsₘ_eq_containsKey h] at h₁
       rw [alterKey]
@@ -655,7 +655,7 @@ theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
       simp only [buckets_withComputedSize]
       simp only [containsKey_of_perm <| toListModel_updateBucket_alter h]
       rw [← getValue?_eq_some_getValue h₁]
-      conv => lhs; congr; rw [Const.containsKey_alterKey_iff (a := a) (f := f) h.distinct];
+      conv => lhs; congr; rw [Const.containsKey_alterKey_self h.distinct]
     · next h₁ =>
       rw [containsₘ_eq_containsKey h] at h₁
       rw [Const.alterKey]