diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 9566fe2ec8bc..0e335ad371ae 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -583,11 +583,9 @@ instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
 -- TODO: write this using multiplication
 /-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
 def replicate : (i : Nat) → BitVec w → BitVec (w*i)
-  | 0,   _ => 0
+  | 0,   _ => 0#0
   | n+1, x =>
-    have hEq : w + w*n = w*(n + 1) := by
-      rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
-    hEq ▸ (x ++ replicate n x)
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega)
 
 /-!
 ### Cons and Concat
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 936bdd68ac08..81ffb7121fbd 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1504,4 +1504,43 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
     simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
+@[simp]
+theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
+  simp [replicate]
+
+@[simp]
+theorem replicate_succ_eq {x : BitVec w} :
+    x.replicate (n + 1) =
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
+  simp [replicate]
+
+theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getLsb i =
+    ((decide (i < w * n)) && (x.getLsb (i % w))) := by
+  induction n generalizing x
+  case zero =>
+    simp
+  case succ n ih =>
+    simp only [replicate_succ_eq, getLsb_cast, getLsb_append]
+    by_cases hi : i < w * n
+    · simp only [hi, decide_True, ih, Bool.true_and, cond_true, Bool.iff_and_self,
+      decide_eq_true_eq]
+      intros _
+      rw [Nat.mul_succ]
+      omega
+    · simp only [hi, decide_False, ih, Bool.false_and, cond_false]
+      by_cases hi' : i < w * (n + 1)
+      · simp only [hi', decide_True, Bool.true_and]
+        congr
+        rw [Nat.sub_eq_of_eq_add]
+        have hi : i / w = n := by
+          apply Nat.div_eq_of_lt_le (m := i) (k := n)
+            (by simp at hi; rw[Nat.mul_comm]; assumption)
+            (by rw [Nat.mul_comm]; assumption)
+        rw [← hi, Nat.add_comm, Nat.div_add_mod]
+      · simp only [hi', decide_False, Bool.false_and]
+        apply getLsb_ge
+        apply Nat.le_sub_of_add_le
+        simp only [Nat.mul_succ, Nat.not_lt] at hi'
+        omega
 end BitVec