diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 21af9ba62479..bf3ba087b688 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -232,13 +232,13 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
-@[simp] theorem ofBool_and : ofBool a &&& ofBool b = ofBool (a && b) := by
+@[simp] theorem and_ofBool : ofBool a &&& ofBool b = ofBool (a && b) := by
   cases a <;> cases b <;> rfl
 
-@[simp] theorem ofBool_or : ofBool a ||| ofBool b = ofBool (a || b) := by
+@[simp] theorem or_ofBool : ofBool a ||| ofBool b = ofBool (a || b) := by
   cases a <;> cases b <;> rfl
 
-@[simp] theorem ofBool_xor : ofBool a ^^^ ofBool b = ofBool (a ^^ b) := by
+@[simp] theorem xor_ofBool : ofBool a ^^^ ofBool b = ofBool (a ^^ b) := by
   cases a <;> cases b <;> rfl
 
 @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl