From 501ea674ce241b249c1b4607196659d9c1fa4ab8 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Tue, 12 Nov 2024 20:03:51 +0100
Subject: [PATCH] Fix some proofs

---
 tests/lean/Hashmap/Properties.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 51e46f3f..9cb69054 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -943,10 +943,8 @@ theorem insert_spec {α} (hm : HashMap α) (key : Usize) (value : α)
   split
   . split
     . simp_all (config := {maxDischargeDepth := 1})
-      tauto
     . progress as ⟨ hm2 ⟩
       simp_all (config := {maxDischargeDepth := 1})
-      tauto
   . simp_all (config := {maxDischargeDepth := 1})
 
 @[pspec]