diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 7f66fefed36b..994273ba719c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -518,8 +518,8 @@ theorem and_assoc (a b c : BitVec w) :
 
 theorem xor_assoc (a b c : BitVec w) :
     a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := by
-  ext i; simp [Bool.xor_assoc]
-
+  ext i
+  simp [Bool.xor_assoc]
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl