diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1b2a29f221..54d21c5db1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -4015,6 +4015,16 @@ theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
     (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
   simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
 
+theorem toInt_rotateLeft {x : BitVec w} {r : Nat} :
+  (x.rotateLeft r).toInt =
+    ((x <<< (r % w)).toNat ||| (x >>> (w - r % w)).toNat : Int).bmod (2 ^ w) := by
+  simp [rotateLeft_def, toInt_shiftLeft, toInt_ushiftRight, toInt_or]
+
+theorem toFin_rotateLeft {x : BitVec w} {r : Nat} :
+  (x.rotateLeft r).toFin =
+    Fin.ofNat' (2 ^ w) (x.toNat <<< (r % w)) ||| x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (w - r % w)) := by
+  simp [rotateLeft_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or]
+
 /-! ## Rotate Right -/
 
 /-- `rotateRight` is defined in terms of left and right shifts. -/
@@ -4161,6 +4171,14 @@ theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
     (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
   simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
 
+theorem toInt_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toInt = ((x >>> (r % w)).toNat ||| (x <<< (w - r % w)).toNat : Int).bmod (2 ^ w) := by
+  simp [rotateRight_def, toInt_shiftLeft, toInt_ushiftRight, toInt_or]
+
+theorem toFin_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (r % w)) ||| Fin.ofNat' (2 ^ w) (x.toNat <<< (w - r % w)) := by
+  simp [rotateRight_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by