diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1881887062f2..dee8a74610be 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -781,6 +781,32 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+/-!
+  We extract a BitVec x' with length `len` from BitVec x, starting from the element at position `start`
+  let x                       = 8 7 6 5 4 3 2 1 0
+  let x' = x.extractLsb' 3 4  =     6 5 4 3
+  with `start = 3` and `len = 4`
+  we have `x'.getMsbD i = x[start + (len - 1 - i)] = x.getLsbD (start + (len - 1 - i))`
+  and rewrite `x.getLsbD (start + (len - 1 - i))` as `getMsbD`, which requires checking
+  `start + (len - 1 - i) < w` and yields `x.getMsbD (w - 1 - (start + (len - 1 - i)))`
+-/
+@[simp] theorem getMsbD_extractLsb' {start len : Nat} {x : BitVec w} {i : Nat} :
+    (extractLsb' start len x).getMsbD i =
+      (decide (i < len) &&
+      (decide (start + (len - 1 - i) < w) &&
+      x.getMsbD (w - 1 - (start + (len - 1 - i))))) := by
+  rcases len with rfl | len
+  · simp
+  · rw [getMsbD_eq_getLsbD, getLsbD_extractLsb', getLsbD_eq_getMsbD]
+    simp [show (len - i < len + 1) by omega]
+
+@[simp] theorem msb_extractLsb' {start len : Nat} {x : BitVec w} :
+    (extractLsb' start len x).msb
+    = (decide (0 < len) && x.getLsbD (start + len - 1)) := by
+  cases len
+  · simp [BitVec.extractLsb', BitVec.msb]
+  · simp [BitVec.msb, BitVec.getMsbD_eq_getLsbD, BitVec.getLsbD_extractLsb', ← Nat.add_assoc]
+
 @[simp] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
   simp [getElem_eq_testBit_toNat, getLsbD, h]
@@ -789,6 +815,32 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
   simp [getLsbD, Nat.lt_succ]
 
+@[boolToPropSimps] theorem and_eq_decide (a b : Bool) : (a && b) = decide (a = true ∧ b = true) := by simp [Bool.decide_and]
+
+attribute [boolToPropSimps] decide_eq_true_iff
+
+@[simp] theorem getLsbD_extractLsb (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsbD (extractLsb hi lo x) i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
+  rw [extractLsb, getLsbD_extractLsb']
+
+@[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
+    (extractLsb hi lo x).getMsbD i =
+      (decide (i < hi - lo + 1) &&
+      (decide ((max hi lo) - i < w) &&
+      x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
+  rw [getMsbD_eq_getLsbD, getLsbD_extractLsb, getLsbD_eq_getMsbD]
+  simp only [and_congr_right_iff, Nat.add_one_sub_one, boolToPropSimps, show hi - lo - i < hi - lo + 1 by omega]
+  intro
+  by_cases hmax : lo ≤ hi
+  · simp [Nat.max_eq_left hmax, show lo + (hi - lo - i) = hi - i by omega]
+  · simp [Nat.max_eq_right (show hi ≤ lo by omega), show lo + (hi - lo - i) = lo - i by omega]
+
+@[simp] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
+    (extractLsb hi lo x).msb
+    = (decide ((max hi lo) < w) &&
+      x.getMsbD (w - 1 - ((max hi lo)))) := by
+  simp [BitVec.msb, BitVec.getMsbD_extractLsb, Nat.le_sub_iff_add_le' (k := lo) (n := 0) (m := hi)]
+
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
   apply eq_of_toNat_eq