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..8da008ecdfca 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 =>
+    rw [replicate_zero_eq]
+    simp
+  case succ n ih =>
+    rw [replicate_succ_eq]
+    simp only [getLsb_cast, getLsb_append]
+    by_cases hi : i < w * n
+    · simp [hi, ih]
+      intros h
+      rw [Nat.mul_succ]
+      omega
+    · simp [hi, ih]
+      by_cases hi' : i < w * (n + 1)
+      · simp [hi']
+        congr
+        rw [Nat.sub_eq_of_eq_add]
+        have hi : w = (i / n) := sorry
+        -- TODO: rewrite, and then use
+        -- rw [Nat.div_add_mod]
+        sorry
+      · simp [hi']
+        apply getLsb_ge
+        apply Nat.le_sub_of_add_le
+        simp [Nat.mul_succ] at hi'
+        rw [Nat.add_comm]
+        assumption
 end BitVec