diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index a270c36cf2ca..992f7d44cd8d 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1248,10 +1248,10 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) :
   simp only [saddOverflow]
   rcases w with _|w
   · revert x y; decide
-  · have := le_toInt x; have := toInt_lt x
-    have := le_toInt y; have := toInt_lt y
-    have := toInd_add_toInt_lt_two_pow x y
-    have := neg_two_pow_le_toInd_add_toInt x y
+  · have := le_toInt (x := x); have := toInt_lt (x := x)
+    have := le_toInt (x := y); have := toInt_lt (x := y)
+    have := toInd_add_toInt_lt_two_pow (x := x) (y := y)
+    have := neg_two_pow_le_toInd_add_toInt (x := x) (y := y)
     have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
         (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by
       simp only [Int.bmod_def]
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 05f00d87c218..ac16f82acf14 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -542,7 +542,7 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
 theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
   simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w]
 
-theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by
+theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by
   simp only [BitVec.toInt]
   rcases w with _|w'
   · omega
@@ -550,7 +550,7 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
-theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
+theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by
   simp only [BitVec.toInt]
   rcases w with _|w'
   · omega
@@ -558,21 +558,21 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
-theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) :
+theorem toInd_add_toInt_lt_two_pow {x y : BitVec w} :
     x.toInt + y.toInt < 2 ^ w := by
   rcases w with _|w'
   · simp [BitVec.eq_nil x, BitVec.eq_nil y]
-  · have hx := toInt_lt x
-    have hy := toInt_lt y
+  · have hx := toInt_lt (x := x)
+    have hy := toInt_lt (x := y)
     rw [Nat.add_sub_cancel] at hx hy
     omega
 
-theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) :
+theorem neg_two_pow_le_toInd_add_toInt {x y : BitVec w} :
     - 2 ^ w ≤ x.toInt + y.toInt := by
   rcases w with _|w'
   · simp [BitVec.eq_nil x, BitVec.eq_nil y]
-  · have hx := le_toInt x
-    have hy := le_toInt y
+  · have hx := le_toInt (x := x)
+    have hy := le_toInt (x := y)
     rw [Nat.add_sub_cancel] at hx hy
     omega