diff --git a/src/Init/Data/SInt.lean b/src/Init/Data/SInt.lean
index f9e16fb925..d821c6948e 100644
--- a/src/Init/Data/SInt.lean
+++ b/src/Init/Data/SInt.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.SInt.Basic
 import Init.Data.SInt.Float
 import Init.Data.SInt.Float32
+import Init.Data.SInt.Lemmas
 
 /-!
 This module contains the definitions and basic theory about signed fixed width integer types.
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
new file mode 100644
index 0000000000..a75d4796d1
--- /dev/null
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.SInt.Basic
+
+@[simp] theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec := rfl
+@[simp] theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec := rfl
+@[simp] theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec := rfl
+@[simp] theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec := rfl
+@[simp] theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec := rfl
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 984dcc6cf4..7ce5c94574 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -295,11 +295,16 @@ def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
 def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
   USize.ofNatLT n h
 
-theorem usize_size_le : USize.size ≤ 18446744073709551616 := by
-  cases usize_size_eq <;> next h => rw [h]; decide
+@[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
+@[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
 
-theorem le_usize_size : 4294967296 ≤ USize.size := by
-  cases usize_size_eq <;> next h => rw [h]; decide
+@[deprecated USize.size_le (since := "2025-02-24")]
+theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
+  USize.size_le
+
+@[deprecated USize.le_size (since := "2025-02-24")]
+theorem le_usize_size : 4294967296 ≤ USize.size :=
+  USize.le_size
 
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
@@ -326,7 +331,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
-  USize.ofNatLT n (Nat.lt_of_lt_of_le h le_usize_size)
+  USize.ofNatLT n (Nat.lt_of_lt_of_le h USize.le_size)
 @[extern "lean_uint8_to_usize"]
 def UInt8.toUSize (a : UInt8) : USize :=
   USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
@@ -351,7 +356,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (a : USize) : UInt64 :=
-  UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le)
+  UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)
 
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index 18df9d8810..1a84a6d870 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -138,8 +138,16 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 
-@[deprecated usize_size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
-  usize_size_pos
+@[deprecated USize.size_eq (since := "2025-02-24")]
+theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
+  USize.size_eq
+
+@[deprecated USize.size_pos (since := "2025-02-24")]
+theorem usize_size_pos : 0 < USize.size :=
+  USize.size_pos
+
+@[deprecated USize.size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
+  USize.size_pos
 
 /-- Converts a `USize` into the corresponding `Fin USize.size`. -/
 def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
@@ -155,7 +163,7 @@ def USize.ofNatTruncate (n : Nat) : USize :=
   if h : n < USize.size then
     USize.ofNatLT n h
   else
-    USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt usize_size_pos))
+    USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos))
 abbrev Nat.toUSize := USize.ofNat
 @[extern "lean_usize_to_nat"]
 def USize.toNat (n : USize) : Nat := n.toBitVec.toNat
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
index deb8f6d23c..33d283763c 100644
--- a/src/Init/Data/UInt/Bitwise.lean
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -25,11 +25,11 @@ namespace $typeName
 @[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
 @[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
 
-@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat]
-@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat]
+@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat, -toNat_toBitVec]
+@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat, -toNat_toBitVec]
+@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat, -toNat_toBitVec]
+@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat, -toNat_toBitVec]
+@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat, -toNat_toBitVec]
 
 open $typeName (toNat_and) in
 @[deprecated toNat_and (since := "2024-11-28")]
@@ -37,7 +37,6 @@ protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.
 
 end $typeName
 )
-
 declare_bitwise_uint_theorems UInt8 8
 declare_bitwise_uint_theorems UInt16 16
 declare_bitwise_uint_theorems UInt32 32
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 41a46408f8..2b378c42a0 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -34,15 +34,23 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   @[deprecated toNat_ofNatLT (since := "2025-02-13")]
   theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
 
-  @[simp] theorem toFin_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
-  @[deprecated toFin_val_eq_toNat (since := "2025-02-12")]
+  @[simp] theorem toFin_val (x : $typeName) : x.toFin.val = x.toNat := rfl
+  @[deprecated toFin_val (since := "2025-02-12")]
   theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
 
+  @[simp] theorem toNat_toBitVec (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
+  @[simp] theorem toFin_toBitVec (x : $typeName) : x.toBitVec.toFin = x.toFin := rfl
+
+  @[deprecated toNat_toBitVec (since := "2025-02-21")]
   theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
 
-  @[simp] theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
+  @[simp] theorem ofBitVec_toBitVec : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
 
+  @[deprecated ofBitVec_toBitVec (since := "2025-02-21")]
+  theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a :=
+    ofBitVec_toBitVec
+
   @[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
   theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
@@ -241,21 +249,174 @@ declare_uint_theorems USize System.Platform.numBits
 
 @[simp] theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n := rfl
 
-@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32  := rfl
-
+@[simp] theorem USize.toNat_toUInt8 (x : USize) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
+@[simp] theorem USize.toNat_toUInt16 (x : USize) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
+@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
 @[simp] theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat := rfl
 
 theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
-  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h le_usize_size)
+  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h USize.le_size)
 
 theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
-  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
-  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
-  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
-  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+
+@[simp] theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8 := n.toFin.isLt
+@[simp] theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16 := n.toFin.isLt
+@[simp] theorem UInt32.toNat_lt (n : UInt32) : n.toNat < 2 ^ 32 := n.toFin.isLt
+@[simp] theorem UInt64.toNat_lt (n : UInt64) : n.toNat < 2 ^ 64 := n.toFin.isLt
+
+theorem UInt8.size_lt_usizeSize : UInt8.size < USize.size := by
+  cases USize.size_eq <;> simp_all +decide
+theorem UInt8.size_le_usizeSize : UInt8.size ≤ USize.size :=
+  Nat.le_of_lt UInt8.size_lt_usizeSize
+theorem UInt16.size_lt_usizeSize : UInt16.size < USize.size := by
+  cases USize.size_eq <;> simp_all +decide
+theorem UInt16.size_le_usizeSize : UInt16.size ≤ USize.size :=
+  Nat.le_of_lt UInt16.size_lt_usizeSize
+theorem UInt32.size_le_usizeSize : UInt32.size ≤ USize.size := by
+  cases USize.size_eq <;> simp_all +decide
+theorem USize.size_eq_two_pow : USize.size = 2 ^ System.Platform.numBits := rfl
+theorem USize.toNat_lt_two_pow_numBits (n : USize) : n.toNat < 2 ^ System.Platform.numBits := n.toFin.isLt
+@[simp] theorem USize.toNat_lt (n : USize) : n.toNat < 2 ^ 64 := Nat.lt_of_lt_of_le n.toFin.isLt size_le
+
+theorem UInt8.toNat_lt_usizeSize (n : UInt8) : n.toNat < USize.size :=
+  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
+theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size :=
+  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
+theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size :=
+  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
+
+@[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt64ToNat (n : UInt64) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+@[simp] theorem Fin.mk_uSizeToNat (n : USize) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+
+@[simp] theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uSizeToNat (n : USize) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+
+@[simp] theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : BitVec.ofFin n.toFin = n.toBitVec := rfl
+@[simp] theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : BitVec.ofFin n.toFin = n.toBitVec := rfl
+@[simp] theorem BitVec.ofFin_uInt32ToFin (n : UInt32) : BitVec.ofFin n.toFin = n.toBitVec := rfl
+@[simp] theorem BitVec.ofFin_uInt64ToFin (n : UInt64) : BitVec.ofFin n.toFin = n.toBitVec := rfl
+@[simp] theorem BitVec.ofFin_uSizeToFin (n : USize) : BitVec.ofFin n.toFin = n.toBitVec := rfl
+
+@[simp] theorem UInt8.toFin_toUInt16 (n : UInt8) : n.toUInt16.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt8.toFin_toUInt32 (n : UInt8) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt8.toFin_toUInt64 (n : UInt8) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt8.toFin_toUSize (n : UInt8) :
+  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
+
+@[simp] theorem UInt16.toFin_toUInt32 (n : UInt16) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt16.toFin_toUInt64 (n : UInt16) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt16.toFin_toUSize (n : UInt16) :
+  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
+
+@[simp] theorem UInt32.toFin_toUInt64 (n : UInt32) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
+@[simp] theorem UInt32.toFin_toUSize (n : UInt32) :
+  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
+
+@[simp] theorem USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = n.toFin.castLE size_le_usizeSize := rfl
+
+@[simp] theorem UInt16.toBitVec_toUInt8 (n : UInt16) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
+@[simp] theorem UInt32.toBitVec_toUInt8 (n : UInt32) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
+@[simp] theorem UInt64.toBitVec_toUInt8 (n : UInt64) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
+@[simp] theorem USize.toBitVec_toUInt8 (n : USize) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := BitVec.eq_of_toNat_eq (by simp)
+
+@[simp] theorem UInt8.toBitVec_toUInt16 (n : UInt8) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
+@[simp] theorem UInt32.toBitVec_toUInt16 (n : UInt32) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
+@[simp] theorem UInt64.toBitVec_toUInt16 (n : UInt64) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
+@[simp] theorem USize.toBitVec_toUInt16 (n : USize) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := BitVec.eq_of_toNat_eq (by simp)
+
+@[simp] theorem UInt8.toBitVec_toUInt32 (n : UInt8) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
+@[simp] theorem UInt16.toBitVec_toUInt32 (n : UInt16) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
+@[simp] theorem UInt64.toBitVec_toUInt32 (n : UInt64) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
+@[simp] theorem USize.toBitVec_toUInt32 (n : USize) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := BitVec.eq_of_toNat_eq (by simp)
+
+@[simp] theorem UInt8.toBitVec_toUInt64 (n : UInt8) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
+@[simp] theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
+@[simp] theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
+@[simp] theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 :=
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt (USize.toNat_lt _)])
+
+@[simp] theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
+@[simp] theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
+@[simp] theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
+  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
+@[simp] theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
+  BitVec.eq_of_toNat_eq (by simp)
+
+@[simp] theorem UInt8.ofNatLT_toNat (n : UInt8) : UInt8.ofNatLT n.toNat n.toNat_lt = n := rfl
+@[simp] theorem UInt16.ofNatLT_uInt8ToNat (n : UInt8) : UInt16.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt16 := rfl
+@[simp] theorem UInt32.ofNatLT_uInt8ToNat (n : UInt8) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
+@[simp] theorem UInt64.ofNatLT_uInt8ToNat (n : UInt8) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
+@[simp] theorem USize.ofNatLT_uInt8ToNat (n : UInt8) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
+
+@[simp] theorem UInt16.ofNatLT_toNat (n : UInt16) : UInt16.ofNatLT n.toNat n.toNat_lt = n := rfl
+@[simp] theorem UInt32.ofNatLT_uInt16ToNat (n : UInt16) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
+@[simp] theorem UInt64.ofNatLT_uInt16ToNat (n : UInt16) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
+@[simp] theorem USize.ofNatLT_uInt16ToNat (n : UInt16) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
+
+@[simp] theorem UInt32.ofNatLT_toNat (n : UInt32) : UInt32.ofNatLT n.toNat n.toNat_lt = n := rfl
+@[simp] theorem UInt64.ofNatLT_uInt32ToNat (n : UInt32) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
+@[simp] theorem USize.ofNatLT_uInt32ToNat (n : UInt32) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
+
+@[simp] theorem UInt64.ofNatLT_toNat (n : UInt64) : UInt64.ofNatLT n.toNat n.toNat_lt = n := rfl
+
+@[simp] theorem USize.ofNatLT_toNat (n : USize) : USize.ofNatLT n.toNat n.toNat_lt_size = n := rfl
+@[simp] theorem UInt64.ofNatLT_uSizeToNat (n : USize) : UInt64.ofNatLT n.toNat n.toNat_lt = n.toUInt64 := rfl
+
+-- We are not making these into `simp` lemmas because they lose the information stored in `h`. ·
+theorem UInt8.ofNatLT_uInt16ToNat (n : UInt16) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
+  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt8.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
+  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt8.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
+  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt8.ofNatLT_uSizeToNat (n : USize) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
+  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt16.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
+  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt16.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
+  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt16.ofNatLT_uSizeToNat (n : USize) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
+  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt32.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
+  UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem UInt32.ofNatLT_uSizeToNat (n : USize) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
+  UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h) : USize.ofNatLT n.toNat h = n.toUSize :=
+  USize.toNat.inj (by simp [Nat.mod_eq_of_lt h])
+
+@[simp] theorem UInt8.ofFin_toFin (n : UInt8) : UInt8.ofFin n.toFin = n := rfl
+@[simp] theorem UInt16.ofFin_toFin (n : UInt16) : UInt16.ofFin n.toFin = n := rfl
+@[simp] theorem UInt32.ofFin_toFin (n : UInt32) : UInt32.ofFin n.toFin = n := rfl
+@[simp] theorem UInt64.ofFin_toFin (n : UInt64) : UInt64.ofFin n.toFin = n := rfl
+@[simp] theorem USize.ofFin_toFin (n : USize) : USize.ofFin n.toFin = n := rfl
+
+@[simp] theorem UInt16.ofFin_uint8ToFin (n : UInt8) : UInt16.ofFin (n.toFin.castLE (by decide)) = n.toUInt16 := rfl
+
+@[simp] theorem UInt32.ofFin_uint8ToFin (n : UInt8) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
+@[simp] theorem UInt32.ofFin_uint16ToFin (n : UInt16) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
+
+@[simp] theorem UInt64.ofFin_uint8ToFin (n : UInt8) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
+@[simp] theorem UInt64.ofFin_uint16ToFin (n : UInt16) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
+@[simp] theorem UInt64.ofFin_uint32ToFin (n : UInt32) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
+
+@[simp] theorem USize.ofFin_uint8ToFin (n : UInt8) : USize.ofFin (n.toFin.castLE UInt8.size_le_usizeSize) = n.toUSize := rfl
+@[simp] theorem USize.ofFin_uint16ToFin (n : UInt16) : USize.ofFin (n.toFin.castLE UInt16.size_le_usizeSize) = n.toUSize := rfl
+@[simp] theorem USize.ofFin_uint32ToFin (n : UInt32) : USize.ofFin (n.toFin.castLE UInt32.size_le_usizeSize) = n.toUSize := rfl
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 25936c5623..f188316fd6 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2150,14 +2150,14 @@ instance : Inhabited UInt64 where
 /-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
 abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
-theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
+theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
   | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
   | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
 
-theorem usize_size_pos : LT.lt 0 USize.size :=
-  match USize.size, usize_size_eq with
+theorem USize.size_pos : LT.lt 0 USize.size :=
+  match USize.size, USize.size_eq with
   | _, Or.inl rfl => of_decide_eq_true rfl
   | _, Or.inr rfl => of_decide_eq_true rfl
 
@@ -2207,7 +2207,7 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
 instance : DecidableEq USize := USize.decEq
 
 instance : Inhabited USize where
-  default := USize.ofNatLT 0 usize_size_pos
+  default := USize.ofNatLT 0 USize.size_pos
 
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and