diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 08810a843f94..917b70fdff53 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1147,7 +1147,10 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
     x.signExtend v = x.zeroExtend v := by
   ext i
   by_cases hv : i < v
-  · simp [signExtend, toInt_eq_msb_cond, hmsb]
+  · simp only [signExtend, getLsbD, getLsbD_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
+      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
+    rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
+    simp [BitVec.testBit_toNat]
   · simp only [getLsbD_zeroExtend, hv, decide_False, Bool.false_and]
     apply getLsbD_ge
     omega