From 973225b1c5ed10f2a99374c91a9d6a957067f654 Mon Sep 17 00:00:00 2001 From: Andreas Grois 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