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

Co-authored-by: Tobias Grosser <github@grosser.es>

src/Init/Data/BitVec/Lemmas.lean

@@ -1253,7 +1253,7 @@ theorem ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) :
 Unsigned shift right by at least one bit makes the value of the bitvector less than or equal to `2^(w-1)`,
 makes the interpretation of the bitvector `Int` and `Nat` agree.
 -/
-theorem toInt_ushiftRight_pos_eq_toNat_shiftRight (x : BitVec w) (n : Nat) (hn : 0 < n) :
+theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
   simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]