diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index cecb35dbd3..24d5e5c6de 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -638,6 +638,18 @@ theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1 :=
+  Int.le_sub_one_of_lt toInt_lt
+
+theorem toInt_lt_of_pos {w : Nat} (hw : 0 < w) {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by
+  have := toInt_lt (w := w) (x := x)
+  generalize x.toInt = x at *
+  rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
+  omega
+
+theorem toInt_le_of_pos {w : Nat} (hw : 0 < w) {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1 :=
+  Int.le_sub_one_of_lt (toInt_lt_of_pos hw)
+
 /--
 `x.toInt` is greater than or equal to `-2^(w-1)`.
 We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
@@ -650,6 +662,12 @@ theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
+theorem le_toInt_of_pos {w : Nat} (hw : 0 < w) (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
+  have := le_toInt (w := w) (x := x)
+  generalize x.toInt = x at *
+  rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
+  omega
+
 /-! ### slt -/
 
 /--
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index b2f8940aff..87e77b577f 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -1406,3 +1406,77 @@ theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) :
 @[simp] theorem ISize.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
     toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
   ISize.toInt64_ofNat' (by rw [toInt_maxValue]; cases System.Platform.numBits_eq <;> simp_all <;> omega)
+
+@[simp] theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) :
+    Int8.ofIntLE n.toInt (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide)) = Int8.ofBitVec n :=
+  Int8.toBitVec.inj (by simp)
+@[simp] theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) :
+    Int16.ofIntLE n.toInt (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide)) = Int16.ofBitVec n :=
+  Int16.toBitVec.inj (by simp)
+@[simp] theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) :
+    Int32.ofIntLE n.toInt (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide)) = Int32.ofBitVec n :=
+  Int32.toBitVec.inj (by simp)
+@[simp] theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) :
+    Int64.ofIntLE n.toInt (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide)) = Int64.ofBitVec n :=
+  Int64.toBitVec.inj (by simp)
+@[simp] theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) :
+    ISize.ofIntLE n.toInt (toInt_minValue ▸ n.le_toInt_of_pos System.Platform.numBits_pos)
+    (toInt_maxValue ▸ n.toInt_le_of_pos System.Platform.numBits_pos) = ISize.ofBitVec n :=
+  ISize.toBitVec.inj (by simp)
+
+theorem Int8.ofBitVec_ofNatLT (n : Nat) (hn) : Int8.ofBitVec (BitVec.ofNatLT n hn) = Int8.ofNat n :=
+  Int8.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat hn])
+theorem Int16.ofBitVec_ofNatLT (n : Nat) (hn) : Int16.ofBitVec (BitVec.ofNatLT n hn) = Int16.ofNat n :=
+  Int16.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat hn])
+theorem Int32.ofBitVec_ofNatLT (n : Nat) (hn) : Int32.ofBitVec (BitVec.ofNatLT n hn) = Int32.ofNat n :=
+  Int32.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat hn])
+theorem Int64.ofBitVec_ofNatLT (n : Nat) (hn) : Int64.ofBitVec (BitVec.ofNatLT n hn) = Int64.ofNat n :=
+  Int64.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat hn])
+theorem ISize.ofBitVec_ofNatLT (n : Nat) (hn) : ISize.ofBitVec (BitVec.ofNatLT n hn) = ISize.ofNat n :=
+  ISize.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat hn])
+
+@[simp] theorem Int8.ofBitVec_ofNat (n : Nat) : Int8.ofBitVec (BitVec.ofNat 8 n) = Int8.ofNat n := rfl
+@[simp] theorem Int16.ofBitVec_ofNat (n : Nat) : Int16.ofBitVec (BitVec.ofNat 16 n) = Int16.ofNat n := rfl
+@[simp] theorem Int32.ofBitVec_ofNat (n : Nat) : Int32.ofBitVec (BitVec.ofNat 32 n) = Int32.ofNat n := rfl
+@[simp] theorem Int64.ofBitVec_ofNat (n : Nat) : Int64.ofBitVec (BitVec.ofNat 64 n) = Int64.ofNat n := rfl
+@[simp] theorem ISize.ofBitVec_ofNat (n : Nat) : ISize.ofBitVec (BitVec.ofNat System.Platform.numBits n) = ISize.ofNat n := rfl
+
+@[simp] theorem Int8.ofBitVec_ofInt (n : Int) : Int8.ofBitVec (BitVec.ofInt 8 n) = Int8.ofInt n := rfl
+@[simp] theorem Int16.ofBitVec_ofInt (n : Int) : Int16.ofBitVec (BitVec.ofInt 16 n) = Int16.ofInt n := rfl
+@[simp] theorem Int32.ofBitVec_ofInt (n : Int) : Int32.ofBitVec (BitVec.ofInt 32 n) = Int32.ofInt n := rfl
+@[simp] theorem Int64.ofBitVec_ofInt (n : Int) : Int64.ofBitVec (BitVec.ofInt 64 n) = Int64.ofInt n := rfl
+@[simp] theorem ISize.ofBitVec_ofInt (n : Int) : ISize.ofBitVec (BitVec.ofInt System.Platform.numBits n) = ISize.ofInt n := rfl
+
+@[simp] theorem Int8.ofNat_bitVecToNat (n : BitVec 8) : Int8.ofNat n.toNat = Int8.ofBitVec n :=
+  Int8.toBitVec.inj (by simp)
+@[simp] theorem Int16.ofNat_bitVecToNat (n : BitVec 16) : Int16.ofNat n.toNat = Int16.ofBitVec n :=
+  Int16.toBitVec.inj (by simp)
+@[simp] theorem Int32.ofNat_bitVecToNat (n : BitVec 32) : Int32.ofNat n.toNat = Int32.ofBitVec n :=
+  Int32.toBitVec.inj (by simp)
+@[simp] theorem Int64.ofNat_bitVecToNat (n : BitVec 64) : Int64.ofNat n.toNat = Int64.ofBitVec n :=
+  Int64.toBitVec.inj (by simp)
+@[simp] theorem ISize.ofNat_bitVecToNat (n : BitVec System.Platform.numBits) : ISize.ofNat n.toNat = ISize.ofBitVec n :=
+  ISize.toBitVec.inj (by simp)
+
+@[simp] theorem Int8.ofInt_bitVecToInt (n : BitVec 8) : Int8.ofInt n.toInt = Int8.ofBitVec n :=
+  Int8.toBitVec.inj (by simp)
+@[simp] theorem Int16.ofInt_bitVecToInt (n : BitVec 16) : Int16.ofInt n.toInt = Int16.ofBitVec n :=
+  Int16.toBitVec.inj (by simp)
+@[simp] theorem Int32.ofInt_bitVecToInt (n : BitVec 32) : Int32.ofInt n.toInt = Int32.ofBitVec n :=
+  Int32.toBitVec.inj (by simp)
+@[simp] theorem Int64.ofInt_bitVecToInt (n : BitVec 64) : Int64.ofInt n.toInt = Int64.ofBitVec n :=
+  Int64.toBitVec.inj (by simp)
+@[simp] theorem ISize.ofInt_bitVecToInt (n : BitVec System.Platform.numBits) : ISize.ofInt n.toInt = ISize.ofBitVec n :=
+  ISize.toBitVec.inj (by simp)
+
+@[simp] theorem Int8.ofIntTruncate_bitVecToInt (n : BitVec 8) : Int8.ofIntTruncate n.toInt = Int8.ofBitVec n :=
+  Int8.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide))])
+@[simp] theorem Int16.ofIntTruncate_bitVecToInt (n : BitVec 16) : Int16.ofIntTruncate n.toInt = Int16.ofBitVec n :=
+  Int16.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide))])
+@[simp] theorem Int32.ofIntTruncate_bitVecToInt (n : BitVec 32) : Int32.ofIntTruncate n.toInt = Int32.ofBitVec n :=
+  Int32.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide))])
+@[simp] theorem Int64.ofIntTruncate_bitVecToInt (n : BitVec 64) : Int64.ofIntTruncate n.toInt = Int64.ofBitVec n :=
+  Int64.toBitVec.inj (by simp [toBitVec_ofIntTruncate (n.le_toInt_of_pos (by decide)) (n.toInt_le_of_pos (by decide))])
+@[simp] theorem ISize.ofIntTruncate_bitVecToInt (n : BitVec System.Platform.numBits) : ISize.ofIntTruncate n.toInt = ISize.ofBitVec n :=
+  ISize.toBitVec.inj (by simp [toBitVec_ofIntTruncate (toInt_minValue ▸ n.le_toInt_of_pos System.Platform.numBits_pos)
+    (toInt_maxValue ▸ n.toInt_le_of_pos System.Platform.numBits_pos) ])
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 3da3d818b4..82ab94f584 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1253,3 +1253,94 @@ theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
 
 @[simp] theorem USize.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
   USize.toUInt64_ofNat' (Nat.lt_of_lt_of_le hn UInt32.size_le_usizeSize)
+
+@[simp] theorem UInt8.ofNatLT_finVal (n : Fin UInt8.size) : UInt8.ofNatLT n.val n.isLt = UInt8.ofFin n := rfl
+@[simp] theorem UInt16.ofNatLT_finVal (n : Fin UInt16.size) : UInt16.ofNatLT n.val n.isLt = UInt16.ofFin n := rfl
+@[simp] theorem UInt32.ofNatLT_finVal (n : Fin UInt32.size) : UInt32.ofNatLT n.val n.isLt = UInt32.ofFin n := rfl
+@[simp] theorem UInt64.ofNatLT_finVal (n : Fin UInt64.size) : UInt64.ofNatLT n.val n.isLt = UInt64.ofFin n := rfl
+@[simp] theorem USize.ofNatLT_finVal (n : Fin USize.size) : USize.ofNatLT n.val n.isLt = USize.ofFin n := rfl
+
+@[simp] theorem UInt8.ofNatLT_bitVecToNat (n : BitVec 8) : UInt8.ofNatLT n.toNat n.isLt = UInt8.ofBitVec n := rfl
+@[simp] theorem UInt16.ofNatLT_bitVecToNat (n : BitVec 16) : UInt16.ofNatLT n.toNat n.isLt = UInt16.ofBitVec n := rfl
+@[simp] theorem UInt32.ofNatLT_bitVecToNat (n : BitVec 32) : UInt32.ofNatLT n.toNat n.isLt = UInt32.ofBitVec n := rfl
+@[simp] theorem UInt64.ofNatLT_bitVecToNat (n : BitVec 64) : UInt64.ofNatLT n.toNat n.isLt = UInt64.ofBitVec n := rfl
+@[simp] theorem USize.ofNatLT_bitVecToNat (n : BitVec System.Platform.numBits) : USize.ofNatLT n.toNat n.isLt = USize.ofBitVec n := rfl
+
+@[simp] theorem UInt8.ofNat_finVal (n : Fin UInt8.size) : UInt8.ofNat n.val = UInt8.ofFin n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_finVal]
+@[simp] theorem UInt16.ofNat_finVal (n : Fin UInt16.size) : UInt16.ofNat n.val = UInt16.ofFin n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_finVal]
+@[simp] theorem UInt32.ofNat_finVal (n : Fin UInt32.size) : UInt32.ofNat n.val = UInt32.ofFin n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_finVal]
+@[simp] theorem UInt64.ofNat_finVal (n : Fin UInt64.size) : UInt64.ofNat n.val = UInt64.ofFin n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_finVal]
+@[simp] theorem USize.ofNat_finVal (n : Fin USize.size) : USize.ofNat n.val = USize.ofFin n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_finVal]
+
+@[simp] theorem UInt8.ofNat_bitVecToNat (n : BitVec 8) : UInt8.ofNat n.toNat = UInt8.ofBitVec n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_bitVecToNat]
+@[simp] theorem UInt16.ofNat_bitVecToNat (n : BitVec 16) : UInt16.ofNat n.toNat = UInt16.ofBitVec n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_bitVecToNat]
+@[simp] theorem UInt32.ofNat_bitVecToNat (n : BitVec 32) : UInt32.ofNat n.toNat = UInt32.ofBitVec n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_bitVecToNat]
+@[simp] theorem UInt64.ofNat_bitVecToNat (n : BitVec 64) : UInt64.ofNat n.toNat = UInt64.ofBitVec n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_bitVecToNat]
+@[simp] theorem USize.ofNat_bitVecToNat (n : BitVec System.Platform.numBits) : USize.ofNat n.toNat = USize.ofBitVec n := by
+  rw [← ofNatLT_eq_ofNat (h := n.isLt), ofNatLT_bitVecToNat]
+
+@[simp] theorem UInt8.ofNatTruncate_finVal (n : Fin UInt8.size) : UInt8.ofNatTruncate n.val = UInt8.ofFin n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, UInt8.ofNat_finVal]
+@[simp] theorem UInt16.ofNatTruncate_finVal (n : Fin UInt16.size) : UInt16.ofNatTruncate n.val = UInt16.ofFin n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, UInt16.ofNat_finVal]
+@[simp] theorem UInt32.ofNatTruncate_finVal (n : Fin UInt32.size) : UInt32.ofNatTruncate n.val = UInt32.ofFin n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, UInt32.ofNat_finVal]
+@[simp] theorem UInt64.ofNatTruncate_finVal (n : Fin UInt64.size) : UInt64.ofNatTruncate n.val = UInt64.ofFin n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, UInt64.ofNat_finVal]
+@[simp] theorem USize.ofNatTruncate_finVal (n : Fin USize.size) : USize.ofNatTruncate n.val = USize.ofFin n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, USize.ofNat_finVal]
+
+@[simp] theorem UInt8.ofNatTruncate_bitVecToNat (n : BitVec 8) : UInt8.ofNatTruncate n.toNat = UInt8.ofBitVec n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, ofNat_bitVecToNat]
+@[simp] theorem UInt16.ofNatTruncate_bitVecToNat (n : BitVec 16) : UInt16.ofNatTruncate n.toNat = UInt16.ofBitVec n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, ofNat_bitVecToNat]
+@[simp] theorem UInt32.ofNatTruncate_bitVecToNat (n : BitVec 32) : UInt32.ofNatTruncate n.toNat = UInt32.ofBitVec n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, ofNat_bitVecToNat]
+@[simp] theorem UInt64.ofNatTruncate_bitVecToNat (n : BitVec 64) : UInt64.ofNatTruncate n.toNat = UInt64.ofBitVec n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, ofNat_bitVecToNat]
+@[simp] theorem USize.ofNatTruncate_bitVecToNat (n : BitVec System.Platform.numBits) : USize.ofNatTruncate n.toNat = USize.ofBitVec n := by
+  rw [ofNatTruncate_eq_ofNat _ n.isLt, ofNat_bitVecToNat]
+
+@[simp] theorem UInt8.ofFin_mk {n : Nat} (hn) : UInt8.ofFin (Fin.mk n hn) = UInt8.ofNatLT n hn := rfl
+@[simp] theorem UInt16.ofFin_mk {n : Nat} (hn) : UInt16.ofFin (Fin.mk n hn) = UInt16.ofNatLT n hn := rfl
+@[simp] theorem UInt32.ofFin_mk {n : Nat} (hn) : UInt32.ofFin (Fin.mk n hn) = UInt32.ofNatLT n hn := rfl
+@[simp] theorem UInt64.ofFin_mk {n : Nat} (hn) : UInt64.ofFin (Fin.mk n hn) = UInt64.ofNatLT n hn := rfl
+@[simp] theorem USize.ofFin_mk {n : Nat} (hn) : USize.ofFin (Fin.mk n hn) = USize.ofNatLT n hn := rfl
+
+@[simp] theorem UInt8.ofFin_bitVecToFin (n : BitVec 8) : UInt8.ofFin n.toFin = UInt8.ofBitVec n := rfl
+@[simp] theorem UInt16.ofFin_bitVecToFin (n : BitVec 16) : UInt16.ofFin n.toFin = UInt16.ofBitVec n := rfl
+@[simp] theorem UInt32.ofFin_bitVecToFin (n : BitVec 32) : UInt32.ofFin n.toFin = UInt32.ofBitVec n := rfl
+@[simp] theorem UInt64.ofFin_bitVecToFin (n : BitVec 64) : UInt64.ofFin n.toFin = UInt64.ofBitVec n := rfl
+@[simp] theorem USize.ofFin_bitVecToFin (n : BitVec System.Platform.numBits) : USize.ofFin n.toFin = USize.ofBitVec n := rfl
+
+@[simp] theorem UInt8.ofBitVec_ofNatLT {n : Nat} (hn) : UInt8.ofBitVec (BitVec.ofNatLT n hn) = UInt8.ofNatLT n hn := rfl
+@[simp] theorem UInt16.ofBitVec_ofNatLT {n : Nat} (hn) : UInt16.ofBitVec (BitVec.ofNatLT n hn) = UInt16.ofNatLT n hn := rfl
+@[simp] theorem UInt32.ofBitVec_ofNatLT {n : Nat} (hn) : UInt32.ofBitVec (BitVec.ofNatLT n hn) = UInt32.ofNatLT n hn := rfl
+@[simp] theorem UInt64.ofBitVec_ofNatLT {n : Nat} (hn) : UInt64.ofBitVec (BitVec.ofNatLT n hn) = UInt64.ofNatLT n hn := rfl
+@[simp] theorem USize.ofBitVec_ofNatLT {n : Nat} (hn) : USize.ofBitVec (BitVec.ofNatLT n hn) = USize.ofNatLT n hn := rfl
+
+@[simp] theorem UInt8.ofBitVec_ofFin (n) : UInt8.ofBitVec (BitVec.ofFin n) = UInt8.ofFin n := rfl
+@[simp] theorem UInt16.ofBitVec_ofFin (n) : UInt16.ofBitVec (BitVec.ofFin n) = UInt16.ofFin n := rfl
+@[simp] theorem UInt32.ofBitVec_ofFin (n) : UInt32.ofBitVec (BitVec.ofFin n) = UInt32.ofFin n := rfl
+@[simp] theorem UInt64.ofBitVec_ofFin (n) : UInt64.ofBitVec (BitVec.ofFin n) = UInt64.ofFin n := rfl
+@[simp] theorem USize.ofBitVec_ofFin (n) : USize.ofBitVec (BitVec.ofFin n) = USize.ofFin n := rfl
+
+@[simp] theorem BitVec.ofNat_uInt8ToNat (n : UInt8) : BitVec.ofNat 8 n.toNat = n.toBitVec :=
+  BitVec.eq_of_toNat_eq (by simp)
+@[simp] theorem BitVec.ofNat_uInt16ToNat (n : UInt16) : BitVec.ofNat 16 n.toNat = n.toBitVec :=
+  BitVec.eq_of_toNat_eq (by simp)
+@[simp] theorem BitVec.ofNat_uInt32ToNat (n : UInt32) : BitVec.ofNat 32 n.toNat = n.toBitVec :=
+  BitVec.eq_of_toNat_eq (by simp)
+@[simp] theorem BitVec.ofNat_uInt64ToNat (n : UInt64) : BitVec.ofNat 64 n.toNat = n.toBitVec :=
+  BitVec.eq_of_toNat_eq (by simp)
+@[simp] theorem BitVec.ofNat_uSizeToNat (n : USize) : BitVec.ofNat System.Platform.numBits n.toNat = n.toBitVec :=
+  BitVec.eq_of_toNat_eq (by simp)