diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 2c8b97923c4d..3500dc24cdb8 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -47,11 +47,11 @@ protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b
 open $typeName (ne_of_val_ne) in
 protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
 
-@[simp] protected theorem zero_toNat : (0 : $typeName).toNat = 0 := Nat.zero_mod _
-@[simp] protected theorem mod_toNat (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
-@[simp] protected theorem div_toNat (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
-@[simp] protected theorem sub_toNat_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
-@[simp] protected theorem modn_toNat (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
+@[simp] protected theorem toNat_zero : (0 : $typeName).toNat = 0 := Nat.zero_mod _
+@[simp] protected theorem toNat_mod (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
+@[simp] protected theorem toNat_div (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
+@[simp] protected theorem toNat_sub_of_le (a b : $typeName) : b ≤ a → (a - b).toNat = a.toNat - b.toNat := Fin.sub_val_of_le
+@[simp] protected theorem toNat_modn (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
 protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
   | ⟨u⟩, h => Fin.modn_lt u h
 open $typeName (modn_lt) in
@@ -69,3 +69,28 @@ declare_uint_theorems UInt16
 declare_uint_theorems UInt32
 declare_uint_theorems UInt64
 declare_uint_theorems USize
+
+@[deprecated (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
+@[deprecated (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
+@[deprecated (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt8.modn_toNat := @UInt8.toNat_modn
+
+@[deprecated (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
+@[deprecated (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
+@[deprecated (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt16.modn_toNat := @UInt16.toNat_modn
+
+@[deprecated (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
+@[deprecated (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
+@[deprecated (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt32.modn_toNat := @UInt32.toNat_modn
+
+@[deprecated (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
+@[deprecated (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
+@[deprecated (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev UInt64.modn_toNat := @UInt64.toNat_modn
+
+@[deprecated (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
+@[deprecated (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
+@[deprecated (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod
+@[deprecated (since := "2024-06-23")] protected abbrev USize.modn_toNat := @USize.toNat_modn
diff --git a/src/Std/Data/DHashMap/Internal/Index.lean b/src/Std/Data/DHashMap/Internal/Index.lean
index e2b25b858b69..a6afa47b5697 100644
--- a/src/Std/Data/DHashMap/Internal/Index.lean
+++ b/src/Std/Data/DHashMap/Internal/Index.lean
@@ -48,7 +48,7 @@ cf. https://github.com/leanprover/lean4/issues/4157
   ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
     -- Making this proof significantly less painful will be a good test for our USize API
     by_cases h' : sz < USize.size
-    · rw [USize.and_toNat, ← USize.ofNat_one, USize.sub_toNat_of_le, USize.toNat_ofNat_of_lt]
+    · rw [USize.and_toNat, ← 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