diff --git a/tests/lean/simprocUInt.lean b/tests/lean/simprocUInt.lean
new file mode 100644
index 000000000000..98ae68359fb0
--- /dev/null
+++ b/tests/lean/simprocUInt.lean
@@ -0,0 +1,7 @@
+variable (x : USize)
+
+/- USize.toNat -/
+
+#check_simp USize.toNat 4294967296 !~>
+#check_simp USize.toNat 4294967295 ~> 4294967295
+#check_simp USize.toNat (x &&& 1) ~> x.toNat % 2