From fe481dc387d14b4a45f1df0028dde3ed8d6257dd Mon Sep 17 00:00:00 2001
From: Harun Khan <harun19@stanford.edu>
Date: Sat, 7 Dec 2024 22:41:59 -0800
Subject: [PATCH] toInt_shiftLeft

---
 src/Init/Data/BitVec/Lemmas.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 590bfcb7a7ad..c92fc97cc5aa 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1124,6 +1124,11 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
   BitVec.toNat_ofNat _ _
 
+@[simp] theorem toInt_shiftLeft {x : BitVec w} :
+    BitVec.toInt (x <<< n) = Int.bmod (x.toNat <<< n) (2^w) := by
+    rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
+    simp
+
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl