diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index befe1fbed638..05c4331d134c 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -2278,9 +2278,9 @@ theorem contains_insertList_of_mem [BEq α] [PartialEquivBEq α] (l toInsert: Li
   rw [containsKey_insertList]
   right
   simp [List.contains_eq_any_beq]
-  exists k
+  exists ⟨k, v⟩
   constructor
-  · exists ⟨k,v⟩
+  · exact mem
   · apply PartialEquivBEq.symm
     exact k_eq