From 2402a88a863e41f5bceefcdc13323ef609809a8a Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 9 Oct 2025 22:53:27 +0200
Subject: Lean 4.18

---
 LeanAStar/HashSet.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'LeanAStar')

diff --git a/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean
index 33ef316..c73216e 100644
--- a/LeanAStar/HashSet.lean
+++ b/LeanAStar/HashSet.lean
@@ -100,7 +100,7 @@ theorem size_le_finite_set_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α
     exact Std.HashSet.size_le_finite_worker_size α set ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λa hx ↦
       by
       have h₁ := a.isLt
-      simp_arith[h] at h₁
+      simp +arith[h] at h₁
       have h₂ : a > l := Fin.lt_iff_val_lt_val.mp hx
       exact absurd h₁ (Nat.not_le.mpr h₂)
     )
-- 
cgit v1.2.3