diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index b26e34570d..2faf765a0e 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -174,8 +174,7 @@ 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]
+    x.getLsbD i = x[i] := rfl
 
 end getElem
 
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 36d41c46cc..4d5eb4081b 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -68,6 +68,9 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
   rfl
 
+@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
+  Nat.eq_zero_of_le_zero <| Nat.le_of_lt_succ a.isLt
+
 theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
     (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
   by_cases c <;> simp [*]
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index e8f0640f2b..8a41147175 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -206,5 +206,17 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
 
+@[bv_normalize]
+theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
+    BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
+  ext j
+  simp
+
+@[bv_normalize]
+theorem BitVec.ofBool_getElem (a : BitVec w) (i : Nat) (h : i < w) :
+    BitVec.ofBool a[i] = a.extractLsb' i 1 := by
+  rw [← BitVec.getLsbD_eq_getElem]
+  apply ofBool_getLsbD
+
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_extract.lean b/tests/lean/run/bv_extract.lean
index 57b8af64a4..7d81eeed7d 100644
--- a/tests/lean/run/bv_extract.lean
+++ b/tests/lean/run/bv_extract.lean
@@ -13,3 +13,15 @@ theorem bv_extract_3 (h : x = 1#64) : extractLsb 63 32 x = 0#32 := by
 
 theorem bv_extract_4 (h : x = 1#64) : extractLsb 31 0 x = 1#32 := by
   bv_decide
+
+theorem bv_ofBool_1 (h : x = 1#64) : ofBool (x.getLsbD 0) = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_2 (h : x = 1#64) : ofBool (x.getLsbD 1) = 0#1 := by
+  bv_decide
+
+theorem bv_ofBool_3 (h : x = 1#64) : ofBool x[0] = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_4 (h : x = 1#64) : ofBool x[1] = 0#1 := by
+  bv_decide