diff options
| author | Andreas Grois <andi@grois.info> | 2025-10-09 22:53:27 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-10-09 22:53:27 +0200 |
| commit | 2402a88a863e41f5bceefcdc13323ef609809a8a (patch) | |
| tree | 8672033c3486b348ee715244d932d6f831dff05e /LeanAStar/HashSet.lean | |
| parent | dee1a274a1c625462de03b58eaeff82e5db8b830 (diff) | |
Lean 4.18
Diffstat (limited to 'LeanAStar/HashSet.lean')
| -rw-r--r-- | LeanAStar/HashSet.lean | 2 |
1 files changed, 1 insertions, 1 deletions
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₂) ) |