diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 591a253c0438..937e870cc6a1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/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