From 0a686baaf95205e4ffc5308bba29003199ca792c Mon Sep 17 00:00:00 2001
From: Tobias Grosser <github@grosser.es>
Date: Tue, 28 May 2024 06:17:28 +0100
Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 src/Init/Data/BitVec/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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) :