diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index ff376e15cc..b89a898647 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -115,6 +115,15 @@ protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
 
 @[simp] protected theorem ofNat_one : ofNat 1 = 1 := rfl
 
+@[simp]
+theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+@[simp]
+theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
+
+@[simp]
+theorem mk_ofNat (n : Nat) : mk (BitVec.ofNat _ n) = OfNat.ofNat n := rfl
+
 end $typeName
 )
 
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index d3aaedd122..a8f975a989 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -46,7 +46,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 44895f5576..b7dc0cc094 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -42,7 +42,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property
diff --git a/tests/lean/run/trivial_uint.lean b/tests/lean/run/trivial_uint.lean
new file mode 100644
index 0000000000..06977ec67d
--- /dev/null
+++ b/tests/lean/run/trivial_uint.lean
@@ -0,0 +1,15 @@
+example : UInt8.val 42 = 42 := by simp
+example : UInt16.val 42 = 42 := by simp
+example : UInt32.val 42 = 42 := by simp
+example : UInt64.val 42 = 42 := by simp
+example : USize.val 42 = 42 := by simp
+example : UInt8.toBitVec 42 = 42 := by simp
+example : UInt16.toBitVec 42 = 42 := by simp
+example : UInt32.toBitVec 42 = 42 := by simp
+example : UInt64.toBitVec 42 = 42 := by simp
+example : USize.toBitVec 42 = 42 := by simp
+example : UInt8.mk 42 = 42 := by simp
+example : UInt16.mk 42 = 42 := by simp
+example : UInt32.mk 42 = 42 := by simp
+example : UInt64.mk 42 = 42 := by simp
+example : USize.mk 42 = 42 := by simp