diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 1eaa1d0476..b26e34570d 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -173,6 +173,10 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
 theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
+theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
+    x.getLsbD i = x[i] := by
+  simp [getLsbD, getElem_eq_testBit_toNat]
+
 end getElem
 
 section Int
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 8cc832f3ae..c04b19a94a 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -523,6 +523,15 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
   all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
+@[simp]
+theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) :
+    (truncate m x)[i] = x.getLsbD i := by
+  simp only [getElem_zeroExtend]
+
+theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+    (truncate m x)[i]? = if i < m then some (x.getLsbD i) else none :=
+  getElem?_zeroExtend m x i
+
 theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
   getLsbD_zeroExtend m x i