Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Siddharth <siddu.druid@gmail.com>

src/Init/Data/BitVec/Lemmas.lean

@@ -1532,8 +1532,8 @@ theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
 theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
 
-theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} :
-  (x.signExtend (w + v)).toNat = x.toNat + (2 ^ (w + v)  - 2^w) * (if x.msb then 1 else 0) := by
+theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} (hv : v >= w):
+  (x.signExtend v).toNat = x.toNat + (2^v - 2^w) * (if x.msb then 1 else 0) := by
   apply Nat.eq_of_testBit_eq
   intro i
   rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one,