From 973225b1c5ed10f2a99374c91a9d6a957067f654 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 18:27:10 +0200
Subject: Lean 4.19

---
 LeanAStar/Finite.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'LeanAStar/Finite.lean')

diff --git a/LeanAStar/Finite.lean b/LeanAStar/Finite.lean
index 4c1455f..302e3b1 100644
--- a/LeanAStar/Finite.lean
+++ b/LeanAStar/Finite.lean
@@ -102,8 +102,8 @@ theorem Finite.forall_nth {α : Type u} [Finite α] (p : α → Prop) (h₁ : 
 
 def Finite.set (α : Type u) [Finite α] [BEq α] [Hashable α] : Std.HashSet α :=
   match h: (Finite.cardinality α) with
-  | 0 => Std.HashSet.empty
-  | l+1 => set_worker Std.HashSet.empty ⟨l,h.substr (p := λx ↦ l < x) $ Nat.lt.base l⟩
+  | 0 => Std.HashSet.emptyWithCapacity
+  | l+1 => set_worker Std.HashSet.emptyWithCapacity ⟨l,h.substr (p := λx ↦ l < x) $ Nat.lt.base l⟩
 where set_worker (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) : Std.HashSet α :=
   let e := Finite.nth n
   let set := set.insert e
@@ -148,7 +148,7 @@ theorem Finite.set_contains (α : Type u) [Finite α] [BEq α] [Hashable α] [La
   case h_2 l h =>
     let o := l - enumerate a
     have h₁ : (Finite.enumerate a).val + o = l := by omega
-    have h₂ := Finite.set_worker_contains _ a Std.HashSet.empty o (by omega)
+    have h₂ := Finite.set_worker_contains _ a Std.HashSet.emptyWithCapacity o (by omega)
     simp[h₁] at h₂
     assumption
 
@@ -196,5 +196,5 @@ theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hasha
   case h_1 h => exact Std.HashSet.size_empty.substr h.symm
   case h_2 l h =>
     rewrite(occs := .pos [3])[h]
-    have := Finite.set_worker_size α Std.HashSet.empty ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λx _↦Bool.eq_false_iff.mp (Std.HashSet.contains_empty (a:=Finite.nth x)))
-    simp only [this, Std.HashSet.size_empty, Nat.zero_add]
+    have := Finite.set_worker_size α Std.HashSet.emptyWithCapacity ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λx _↦Bool.eq_false_iff.mp (Std.HashSet.contains_empty (a:=Finite.nth x)))
+    simp only [this, Std.HashSet.size_emptyWithCapacity, Nat.zero_add, Nat.succ_eq_add_one]
-- 
cgit v1.2.3

