Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Siddharth <[email protected]>
opencompl · May 28, 2024 · 0a686ba · 0a686ba
1 parent 57d84ea
commit 0a686ba
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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) :