From a09aa3c91f4c6555093549075c42f88e04d5b3f0 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <github@grosser.es>
Date: Thu, 5 Dec 2024 11:33:06 +0000
Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean

---
 src/Init/Data/BitVec/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 9f24e2ff5ab8..3abd443efb9f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1771,7 +1771,7 @@ theorem toNat_append_lt {m n : Nat} (x : BitVec m) (y : BitVec n) :
     <;> omega
   · omega
 
-@[simp] theorem toFin_append (x : BitVec m) (y : BitVec n) :
+@[simp] theorem toFin_append {x : BitVec m} {y : BitVec n} :
     (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) (toNat_append_lt x y) := by
   ext
   simp