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

Co-authored-by: Tobias Grosser <[email protected]>

src/Init/Data/BitVec/Lemmas.lean

@@ -1242,7 +1242,7 @@ theorem toNat_ushiftRight_lt (x : BitVec w) (n : Nat) (hn : n ≤ w) :
 
 
 /-- Shifting right by `n`, which is larger than the bitwidth `w` produces `0. -/
-theorem ushiftRight_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) :
+theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
     x >>> n = 0#w := by
   simp [bv_toNat]
   have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn