diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3f57854a6d..7f9c2ac71f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3328,6 +3328,11 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
       apply Nat.pow_dvd_pow 2 (by omega)
     simp [Nat.mul_mod, hpow]
 
+theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) :
+    (twoPow w i) * x = x <<< i := by
+  rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft]
+
+
 theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
   apply eq_of_toNat_eq
   simp
@@ -3337,6 +3342,12 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   ext i
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
+/-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+  apply BitVec.eq_of_toNat_eq
+  simp only [toNat_mul, toNat_twoPow]
+  rw [← Nat.mul_mod, Nat.pow_add]
+
 /--
 The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
 when `k` is less than the bitwidth `w`.