Hotfix for build after rebase

leanprover · Nov 27, 2024 · cea3723 · cea3723
1 parent 77bc339
commit cea3723
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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