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/HashSet.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'LeanAStar/HashSet.lean')

diff --git a/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean
index c73216e..87f351a 100644
--- a/LeanAStar/HashSet.lean
+++ b/LeanAStar/HashSet.lean
@@ -12,13 +12,13 @@ theorem erase_not_mem_of_not_mem {α : Type u} [BEq α] [Hashable α] [LawfulBEq
   rw[HashSet.mem_erase] at h₂
   exact absurd h₂.right h₁
 
-protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_h₁ : ∀(o : Fin (Finite.cardinality α)) (_h : o > n), Finite.nth o ∉ set), set.size ≤ (Finite.set.set_worker α HashSet.empty  n).size := by
+protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : ∀ (set : Std.HashSet α) (n : Fin (Finite.cardinality α)) (_h₁ : ∀(o : Fin (Finite.cardinality α)) (_h : o > n), Finite.nth o ∉ set), set.size ≤ (Finite.set.set_worker α HashSet.emptyWithCapacity  n).size := by
   intros set n h₁
   cases n
   case mk n h₂ =>
   cases n
   case zero =>
-    have h₃ : (Finite.set.set_worker α empty ⟨0,h₂⟩).size = 1 := by simp[Finite.set.set_worker, HashSet.size_insert]
+    have h₃ : (Finite.set.set_worker α emptyWithCapacity ⟨0,h₂⟩).size = 1 := by simp[Finite.set.set_worker, HashSet.size_insert]
     rw[h₃]
     cases h₄ : set.contains (Finite.nth ⟨0,h₂⟩)
     case false =>
@@ -73,10 +73,10 @@ protected theorem size_le_finite_worker_size (α : Type u) [Finite α] [BEq α]
         have h₆ : o > m+1 := by simp at h₄; omega
         exact erase_not_mem_of_not_mem _ _ (h₁ ⟨o,h₅⟩ h₆)
     have h₅ := Std.HashSet.size_le_finite_worker_size α rset ⟨m, Nat.lt_of_succ_lt h₂⟩ h₄
-    have h₆ : (Finite.set.set_worker α empty ⟨m, Nat.lt_of_succ_lt h₂⟩).size = empty.size + m + 1 :=
-      Finite.set_worker_size α empty ⟨m, Nat.lt_of_succ_lt h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
-    have h₇ : (Finite.set.set_worker α empty ⟨m+1,h₂⟩).size = empty.size + (m + 1) + 1 :=
-      Finite.set_worker_size α empty ⟨m+1,h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
+    have h₆ : (Finite.set.set_worker α emptyWithCapacity ⟨m, Nat.lt_of_succ_lt h₂⟩).size = emptyWithCapacity.size + m + 1 :=
+      Finite.set_worker_size α emptyWithCapacity ⟨m, Nat.lt_of_succ_lt h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
+    have h₇ : (Finite.set.set_worker α emptyWithCapacity ⟨m+1,h₂⟩).size = emptyWithCapacity.size + (m + 1) + 1 :=
+      Finite.set_worker_size α emptyWithCapacity ⟨m+1,h₂⟩ (λa _ ↦Bool.eq_false_iff.mp $ HashSet.contains_empty (a := Finite.nth a))
     have h₈ := HashSet.size_le_size_erase (m := set) (k:=Finite.nth ⟨m+1,h₂⟩)
     simp[h₆] at h₅
     simp[h₇]
-- 
cgit v1.2.3

