fix

kim-em · kim-em · commit 013e98ebc905 · 2025-05-25T15:46:17.000+10:00
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
@@ -278,7 +278,7 @@ theorem ofArray.folder_foldl_mem_of_mem
           · next hfoo =>
             rw [hl]
             cases x
-            simp [Std.HashMap.getElem?_insertIfNew]
+            simp [Std.HashMap.getElem_insertIfNew]
             intro hbar
             exfalso
             apply hfoo
