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/Finite.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'LeanAStar/Finite.lean')

diff --git a/LeanAStar/Finite.lean b/LeanAStar/Finite.lean
index cbd8ee3..e028cf6 100644
--- a/LeanAStar/Finite.lean
+++ b/LeanAStar/Finite.lean
@@ -164,7 +164,7 @@ protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Has
     split
     case h_1 m isLt he =>
       simp at he
-      simp[Std.HashSet.size_insert, Std.HashSet.mem_iff_contains, h₂, he]
+      simp[Std.HashSet.size_insert, h₂, he]
     case h_2 m isLt he =>
       simp
       have h₄ : m < n := have : n = m.succ := Fin.val_eq_of_eq he; this.substr (Nat.lt_succ_self m)
-- 
cgit v1.2.3