recover prettier proof

leanprover · Sep 13, 2024 · d0278ff · d0278ff
1 parent 05642c2
commit d0278ff
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 6 deletions.
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
@@ -113,12 +113,10 @@ instance : Sub USize       := ⟨USize.sub⟩
 instance : LT USize        := ⟨USize.lt⟩
 instance : LE USize        := ⟨USize.le⟩
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_usize_dec_lt"]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
-set_option bootstrap.genMatcherCode false in
 @[extern "lean_usize_dec_le"]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))

diff --git a/src/Std/Data/DHashMap/Internal/Index.lean b/src/Std/Data/DHashMap/Internal/Index.lean
@@ -56,10 +56,9 @@ cf. https://github.com/leanprover/lean4/issues/4157
       · exact h'
       · rw [USize.le_def, BitVec.le_def]
         change _ ≤ (_ % _)
-        rw [Nat.mod_eq_of_lt h']
-        rw [USize.toBitVec_eq_of_lt]
-        · omega
-        · cases usize_size_eq <;> omega
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
+        · exact h
+        · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
 
 end Std.DHashMap.Internal