diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f6d35254e999..590149a7b02e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1273,7 +1273,7 @@ theorem toInt_ushiftRight_pos_eq_toNat_shiftRight (x : BitVec w) (n : Nat) (hn :
     omega
 
 @[simp]
-theorem toFin_uShiftRight (x : BitVec w) (n : Nat) :
+theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
     (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n)) := by
     apply Fin.eq_of_val_eq
     by_cases hn : n < w