chore: replace omega with proper theorem

Co-authored-by: Alex Keizer <[email protected]>
leanprover · Jan 21, 2025 · 4481757 · 4481757
1 parent f794c9e
commit 4481757
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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]