diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index ae75ef3306..a3fc2de367 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -483,6 +483,36 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
         case zero => exact hmsb
         case succ => exact getMsbD_x _ hi (by omega)
 
+/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_ne_intMin`. -/
+@[simp] theorem signExtend_neg_of_le {v w : Nat} (h : w ≤ v) (b : BitVec v) :
+    (-b).signExtend w = -b.signExtend w := by
+  apply BitVec.eq_of_getElem_eq
+  intro i hi
+  simp only [getElem_signExtend, getElem_neg]
+  rw [dif_pos (by omega), dif_pos (by omega)]
+  simp only [getLsbD_signExtend, Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_true_distrib,
+    Bool.bne_right_inj, decide_eq_decide]
+  exact ⟨fun ⟨j, hj₁, hj₂⟩ => ⟨j, ⟨hj₁, ⟨by omega, by rwa [if_pos (by omega)]⟩⟩⟩,
+    fun ⟨j, hj₁, hj₂, hj₃⟩ => ⟨j, hj₁, by rwa [if_pos (by omega)] at hj₃⟩⟩
+
+/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_le`. -/
+@[simp] theorem signExtend_neg_of_ne_intMin {v w : Nat} (b : BitVec v) (hb : b ≠ intMin v) :
+    (-b).signExtend w = -b.signExtend w := by
+  refine (by omega : w ≤ v ∨ v < w).elim (fun h => signExtend_neg_of_le h b) (fun h => ?_)
+  apply BitVec.eq_of_toInt_eq
+  rw [toInt_signExtend_of_le (by omega), toInt_neg_of_ne_intMin hb, toInt_neg_of_ne_intMin,
+    toInt_signExtend_of_le (by omega)]
+  apply ne_of_apply_ne BitVec.toInt
+  rw [toInt_signExtend_of_le (by omega), toInt_intMin_of_pos (by omega)]
+  have := b.le_toInt
+  have : -2 ^ w < -2 ^ v := by
+    apply Int.neg_lt_neg
+    norm_cast
+    rwa [Nat.pow_lt_pow_iff_right (by omega)]
+  have : 2 * b.toInt ≠ -2 ^ w := by omega
+  rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
+  omega
+
 /-! ### abs -/
 
 theorem msb_abs {w : Nat} {x : BitVec w} :
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 56591c907c..4b36c72d37 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2064,14 +2064,18 @@ theorem msb_signExtend {x : BitVec w} :
   · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
 
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
-theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
+theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   x.signExtend v = x.setWidth v := by
   ext i h
   simp [getElem_signExtend, show i < w by omega]
 
+@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
+theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
+  x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
+
 /-- Sign extending to the same bitwidth is a no op. -/
 @[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
-  rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
+  rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
 
 /-- Sign extending to a larger bitwidth depends on the msb.
 If the msb is false, then the result equals the original value.
@@ -2108,7 +2112,7 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} :
     (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 := by
   by_cases h : v ≤ w
   · have : 2^v ≤ 2^w := Nat.pow_le_pow_right Nat.two_pos h
-    simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
+    simp [signExtend_eq_setWidth_of_le x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
   · have : 2^w ≤ 2^v := Nat.pow_le_pow_right Nat.two_pos (by omega)
     rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]
 
@@ -2144,7 +2148,7 @@ and we compute a modulo by `2^v`.
 -/
 theorem toInt_signExtend_eq_toNat_bmod_of_le {x : BitVec w} (hv : v ≤ w) :
     (x.signExtend v).toInt = Int.bmod x.toNat (2^v) := by
-  simp [signExtend_eq_setWidth_of_lt _ hv]
+  simp [signExtend_eq_setWidth_of_le _ hv]
 
 /--
 Interpreting the sign extension of `(x : BitVec w)` to width `v`
@@ -2168,8 +2172,6 @@ theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) :
     (x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by
   rw [BitVec.toInt_signExtend, Nat.min_eq_left h]
 
-attribute [simp] BitVec.signExtend_eq
-
 /-! ### append -/
 
 theorem append_def (x : BitVec v) (y : BitVec w) :
@@ -4002,7 +4004,6 @@ theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
 /--
 The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
-@[simp]
 theorem toInt_intMin {w : Nat} :
     (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by
   by_cases h : w = 0
@@ -4014,10 +4015,16 @@ theorem toInt_intMin {w : Nat} :
     rw [Nat.mul_comm]
     simp [w_pos]
 
+theorem toInt_intMin_of_pos {v : Nat} (hv : 0 < v) : (intMin v).toInt = -2 ^ (v - 1) := by
+  rw [toInt_intMin, Nat.mod_eq_of_lt]
+  · simp [Int.natCast_pow]
+  · rw [Nat.pow_lt_pow_iff_right (by omega)]
+    omega
+
 theorem toInt_intMin_le (x : BitVec w) :
     (intMin w).toInt ≤ x.toInt := by
   cases w
-  case zero => simp [@of_length_zero x]
+  case zero => simp [toInt_intMin, @of_length_zero x]
   case succ w =>
     simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
@@ -4508,7 +4515,7 @@ abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
 
 @[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
-abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt
+abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_le
 
 @[deprecated truncate_append (since := "2024-09-18")]
 abbrev truncate_append := @setWidth_append
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index 87ce60841d..b2f8940aff 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -8,6 +8,7 @@ import Init.Data.SInt.Basic
 import Init.Data.BitVec.Bitblast
 import Init.Data.Int.LemmasAux
 import Init.Data.UInt.Lemmas
+import Init.System.Platform
 
 open Lean in
 set_option hygiene false in
@@ -71,15 +72,26 @@ theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2^32) :
     (ofNat n).toBitVec.toNat = n :=
   Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le h (by cases USize.size_eq <;> simp_all +decide))
 
-theorem Int8.toInt_ofInt {n : Int} (hn : -2^7 ≤ n) (hn' : n < 2^7) : toInt (ofInt n) = n := by
+@[simp] theorem Int8.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int8.size := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
+@[simp] theorem Int16.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int16.size := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
+@[simp] theorem Int32.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int32.size := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
+@[simp] theorem Int64.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod Int64.size := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
+theorem ISize.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod ISize.size := by
+  rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
+
+theorem Int8.toInt_ofInt_of_le {n : Int} (hn : -2^7 ≤ n) (hn' : n < 2^7) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
-theorem Int16.toInt_ofInt {n : Int} (hn : -2^15 ≤ n) (hn' : n < 2^15) : toInt (ofInt n) = n := by
+theorem Int16.toInt_ofInt_of_le {n : Int} (hn : -2^15 ≤ n) (hn' : n < 2^15) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
-theorem Int32.toInt_ofInt {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
+theorem Int32.toInt_ofInt_of_le {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
-theorem Int64.toInt_ofInt {n : Int} (hn : -2^63 ≤ n) (hn' : n < 2^63) : toInt (ofInt n) = n := by
+theorem Int64.toInt_ofInt_of_le {n : Int} (hn : -2^63 ≤ n) (hn' : n < 2^63) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
-theorem ISize.toInt_ofInt {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
+theorem ISize.toInt_ofInt_of_le {n : Int} (hn : -2^31 ≤ n) (hn' : n < 2^31) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self] <;> cases System.Platform.numBits_eq
     <;> (simp_all; try omega)
 
@@ -90,8 +102,14 @@ theorem ISize.toInt_ofInt_of_two_pow_numBits_le {n : Int} (hn : -2 ^ (System.Pla
 
 theorem ISize.toNatClampNeg_ofInt_eq_zero {n : Int} (hn : -2^31 ≤ n) (hn' : n ≤ 0) :
     toNatClampNeg (ofInt n) = 0 := by
-  rwa [toNatClampNeg, toInt_ofInt hn (by omega), Int.toNat_eq_zero]
+  rwa [toNatClampNeg, toInt_ofInt_of_le hn (by omega), Int.toNat_eq_zero]
 
+theorem Int8.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
+  toBitVec.inj (by simp [BitVec.ofInt_neg])
+theorem Int16.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
+  toBitVec.inj (by simp [BitVec.ofInt_neg])
+theorem Int32.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
+  toBitVec.inj (by simp [BitVec.ofInt_neg])
 theorem Int64.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
   toBitVec.inj (by simp [BitVec.ofInt_neg])
 theorem ISize.neg_ofInt {n : Int} : -ofInt n = ofInt (-n) :=
@@ -103,37 +121,67 @@ theorem Int32.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by s
 theorem Int64.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
 theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
 
+@[simp] theorem Int8.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int8.size := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt]
+@[simp] theorem Int16.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int16.size := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt]
+@[simp] theorem Int32.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int32.size := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt]
+@[simp] theorem Int64.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int64.size := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt]
+@[simp] theorem ISize.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod ISize.size := by
+  rw [← ofInt_eq_ofNat, toInt_ofInt]
+
+theorem Int8.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
+  rw [← neg_ofInt, ofInt_eq_ofNat]
+theorem Int16.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
+  rw [← neg_ofInt, ofInt_eq_ofNat]
+theorem Int32.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
+  rw [← neg_ofInt, ofInt_eq_ofNat]
+theorem Int64.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
+  rw [← neg_ofInt, ofInt_eq_ofNat]
 theorem ISize.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
   rw [← neg_ofInt, ofInt_eq_ofNat]
 
 theorem Int8.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : toNatClampNeg (ofNat n) = n := by
-  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega), Int.toNat_ofNat]
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
+theorem Int16.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : toNatClampNeg (ofNat n) = n := by
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
+theorem Int32.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toNatClampNeg (ofNat n) = n := by
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
+theorem Int64.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : toNatClampNeg (ofNat n) = n := by
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
 theorem ISize.toNatClampNeg_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toNatClampNeg (ofNat n) = n := by
-  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega), Int.toNat_ofNat]
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega), Int.toNat_ofNat]
+theorem ISize.toNatClampNeg_ofNat_of_lt_two_pow_numBits {n : Nat} (h : n < 2 ^ (System.Platform.numBits - 1)) :
+    toNatClampNeg (ofNat n) = n := by
+  rw [toNatClampNeg, ← ofInt_eq_ofNat, toInt_ofInt_of_two_pow_numBits_le, Int.toNat_ofNat]
+  · cases System.Platform.numBits_eq <;> simp_all <;> omega
+  · cases System.Platform.numBits_eq <;> simp_all <;> omega
 
 theorem ISize.toNatClampNeg_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) :
     toNatClampNeg (-ofNat n) = 0 := by
   rw [neg_ofNat, toNatClampNeg_ofInt_eq_zero (by omega) (by omega)]
 
 theorem Int8.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 7) : toInt (ofNat n) = n := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
 theorem Int16.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 15) : toInt (ofNat n) = n := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
 theorem Int32.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toInt (ofNat n) = n := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
 theorem Int64.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 63) : toInt (ofNat n) = n := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
 theorem ISize.toInt_ofNat_of_lt {n : Nat} (h : n < 2 ^ 31) : toInt (ofNat n) = n := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, toInt_ofInt_of_le (by omega) (by omega)]
 theorem ISize.toInt_ofNat_of_lt_two_pow_numBits {n : Nat}
     (h : n < 2 ^ (System.Platform.numBits - 1)) : toInt (ofNat n) = n := by
   rw [← ofInt_eq_ofNat, toInt_ofInt_of_two_pow_numBits_le] <;>
     cases System.Platform.numBits_eq <;> simp_all <;> omega
 
 theorem Int64.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2^63) : toInt (-ofNat n) = -n := by
-  rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt_of_le (by omega) (by omega)]
 theorem ISize.toInt_neg_ofNat_of_le {n : Nat} (h : n ≤ 2 ^ 31) : toInt (-ofNat n) = -n := by
-  rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt (by omega) (by omega)]
+  rw [← ofInt_eq_ofNat, neg_ofInt, toInt_ofInt_of_le (by omega) (by omega)]
 
 theorem Int8.toInt_zero : toInt 0 = 0 := by simp
 theorem Int16.toInt_zero : toInt 0 = 0 := by simp
@@ -141,13 +189,30 @@ theorem Int32.toInt_zero : toInt 0 = 0 := by simp
 theorem Int64.toInt_zero : toInt 0 = 0 := by simp
 theorem ISize.toInt_zero : toInt 0 = 0 := by simp
 
+theorem Int8.toInt_minValue : Int8.minValue.toInt = -2^7 := rfl
+theorem Int16.toInt_minValue : Int16.minValue.toInt = -2^15 := rfl
+theorem Int32.toInt_minValue : Int32.minValue.toInt = -2^31 := rfl
+theorem Int64.toInt_minValue : Int64.minValue.toInt = -2^63 := rfl
 @[simp] theorem ISize.toInt_minValue : ISize.minValue.toInt = -2^(System.Platform.numBits - 1) := by
   rw [minValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq
     <;> simp_all
+
+theorem Int8.toInt_maxValue : Int8.maxValue.toInt = 2 ^ 7 - 1 := rfl
+theorem Int16.toInt_maxValue : Int16.maxValue.toInt = 2 ^ 15 - 1 := rfl
+theorem Int32.toInt_maxValue : Int32.maxValue.toInt = 2 ^ 31 - 1 := rfl
+theorem Int64.toInt_maxValue : Int64.maxValue.toInt = 2 ^ 63 - 1 := rfl
 @[simp] theorem ISize.toInt_maxValue : ISize.maxValue.toInt = 2^(System.Platform.numBits - 1) - 1:= by
   rw [maxValue, toInt_ofInt_of_two_pow_numBits_le] <;> cases System.Platform.numBits_eq
     <;> simp_all
 
+@[simp] theorem Int8.toNatClampNeg_minValue : Int8.minValue.toNatClampNeg = 0 := rfl
+@[simp] theorem Int16.toNatClampNeg_minValue : Int16.minValue.toNatClampNeg = 0 := rfl
+@[simp] theorem Int32.toNatClampNeg_minValue : Int32.minValue.toNatClampNeg = 0 := rfl
+@[simp] theorem Int64.toNatClampNeg_minValue : Int64.minValue.toNatClampNeg = 0 := rfl
+@[simp] theorem ISize.toNatClampNeg_minValue : ISize.minValue.toNatClampNeg = 0 := by
+  rw [toNatClampNeg, toInt_minValue]
+  cases System.Platform.numBits_eq <;> simp_all
+
 @[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
@@ -551,13 +616,13 @@ theorem ISize.ofIntLE_int64ToInt (x : Int64) {h₁ h₂} : ISize.ofIntLE x.toInt
 @[simp] theorem ISize.ofInt_int64ToInt (x : Int64) : ISize.ofInt x.toInt = x.toISize := rfl
 
 @[simp] theorem Int8.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
-  rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
+  rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
 @[simp] theorem Int16.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
-  rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
+  rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
 @[simp] theorem Int32.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
-  rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
+  rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
 @[simp] theorem Int64.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
-  rw [ofIntLE, toInt_ofInt h₁ (Int.lt_of_le_sub_one h₂)]
+  rw [ofIntLE, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
 @[simp] theorem ISize.toInt_ofIntLE {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂).toInt = x := by
   rw [ofIntLE, toInt_ofInt_of_two_pow_numBits_le]
   · simpa using h₁
@@ -575,6 +640,12 @@ theorem Int64.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h
 theorem ISize.ofIntLE_eq_ofIntTruncate {x : Int} {h₁ h₂} : (ofIntLE x h₁ h₂) = ofIntTruncate x := by
   rw [ofIntTruncate, dif_pos h₁, dif_pos h₂]
 
+theorem Int8.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int8.ofIntLE n h₁ h₂ = Int8.ofInt n := rfl
+theorem Int16.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int16.ofIntLE n h₁ h₂ = Int16.ofInt n := rfl
+theorem Int32.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int32.ofIntLE n h₁ h₂ = Int32.ofInt n := rfl
+theorem Int64.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : Int64.ofIntLE n h₁ h₂ = Int64.ofInt n := rfl
+theorem ISize.ofIntLE_eq_ofInt {n : Int} (h₁ h₂) : ISize.ofIntLE n h₁ h₂ = ISize.ofInt n := rfl
+
 theorem Int8.toInt_ofIntTruncate {x : Int} (h₁ : Int8.minValue.toInt ≤ x)
     (h₂ : x ≤ Int8.maxValue.toInt) : (Int8.ofIntTruncate x).toInt = x := by
   rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toInt_ofIntLE]
@@ -865,3 +936,473 @@ theorem USize.toISize_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toISize = IS
 @[simp] theorem UInt32.toInt32_ofBitVec (b) : (UInt32.ofBitVec b).toInt32 = Int32.ofBitVec b := rfl
 @[simp] theorem UInt64.toInt64_ofBitVec (b) : (UInt64.ofBitVec b).toInt64 = Int64.ofBitVec b := rfl
 @[simp] theorem USize.toInt8_ofBitVec (b) : (USize.ofBitVec b).toISize = ISize.ofBitVec b := rfl
+
+@[simp] theorem Int8.toBitVec_ofBitVec (b) : (Int8.ofBitVec b).toBitVec = b := rfl
+@[simp] theorem Int16.toBitVec_ofBitVec (b) : (Int16.ofBitVec b).toBitVec = b := rfl
+@[simp] theorem Int32.toBitVec_ofBitVec (b) : (Int32.ofBitVec b).toBitVec = b := rfl
+@[simp] theorem Int64.toBitVec_ofBitVec (b) : (Int64.ofBitVec b).toBitVec = b := rfl
+@[simp] theorem ISize.toBitVec_ofBitVec (b) : (ISize.ofBitVec b).toBitVec = b := rfl
+
+theorem Int8.toBitVec_ofIntTruncate {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
+theorem Int16.toBitVec_ofIntTruncate {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
+theorem Int32.toBitVec_ofIntTruncate {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
+    (Int32.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
+theorem Int64.toBitVec_ofIntTruncate {n : Int} (h₁ : Int64.minValue.toInt ≤ n) (h₂ : n ≤ Int64.maxValue.toInt) :
+    (Int64.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
+theorem ISize.toBitVec_ofIntTruncate {n : Int} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt) :
+    (ISize.ofIntTruncate n).toBitVec = BitVec.ofInt _ n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := h₂), toBitVec_ofIntLE]
+
+@[simp] theorem Int8.toInt_ofBitVec (b) : (Int8.ofBitVec b).toInt = b.toInt := rfl
+@[simp] theorem Int16.toInt_ofBitVec (b) : (Int16.ofBitVec b).toInt = b.toInt := rfl
+@[simp] theorem Int32.toInt_ofBitVec (b) : (Int32.ofBitVec b).toInt = b.toInt := rfl
+@[simp] theorem Int64.toInt_ofBitVec (b) : (Int64.ofBitVec b).toInt = b.toInt := rfl
+@[simp] theorem ISize.toInt_ofBitVec (b) : (ISize.ofBitVec b).toInt = b.toInt := rfl
+
+@[simp] theorem Int8.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int8.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
+  rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
+@[simp] theorem Int16.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int16.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
+  rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
+@[simp] theorem Int32.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
+  rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
+@[simp] theorem Int64.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
+  rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_le h₁ (Int.lt_of_le_sub_one h₂)]
+@[simp] theorem ISize.toNatClampNeg_ofIntLE {n : Int} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat := by
+  rw [ofIntLE, toNatClampNeg, toInt_ofInt_of_two_pow_numBits_le]
+  · rwa [← ISize.toInt_minValue]
+  · apply Int.lt_of_le_sub_one
+    rwa [← ISize.toInt_maxValue]
+
+@[simp] theorem Int8.toNatClampNeg_ofBitVec (b) : (Int8.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
+@[simp] theorem Int16.toNatClampNeg_ofBitVec (b) : (Int16.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
+@[simp] theorem Int32.toNatClampNeg_ofBitVec (b) : (Int32.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
+@[simp] theorem Int64.toNatClampNeg_ofBitVec (b) : (Int64.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
+@[simp] theorem ISize.toNatClampNeg_ofBitVec (b) : (ISize.ofBitVec b).toNatClampNeg = b.toInt.toNat := rfl
+
+theorem Int8.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 7 ≤ n) (h₂ : n < 2 ^ 7) :
+    (Int8.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
+theorem Int16.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
+    (Int16.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
+theorem Int32.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
+    (Int32.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
+theorem Int64.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
+    (Int64.ofInt n).toNatClampNeg = n.toNat := by rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
+theorem ISize.toNatClampNeg_ofInt_of_le {n : Int} (h₁ : -2 ^ 31 ≤ n)
+    (h₂ : n < 2 ^ 31) : (ISize.ofInt n).toNatClampNeg = n.toNat := by
+  rw [toNatClampNeg, toInt_ofInt_of_le h₁ h₂]
+theorem ISize.toNatClampNeg_ofInt_of_two_pow_numBits {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
+    (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofInt n).toNatClampNeg = n.toNat := by
+  rw [toNatClampNeg, toInt_ofInt_of_two_pow_numBits_le h₁ h₂]
+
+theorem Int8.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 7) :
+    (Int8.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  rw [ofIntTruncate]
+  split
+  · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
+  · next h =>
+    rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
+    rw [toInt_minValue] at h
+    omega
+theorem Int16.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 15) :
+    (Int16.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  rw [ofIntTruncate]
+  split
+  · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
+  · next h =>
+    rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
+    rw [toInt_minValue] at h
+    omega
+theorem Int32.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
+    (Int32.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  rw [ofIntTruncate]
+  split
+  · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
+  · next h =>
+    rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
+    rw [toInt_minValue] at h
+    omega
+theorem Int64.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 63) :
+    (Int64.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  rw [ofIntTruncate]
+  split
+  · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
+  · next h =>
+    rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
+    rw [toInt_minValue] at h
+    omega
+theorem ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits {n : Int} (h₁ : n < 2 ^ (System.Platform.numBits - 1)) :
+    (ISize.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  rw [ofIntTruncate]
+  split
+  · rw [dif_pos (by rw [toInt_maxValue]; omega), toNatClampNeg_ofIntLE]
+  · next h =>
+    rw [toNatClampNeg_minValue, eq_comm, Int.toNat_eq_zero]
+    rw [toInt_minValue] at h
+    omega
+theorem ISize.toNatClampNeg_ofIntTruncate_of_lt {n : Int} (h₁ : n < 2 ^ 31) :
+    (ISize.ofIntTruncate n).toNatClampNeg = n.toNat := by
+  apply ISize.toNatClampNeg_ofIntTruncate_of_lt_two_pow_numBits (Int.lt_of_lt_of_le h₁ _)
+  cases System.Platform.numBits_eq <;> simp_all
+
+@[simp] theorem Int8.toUInt8_ofBitVec (b) : (Int8.ofBitVec b).toUInt8 = UInt8.ofBitVec b := rfl
+@[simp] theorem Int16.toUInt16_ofBitVec (b) : (Int16.ofBitVec b).toUInt16 = UInt16.ofBitVec b := rfl
+@[simp] theorem Int32.toUInt32_ofBitVec (b) : (Int32.ofBitVec b).toUInt32 = UInt32.ofBitVec b := rfl
+@[simp] theorem Int64.toUInt64_ofBitVec (b) : (Int64.ofBitVec b).toUInt64 = UInt64.ofBitVec b := rfl
+@[simp] theorem ISize.toUSize_ofBitVec (b) : (ISize.ofBitVec b).toUSize = USize.ofBitVec b := rfl
+
+@[simp] theorem Int8.toUInt8_ofNat' {n} : (Int8.ofNat n).toUInt8 = UInt8.ofNat n := rfl
+@[simp] theorem Int16.toUInt16_ofNat' {n} : (Int16.ofNat n).toUInt16 = UInt16.ofNat n := rfl
+@[simp] theorem Int32.toUInt32_ofNat' {n} : (Int32.ofNat n).toUInt32 = UInt32.ofNat n := rfl
+@[simp] theorem Int64.toUInt64_ofNat' {n} : (Int64.ofNat n).toUInt64 = UInt64.ofNat n := rfl
+@[simp] theorem ISize.toUSize_ofNat' {n} : (ISize.ofNat n).toUSize = USize.ofNat n := rfl
+
+@[simp] theorem Int8.toUInt8_ofNat {n} : toUInt8 (OfNat.ofNat n) = OfNat.ofNat n := rfl
+@[simp] theorem Int16.toUInt16_ofNat {n} : toUInt16 (OfNat.ofNat n) = OfNat.ofNat n := rfl
+@[simp] theorem Int32.toUInt32_ofNat {n} : toUInt32 (OfNat.ofNat n) = OfNat.ofNat n := rfl
+@[simp] theorem Int64.toUInt64_ofNat {n} : toUInt64 (OfNat.ofNat n) = OfNat.ofNat n := rfl
+@[simp] theorem ISize.toUISize_ofNat {n} : toUSize (OfNat.ofNat n) = OfNat.ofNat n := rfl
+
+theorem Int16.toInt8_ofIntLE {n} (h₁ h₂) : (Int16.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
+theorem Int32.toInt8_ofIntLE {n} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
+theorem Int64.toInt8_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
+theorem ISize.toInt8_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n := Int8.toInt.inj (by simp)
+
+@[simp] theorem Int16.toInt8_ofBitVec (b) : (Int16.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int32.toInt8_ofBitVec (b) : (Int32.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int64.toInt8_ofBitVec (b) : (Int64.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem ISize.toInt8_ofBitVec (b) : (ISize.ofBitVec b).toInt8 = Int8.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int16.toInt8_ofNat' {n} : (Int16.ofNat n).toInt8 = Int8.ofNat n :=
+  Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem Int32.toInt8_ofNat' {n} : (Int32.ofNat n).toInt8 = Int8.ofNat n :=
+  Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem Int64.toInt8_ofNat' {n} : (Int64.ofNat n).toInt8 = Int8.ofNat n :=
+  Int8.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem ISize.toInt8_ofNat' {n} : (ISize.ofNat n).toInt8 = Int8.ofNat n := by
+  apply Int8.toBitVec.inj
+  simp only [toBitVec_toInt8, toBitVec_ofNat', Int8.toBitVec_ofNat']
+  rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
+  all_goals cases System.Platform.numBits_eq <;> simp_all
+
+@[simp] theorem Int16.toInt8_ofInt {n} : (Int16.ofInt n).toInt8 = Int8.ofInt n :=
+  Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem Int32.toInt8_ofInt {n} : (Int32.ofInt n).toInt8 = Int8.ofInt n :=
+  Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem Int64.toInt8_ofInt {n} : (Int64.ofInt n).toInt8 = Int8.ofInt n :=
+  Int8.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem ISize.toInt8_ofInt {n} : (ISize.ofInt n).toInt8 = Int8.ofInt n := by
+  apply Int8.toInt.inj
+  simp only [toInt_toInt8, toInt_ofInt, Nat.reducePow, Int8.toInt_ofInt]
+  exact Int.bmod_bmod_of_dvd UInt8.size_dvd_usizeSize
+
+@[simp] theorem Int16.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
+@[simp] theorem Int32.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
+@[simp] theorem Int64.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
+@[simp] theorem ISize.toInt8_ofNat {n} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt8_ofNat'
+
+theorem Int16.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 15 ≤ n) (h₂ : n < 2 ^ 15) :
+    (Int16.ofIntTruncate n).toInt8 = Int8.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
+theorem Int32.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
+    (Int32.ofIntTruncate n).toInt8 = Int8.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
+theorem Int64.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
+    (Int64.ofIntTruncate n).toInt8 = Int8.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt8_ofIntLE]
+theorem ISize.toInt8_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
+    (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt8 = Int8.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate, toInt8_ofIntLE]
+  · exact toInt_minValue ▸ h₁
+  · rw [toInt_maxValue]
+    omega
+
+theorem Int32.toInt16_ofIntLE {n} (h₁ h₂) : (Int32.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
+theorem Int64.toInt16_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
+theorem ISize.toInt16_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt16 = Int16.ofInt n := Int16.toInt.inj (by simp)
+
+@[simp] theorem Int32.toInt16_ofBitVec (b) : (Int32.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int64.toInt16_ofBitVec (b) : (Int64.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem ISize.toInt16_ofBitVec (b) : (ISize.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int32.toInt16_ofNat' {n} : (Int32.ofNat n).toInt16 = Int16.ofNat n :=
+  Int16.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem Int64.toInt16_ofNat' {n} : (Int64.ofNat n).toInt16 = Int16.ofNat n :=
+  Int16.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem ISize.toInt16_ofNat' {n} : (ISize.ofNat n).toInt16 = Int16.ofNat n := by
+  apply Int16.toBitVec.inj
+  simp only [toBitVec_toInt16, toBitVec_ofNat', Int16.toBitVec_ofNat']
+  rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
+  all_goals cases System.Platform.numBits_eq <;> simp_all
+
+@[simp] theorem Int32.toInt16_ofInt {n} : (Int32.ofInt n).toInt16 = Int16.ofInt n :=
+  Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem Int64.toInt16_ofInt {n} : (Int64.ofInt n).toInt16 = Int16.ofInt n :=
+  Int16.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem ISize.toInt16_ofInt {n} : (ISize.ofInt n).toInt16 = Int16.ofInt n := by
+  apply Int16.toInt.inj
+  simp only [toInt_toInt16, toInt_ofInt, Nat.reducePow, Int16.toInt_ofInt]
+  exact Int.bmod_bmod_of_dvd UInt16.size_dvd_usizeSize
+
+@[simp] theorem Int32.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
+@[simp] theorem Int64.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
+@[simp] theorem ISize.toInt16_ofNat {n} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt16_ofNat'
+
+theorem Int32.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 31 ≤ n) (h₂ : n < 2 ^ 31) :
+    (Int32.ofIntTruncate n).toInt16 = Int16.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
+theorem Int64.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
+    (Int64.ofIntTruncate n).toInt16 = Int16.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt16_ofIntLE]
+theorem ISize.toInt16_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
+    (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt16 = Int16.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate, toInt16_ofIntLE]
+  · exact toInt_minValue ▸ h₁
+  · rw [toInt_maxValue]
+    omega
+
+theorem Int64.toInt32_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n := Int32.toInt.inj (by simp)
+theorem ISize.toInt32_ofIntLE {n} (h₁ h₂) : (ISize.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n := Int32.toInt.inj (by simp)
+
+@[simp] theorem Int64.toInt32_ofBitVec (b) : (Int64.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem ISize.toInt32_ofBitVec (b) : (ISize.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int64.toInt32_ofNat' {n} : (Int64.ofNat n).toInt32 = Int32.ofNat n :=
+  Int32.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+@[simp] theorem ISize.toInt32_ofNat' {n} : (ISize.ofNat n).toInt32 = Int32.ofNat n := by
+  apply Int32.toBitVec.inj
+  simp only [toBitVec_toInt32, toBitVec_ofNat', Int32.toBitVec_ofNat']
+  rw [BitVec.signExtend_eq_setWidth_of_le, BitVec.setWidth_ofNat_of_le]
+  all_goals cases System.Platform.numBits_eq <;> simp_all
+
+@[simp] theorem Int64.toInt32_ofInt {n} : (Int64.ofInt n).toInt32 = Int32.ofInt n :=
+  Int32.toInt.inj (by simpa using Int.bmod_bmod_of_dvd (by decide))
+@[simp] theorem ISize.toInt32_ofInt {n} : (ISize.ofInt n).toInt32 = Int32.ofInt n := by
+  apply Int32.toInt.inj
+  simp only [toInt_toInt32, toInt_ofInt, Nat.reducePow, Int32.toInt_ofInt]
+  exact Int.bmod_bmod_of_dvd UInt32.size_dvd_usizeSize
+
+@[simp] theorem Int64.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
+@[simp] theorem ISize.toInt32_ofNat {n} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toInt32_ofNat'
+
+theorem Int64.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
+    (Int64.ofIntTruncate n).toInt32 = Int32.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toInt32_ofIntLE]
+theorem ISize.toInt32_ofIntTruncate {n : Int} (h₁ : -2 ^ (System.Platform.numBits - 1) ≤ n)
+    (h₂ : n < 2 ^ (System.Platform.numBits - 1)) : (ISize.ofIntTruncate n).toInt32 = Int32.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate, toInt32_ofIntLE]
+  · exact toInt_minValue ▸ h₁
+  · rw [toInt_maxValue]
+    omega
+
+theorem Int64.toISize_ofIntLE {n} (h₁ h₂) : (Int64.ofIntLE n h₁ h₂).toISize = ISize.ofInt n :=
+  ISize.toInt.inj (by simp [ISize.toInt_ofInt])
+
+@[simp] theorem Int64.toISize_ofBitVec (b) : (Int64.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int64.toISize_ofNat' {n} : (Int64.ofNat n).toISize = ISize.ofNat n :=
+  ISize.toBitVec.inj (by simp [BitVec.signExtend_eq_setWidth_of_le])
+
+@[simp] theorem Int64.toISize_ofInt {n} : (Int64.ofInt n).toISize = ISize.ofInt n :=
+ ISize.toInt.inj (by simpa [ISize.toInt_ofInt] using Int.bmod_bmod_of_dvd USize.size_dvd_uInt64Size)
+
+@[simp] theorem Int64.toISize_ofNat {n} : toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toISize_ofNat'
+
+theorem Int64.toISize_ofIntTruncate {n : Int} (h₁ : -2 ^ 63 ≤ n) (h₂ : n < 2 ^ 63) :
+    (Int64.ofIntTruncate n).toISize = ISize.ofInt n := by
+  rw [← ofIntLE_eq_ofIntTruncate (h₁ := h₁) (h₂ := Int.le_of_lt_add_one h₂), toISize_ofIntLE]
+
+@[simp] theorem Int8.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
+@[simp] theorem Int16.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
+@[simp] theorem Int32.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
+@[simp] theorem Int64.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ := rfl
+@[simp] theorem ISize.toBitVec_minValue : minValue.toBitVec = BitVec.intMin _ :=
+  BitVec.eq_of_toInt_eq (by rw [toInt_toBitVec, toInt_minValue,
+    BitVec.toInt_intMin_of_pos (by cases System.Platform.numBits_eq <;> simp_all)])
+
+@[simp] theorem Int16.toInt8_neg (x : Int16) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
+@[simp] theorem Int32.toInt8_neg (x : Int32) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
+@[simp] theorem Int64.toInt8_neg (x : Int64) : (-x).toInt8 = -x.toInt8 := Int8.toBitVec.inj (by simp)
+@[simp] theorem ISize.toInt8_neg (x : ISize) : (-x).toInt8 = -x.toInt8 :=
+  Int8.toBitVec.inj (by rw [toBitVec_toInt8, toBitVec_neg, Int8.toBitVec_neg, toBitVec_toInt8,
+    BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
+
+@[simp] theorem Int32.toInt16_neg (x : Int32) : (-x).toInt16 = -x.toInt16 := Int16.toBitVec.inj (by simp)
+@[simp] theorem Int64.toInt16_neg (x : Int64) : (-x).toInt16 = -x.toInt16 := Int16.toBitVec.inj (by simp)
+@[simp] theorem ISize.toInt16_neg (x : ISize) : (-x).toInt16 = -x.toInt16 :=
+  Int16.toBitVec.inj (by rw [toBitVec_toInt16, toBitVec_neg, Int16.toBitVec_neg, toBitVec_toInt16,
+    BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
+
+@[simp] theorem Int64.toInt32_neg (x : Int64) : (-x).toInt32 = -x.toInt32 := Int32.toBitVec.inj (by simp)
+@[simp] theorem ISize.toInt32_neg (x : ISize) : (-x).toInt32 = -x.toInt32 :=
+  Int32.toBitVec.inj (by rw [toBitVec_toInt32, toBitVec_neg, Int32.toBitVec_neg, toBitVec_toInt32,
+    BitVec.signExtend_neg_of_le (by cases System.Platform.numBits_eq <;> simp_all)])
+
+@[simp] theorem Int64.toISize_neg (x : Int64) : (-x).toISize = -x.toISize := ISize.toBitVec.inj (by simp)
+
+@[simp] theorem Int8.toInt16_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt16 = -x.toInt16 :=
+  Int16.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
+
+@[simp] theorem Int8.toInt32_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt32 = -x.toInt32 :=
+  Int32.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
+@[simp] theorem Int16.toInt32_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt32 = -x.toInt32 :=
+  Int32.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
+
+@[simp] theorem Int8.toISize_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toISize = -x.toISize :=
+  ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
+@[simp] theorem Int16.toISize_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toISize = -x.toISize :=
+  ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
+@[simp] theorem Int32.toISize_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toISize = -x.toISize :=
+  ISize.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int32.toBitVec.inj h)))
+
+@[simp] theorem Int8.toInt64_neg_of_ne {x : Int8} (hx : x ≠ -128) : (-x).toInt64 = -x.toInt64 :=
+  Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int8.toBitVec.inj h)))
+@[simp] theorem Int16.toInt64_neg_of_ne {x : Int16} (hx : x ≠ -32768) : (-x).toInt64 = -x.toInt64 :=
+  Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _ (fun h => hx (Int16.toBitVec.inj h)))
+@[simp] theorem Int32.toInt64_neg_of_ne {x : Int32} (hx : x ≠ -2147483648) : (-x).toInt64 = -x.toInt64 :=
+  Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _  (fun h => hx (Int32.toBitVec.inj h)))
+@[simp] theorem ISize.toInt64_neg_of_ne {x : ISize} (hx : x ≠ minValue) : (-x).toInt64 = -x.toInt64 :=
+  Int64.toBitVec.inj (BitVec.signExtend_neg_of_ne_intMin _
+    (fun h => hx (ISize.toBitVec.inj (h.trans toBitVec_minValue.symm))))
+
+theorem Int8.toInt16_ofIntLE {n : Int} (h₁ h₂) :
+    (Int8.ofIntLE n h₁ h₂).toInt16 = Int16.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int16.toInt.inj (by simp)
+theorem Int8.toInt32_ofIntLE {n : Int} (h₁ h₂) :
+    (Int8.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int32.toInt.inj (by simp)
+theorem Int8.toInt64_ofIntLE {n : Int} (h₁ h₂) :
+    (Int8.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int64.toInt.inj (by simp)
+theorem Int8.toISize_ofIntLE {n : Int} (h₁ h₂) :
+    (Int8.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
+      (Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
+  ISize.toInt.inj (by simp)
+
+@[simp] theorem Int8.toInt16_ofBitVec (b) : (Int8.ofBitVec b).toInt16 = Int16.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int8.toInt32_ofBitVec (b) : (Int8.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int8.toInt64_ofBitVec (b) : (Int8.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int8.toISize_ofBitVec (b) : (Int8.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int8.toInt16_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofInt n).toInt16 = Int16.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt16_ofIntLE, Int16.ofIntLE_eq_ofInt]
+@[simp] theorem Int8.toInt32_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofInt n).toInt32 = Int32.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt32_ofIntLE, Int32.ofIntLE_eq_ofInt]
+@[simp] theorem Int8.toInt64_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
+@[simp] theorem Int8.toISize_ofInt {n : Int} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofInt n).toISize = ISize.ofInt n := by rw [← Int8.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
+
+@[simp] theorem Int8.toInt16_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofNat n).toInt16 = Int16.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt16_ofInt (by simp [toInt_minValue]) h, Int16.ofInt_eq_ofNat]
+@[simp] theorem Int8.toInt32_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofNat n).toInt32 = Int32.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt32_ofInt (by simp [toInt_minValue]) h, Int32.ofInt_eq_ofNat]
+@[simp] theorem Int8.toInt64_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofNat n).toInt64 = Int64.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
+@[simp] theorem Int8.toISize_ofNat' {n : Nat} (h : n ≤ Int8.maxValue.toInt) :
+    (Int8.ofNat n).toISize = ISize.ofNat n := by
+  rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
+
+@[simp] theorem Int8.toInt16_ofNat {n : Nat} (h : n ≤ 127) :
+    toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt16_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int8.toInt32_ofNat {n : Nat} (h : n ≤ 127) :
+    toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt32_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int8.toInt64_ofNat {n : Nat} (h : n ≤ 127) :
+    toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int8.toISize_ofNat {n : Nat} (h : n ≤ 127) :
+    toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int8.toISize_ofNat' (by rw [toInt_maxValue]; omega)
+
+theorem Int16.toInt32_ofIntLE {n : Int} (h₁ h₂) :
+    (Int16.ofIntLE n h₁ h₂).toInt32 = Int32.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int32.toInt.inj (by simp)
+theorem Int16.toInt64_ofIntLE {n : Int} (h₁ h₂) :
+    (Int16.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int64.toInt.inj (by simp)
+theorem Int16.toISize_ofIntLE {n : Int} (h₁ h₂) :
+    (Int16.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
+      (Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
+  ISize.toInt.inj (by simp)
+
+@[simp] theorem Int16.toInt32_ofBitVec (b) : (Int16.ofBitVec b).toInt32 = Int32.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int16.toInt64_ofBitVec (b) : (Int16.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int16.toISize_ofBitVec (b) : (Int16.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int16.toInt32_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofInt n).toInt32 = Int32.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toInt32_ofIntLE, Int32.ofIntLE_eq_ofInt]
+@[simp] theorem Int16.toInt64_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
+@[simp] theorem Int16.toISize_ofInt {n : Int} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofInt n).toISize = ISize.ofInt n := by rw [← Int16.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
+
+@[simp] theorem Int16.toInt32_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofNat n).toInt32 = Int32.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt32_ofInt (by simp [toInt_minValue]) h, Int32.ofInt_eq_ofNat]
+@[simp] theorem Int16.toInt64_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofNat n).toInt64 = Int64.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
+@[simp] theorem Int16.toISize_ofNat' {n : Nat} (h : n ≤ Int16.maxValue.toInt) :
+    (Int16.ofNat n).toISize = ISize.ofNat n := by
+  rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
+
+@[simp] theorem Int16.toInt32_ofNat {n : Nat} (h : n ≤ 32767) :
+    toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toInt32_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int16.toInt64_ofNat {n : Nat} (h : n ≤ 32767) :
+    toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int16.toISize_ofNat {n : Nat} (h : n ≤ 32767) :
+    toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int16.toISize_ofNat' (by rw [toInt_maxValue]; omega)
+
+theorem Int32.toInt64_ofIntLE {n : Int} (h₁ h₂) :
+    (Int32.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans (by decide) h₁) (Int.le_trans h₂ (by decide)) :=
+  Int64.toInt.inj (by simp)
+theorem Int32.toISize_ofIntLE {n : Int} (h₁ h₂) :
+    (Int32.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n (Int.le_trans minValue.iSizeMinValue_le_toInt h₁)
+      (Int.le_trans h₂ maxValue.toInt_le_iSizeMaxValue) :=
+  ISize.toInt.inj (by simp)
+
+@[simp] theorem Int32.toInt64_ofBitVec (b) : (Int32.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
+@[simp] theorem Int32.toISize_ofBitVec (b) : (Int32.ofBitVec b).toISize = ISize.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem Int32.toInt64_ofInt {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
+    (Int32.ofInt n).toInt64 = Int64.ofInt n := by rw [← Int32.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
+@[simp] theorem Int32.toISize_ofInt {n : Int} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt) :
+    (Int32.ofInt n).toISize = ISize.ofInt n := by rw [← Int32.ofIntLE_eq_ofInt h₁ h₂, toISize_ofIntLE, ISize.ofIntLE_eq_ofInt]
+
+@[simp] theorem Int32.toInt64_ofNat' {n : Nat} (h : n ≤ Int32.maxValue.toInt) :
+    (Int32.ofNat n).toInt64 = Int64.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt64_ofInt (by simp [toInt_minValue]) h, Int64.ofInt_eq_ofNat]
+@[simp] theorem Int32.toISize_ofNat' {n : Nat} (h : n ≤ Int32.maxValue.toInt) :
+    (Int32.ofNat n).toISize = ISize.ofNat n := by
+  rw [← ofInt_eq_ofNat, toISize_ofInt (by simp [toInt_minValue]) h, ISize.ofInt_eq_ofNat]
+
+@[simp] theorem Int32.toInt64_ofNat {n : Nat} (h : n ≤ 2147483647) :
+    toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int32.toInt64_ofNat' (by rw [toInt_maxValue]; omega)
+@[simp] theorem Int32.toISize_ofNat {n : Nat} (h : n ≤ 2147483647) :
+    toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := Int32.toISize_ofNat' (by rw [toInt_maxValue]; omega)
+
+theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) :
+    (ISize.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n (Int.le_trans minValue.int64MinValue_le_toInt h₁)
+      (Int.le_trans h₂ maxValue.toInt_le_int64MaxValue) :=
+  Int64.toInt.inj (by simp)
+
+@[simp] theorem ISize.toInt64_ofBitVec (b) : (ISize.ofBitVec b).toInt64 = Int64.ofBitVec (b.signExtend _) := rfl
+
+@[simp] theorem ISize.toInt64_ofInt {n : Int} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt) :
+    (ISize.ofInt n).toInt64 = Int64.ofInt n := by rw [← ISize.ofIntLE_eq_ofInt h₁ h₂, toInt64_ofIntLE, Int64.ofIntLE_eq_ofInt]
+
+@[simp] theorem ISize.toInt64_ofNat' {n : Nat} (h : n ≤ ISize.maxValue.toInt) :
+    (ISize.ofNat n).toInt64 = Int64.ofNat n := by
+  rw [← ofInt_eq_ofNat, toInt64_ofInt _ h, Int64.ofInt_eq_ofNat]
+  refine Int.le_trans ?_ (Int.zero_le_ofNat _)
+  cases System.Platform.numBits_eq <;> simp_all
+
+@[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)
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 4da67e0f99..3da3d818b4 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1205,3 +1205,51 @@ theorem USize.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
 theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
     (USize.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (USize.size - 1) (by cases USize.size_eq <;> simp_all +decide) :=
   UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt8.toUInt16_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt16 = UInt16.ofNat n := by
+  rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt16_ofNatLT, UInt16.ofNatLT_eq_ofNat]
+@[simp] theorem UInt8.toUInt32_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt32 = UInt32.ofNat n := by
+  rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt32_ofNatLT, UInt32.ofNatLT_eq_ofNat]
+@[simp] theorem UInt8.toUInt64_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUInt64 = UInt64.ofNat n := by
+  rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
+@[simp] theorem UInt8.toUSize_ofNat' {n : Nat} (hn : n < UInt8.size) : (UInt8.ofNat n).toUSize = USize.ofNat n := by
+  rw [← UInt8.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
+
+@[simp] theorem UInt16.toUInt32_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUInt32 = UInt32.ofNat n := by
+  rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUInt32_ofNatLT, UInt32.ofNatLT_eq_ofNat]
+@[simp] theorem UInt16.toUInt64_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUInt64 = UInt64.ofNat n := by
+  rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
+@[simp] theorem UInt16.toUSize_ofNat' {n : Nat} (hn : n < UInt16.size) : (UInt16.ofNat n).toUSize = USize.ofNat n := by
+  rw [← UInt16.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
+
+@[simp] theorem UInt32.toUInt64_ofNat' {n : Nat} (hn : n < UInt32.size) : (UInt32.ofNat n).toUInt64 = UInt64.ofNat n := by
+  rw [← UInt32.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
+@[simp] theorem UInt32.toUSize_ofNat' {n : Nat} (hn : n < UInt32.size) : (UInt32.ofNat n).toUSize = USize.ofNat n := by
+  rw [← UInt32.ofNatLT_eq_ofNat (h := hn), toUSize_ofNatLT, USize.ofNatLT_eq_ofNat]
+
+@[simp] theorem USize.toUInt64_ofNat' {n : Nat} (hn : n < USize.size) : (USize.ofNat n).toUInt64 = UInt64.ofNat n := by
+  rw [← USize.ofNatLT_eq_ofNat (h := hn), toUInt64_ofNatLT, UInt64.ofNatLT_eq_ofNat]
+
+@[simp] theorem UInt8.toUInt16_ofNat {n : Nat} (hn : n < 256) : toUInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt8.toUInt16_ofNat' hn
+@[simp] theorem UInt8.toUInt32_ofNat {n : Nat} (hn : n < 256) : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt8.toUInt32_ofNat' hn
+@[simp] theorem UInt8.toUInt64_ofNat {n : Nat} (hn : n < 256) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt8.toUInt64_ofNat' hn
+@[simp] theorem UInt8.toUSize_ofNat {n : Nat} (hn : n < 256) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt8.toUSize_ofNat' hn
+
+@[simp] theorem UInt16.toUInt32_ofNat {n : Nat} (hn : n < 65536) : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt16.toUInt32_ofNat' hn
+@[simp] theorem UInt16.toUInt64_ofNat {n : Nat} (hn : n < 65536) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt16.toUInt64_ofNat' hn
+@[simp] theorem UInt16.toUSize_ofNat {n : Nat} (hn : n < 65536) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt16.toUSize_ofNat' hn
+
+@[simp] theorem UInt32.toUInt64_ofNat {n : Nat} (hn : n < 4294967296) : toUInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt32.toUInt64_ofNat' hn
+@[simp] theorem UInt32.toUSize_ofNat {n : Nat} (hn : n < 4294967296) : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
+  UInt32.toUSize_ofNat' hn
+
+@[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)
diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean
index 062532123e..14afae6cb7 100644
--- a/src/Init/System/Platform.lean
+++ b/src/Init/System/Platform.lean
@@ -26,9 +26,11 @@ def target : String := getTarget ()
 theorem numBits_pos : 0 < numBits := by
   cases numBits_eq <;> next h => simp [h]
 
+@[simp]
 theorem le_numBits : 32 ≤ numBits := by
   cases numBits_eq <;> next h => simp [h]
 
+@[simp]
 theorem numBits_le : numBits ≤ 64 := by
   cases numBits_eq <;> next h => simp [h]
 
diff --git a/tests/lean/run/simpSInt.lean b/tests/lean/run/simpSInt.lean
new file mode 100644
index 0000000000..ab728839f5
--- /dev/null
+++ b/tests/lean/run/simpSInt.lean
@@ -0,0 +1,73 @@
+#check_simp (-64 : Int8).toBitVec ~> 192#8
+#check_simp (-64 : Int16).toBitVec ~> 65472#16
+#check_simp (-64 : Int32).toBitVec ~> 4294967232#32
+#check_simp (-64 : Int64).toBitVec ~> 18446744073709551552#64
+
+#check_simp (64 : UInt8).toUInt16 ~> 64
+#check_simp (64 : UInt8).toUInt32 ~> 64
+#check_simp (64 : UInt8).toUInt64 ~> 64
+#check_simp (64 : UInt8).toUSize ~> 64
+
+#check_simp (64 : UInt16).toUInt8 ~> 64
+#check_simp (64 : UInt16).toUInt32 ~> 64
+#check_simp (64 : UInt16).toUInt64 ~> 64
+#check_simp (64 : UInt16).toUSize ~> 64
+
+#check_simp (64 : UInt32).toUInt8 ~> 64
+#check_simp (64 : UInt32).toUInt16 ~> 64
+#check_simp (64 : UInt32).toUInt64 ~> 64
+#check_simp (64 : UInt32).toUSize ~> 64
+
+#check_simp (64 : UInt64).toUInt8 ~> 64
+#check_simp (64 : UInt64).toUInt16 ~> 64
+#check_simp (64 : UInt64).toUInt32 ~> 64
+#check_simp (64 : UInt64).toUSize ~> 64
+
+#check_simp (64 : USize).toUInt8 ~> 64
+#check_simp (64 : USize).toUInt16 ~> 64
+#check_simp (64 : USize).toUInt32 ~> 64
+
+#check_simp (-64 : Int8).toInt16 ~> -64
+#check_simp (-64 : Int8).toInt32 ~> -64
+#check_simp (-64 : Int8).toInt64 ~> -64
+#check_simp (-64 : Int8).toISize ~> -64
+
+#check_simp (-64 : Int16).toInt8 ~> -64
+#check_simp (-64 : Int16).toInt32 ~> -64
+#check_simp (-64 : Int16).toInt64 ~> -64
+#check_simp (-64 : Int16).toISize ~> -64
+
+#check_simp (-64 : Int32).toInt8 ~> -64
+#check_simp (-64 : Int32).toInt16 ~> -64
+#check_simp (-64 : Int32).toInt64 ~> -64
+#check_simp (-64 : Int32).toISize ~> -64
+
+#check_simp (-64 : Int64).toInt8 ~> -64
+#check_simp (-64 : Int64).toInt16 ~> -64
+#check_simp (-64 : Int64).toInt32 ~> -64
+#check_simp (-64 : Int64).toISize ~> -64
+
+#check_simp (-64 : ISize).toInt8 ~> -64
+#check_simp (-64 : ISize).toInt16 ~> -64
+#check_simp (-64 : ISize).toInt32 ~> -64
+
+-- This could be fixed with some additional work
+#check_simp (-64 : ISize).toInt64 !~>
+
+#check_simp (-127 : Int8).toInt16 ~> -127
+#check_simp (-128 : Int8).toInt16 !~>
+
+-- All of these could probably made to reduce using an additional simproc
+#check_simp (300 : UInt8) !~>
+#check_simp (300 : Int8) !~>
+#check_simp (-32767 : Int16).toInt8 ~> -32767
+#check_simp (-32768 : Int16).toInt8 ~> -32768
+#check_simp (-32769 : Int16).toInt8 ~> -32769
+
+#check_simp (-32767 : Int16).toInt32 ~> -32767
+#check_simp (-32768 : Int16).toInt32 !~>
+
+#check_simp (-2147483647 : Int32).toInt64 ~> -2147483647
+#check_simp (-2147483648 : Int32).toInt64 !~>
+
+-- see also simprocSInt.lean
diff --git a/tests/lean/run/simprocSInt.lean b/tests/lean/run/simprocSInt.lean
index 666a057769..6b0df5f5f5 100644
--- a/tests/lean/run/simprocSInt.lean
+++ b/tests/lean/run/simprocSInt.lean
@@ -202,3 +202,5 @@ section
 #check_simp ISize.toInt (-2147483648) ~> -2147483648
 
 end
+
+-- see also simpSInt.lean