diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f1e8bcd67f96..9f35e7b4a381 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2672,6 +2672,21 @@ theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i
   simp [eq_comm]
   omega
 
+@[simp]
+theorem getMsbD_twoPow {i j w: Nat} :
+    (twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1)) := by
+  simp only [getMsbD_eq_getLsbD, getLsbD_twoPow]
+  by_cases h₀ : i < w <;> by_cases h₁ : j < w <;>
+  simp [h₀, h₁] <;> omega
+
+@[simp]
+theorem msb_twoPow {i w: Nat} :
+    (twoPow w i).msb = (decide (i < w) && decide (i = w - 1)) := by
+  simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.sub_zero, getLsbD_twoPow,
+    Bool.and_iff_right_iff_imp, Bool.and_eq_true, decide_eq_true_eq, and_imp]
+  intros
+  omega
+
 theorem and_twoPow (x : BitVec w) (i : Nat) :
     x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
   ext j