diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e4d07c5cf9db..1c9d902f6375 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3796,7 +3796,7 @@ theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :
   by_cases h' : w = 0 <;> simp [h'] <;> omega
 
 @[simp]
-theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by omega) :
+theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := Nat.mul_one _) :
     (x.replicate 1) = x.cast h := by 
   simp [replicate, h]