diff options
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₂) ) |