diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 24d5e5c6de..699fa8b22d 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1046,6 +1046,11 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   apply eq_of_toNat_eq
   simp [extractLsb, show len - 1 + 1 = len by omega]
 
+/-- Extracting all the bits of a bitvector is an identity operation. -/
+@[simp] theorem extractLsb'_eq_self {x : BitVec w} : x.extractLsb' 0 w = x := by
+  apply eq_of_toNat_eq
+  simp [extractLsb']
+
 /-! ### allOnes -/
 
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by