diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 8da008ecdfca..892b4cbadc71 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1525,7 +1525,7 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
     simp only [getLsb_cast, getLsb_append]
     by_cases hi : i < w * n
     · simp [hi, ih]
-      intros h
+      intros _
       rw [Nat.mul_succ]
       omega
     · simp [hi, ih]
@@ -1533,10 +1533,13 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
       · 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
+        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]
+        rw [Nat.add_comm]
+        rw [Nat.div_add_mod]
       · simp [hi']
         apply getLsb_ge
         apply Nat.le_sub_of_add_le