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

Co-authored-by: Tobias Grosser <github@grosser.es>
opencompl · Nov 12, 2024 · d0ae41a · d0ae41a
1 parent d9bf86f
commit d0ae41a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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