From eebf50562af5de9779aa11ab2671bc1c917e6000 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 23:39:59 +0200
Subject: Lean 4.20.1

---
 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 302e3b1..cbd8ee3 100644
--- a/LeanAStar/Finite.lean
+++ b/LeanAStar/Finite.lean
@@ -187,7 +187,7 @@ protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Has
         subst n
         have h₂ := h₂ ⟨m+1,h₁⟩ (Fin.le_refl _)
         have hx := Std.HashSet.mem_iff_contains.mp hx
-        exact absurd hx (Bool.eq_false_iff.mp h₂)
+        exact absurd hx h₂
 termination_by _ n => n.val
 
 theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : (Finite.set α).size = Finite.cardinality α := by
-- 
cgit v1.2.3

