From 7480e42e0a7ef6631b01fb7208b2b3b9c7fcc354 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 13:47:12 +0100
Subject: Lean 4.23

---
 LeanAStar/HashSet.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'LeanAStar/HashSet.lean')

diff --git a/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean
index 87f351a..31691ed 100644
--- a/LeanAStar/HashSet.lean
+++ b/LeanAStar/HashSet.lean
@@ -23,7 +23,7 @@ protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α]
     cases h₄ : set.contains (Finite.nth ⟨0,h₂⟩)
     case false =>
       have h₅ : ∀(o : Fin (Finite.cardinality α)), Finite.nth o ∉ set := by
-        simp[←Bool.not_eq_true, ←HashSet.mem_iff_contains] at h₄
+        simp[←Bool.not_eq_true] at h₄
         intro o
         cases o
         case mk o ho =>
-- 
cgit v1.2.3