diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 103a6d4af8..107b0d6b54 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1757,4 +1757,17 @@ theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
     (x ++ 0#w) + (0#v ++ y) = x ++ y := by
   rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
 
+/-- Heuristically, `y <<< x` is much larger than `x`,
+and hence low bits of `y <<< x`. Thus, `x + (y <<< x) = x ||| (y <<< x).` -/
+theorem add_shifLeft_eq_or_shiftLeft {x y : BitVec w} :
+    x + (y <<< x) =  x ||| (y <<< x) := by
+  rw [add_eq_or_of_and_eq_zero]
+  ext i hi
+  simp only [shiftLeft_eq', getElem_and, getElem_shiftLeft, getElem_zero, and_eq_false_imp,
+    not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Nat.not_lt]
+  intros hxi hxval
+  have : 2^i ≤ x.toNat := two_pow_le_toNat_of_getElem_eq_true hi hxi
+  have : i < 2^i := by exact Nat.lt_two_pow_self
+  omega
+
 end BitVec
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d80fc88937..b8f06ce3ea 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -136,6 +136,12 @@ protected theorem toNat_lt_twoPow_of_le (h : m ≤ n) {x : BitVec m} :
 
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 
+theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
+    (hi : i < w) (hx : x[i] = true) : 2^i ≤ x.toNat := by
+  apply Nat.testBit_implies_ge
+  rw [← getElem_eq_testBit_toNat x i hi]
+  exact hx
+
 theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
     x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩ := by
   simp only [getMsb', getLsb']