refactor: golf proof

src/Std/Data/DHashMap/Internal/Index.lean

@@ -46,19 +46,11 @@ cf. https://github.com/leanprover/lean4/issues/4157
 @[irreducible, inline] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
     { u : USize // u.toNat < sz } :=
   ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
-    -- Making this proof significantly less painful will be a good test for our USize API
+    -- This proof is a good test for our USize API
     by_cases h' : sz < USize.size
-    · rw [USize.toNat_and, ← USize.ofNat_one, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt]
-      · refine Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h ?_)
-        rw [USize.toNat_ofNat_of_lt]
-        · exact Nat.one_pos
-        · exact Nat.lt_of_le_of_lt h h'
-      · exact h'
-      · rw [USize.le_def, BitVec.le_def]
-        change _ ≤ (_ % _)
-        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'
+    · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt h']
+      · exact Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h (by simp))
+      · simp [USize.le_iff_toNat_le, Nat.mod_eq_of_lt h', Nat.succ_le_of_lt h]
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
 
 end Std.DHashMap.Internal