diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 647ceebb25c9..7f66fefed36b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -494,8 +494,8 @@ theorem or_assoc (a b c : BitVec w) :
 
 theorem and_assoc (a b c : BitVec w) :
     a &&& b &&& c = a &&& (b &&& c) := by
-  ext i; simp [Bool.and_assoc]
-
+  ext i
+  simp [Bool.and_assoc]
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :