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

Co-authored-by: Tobias Grosser <github@grosser.es>
opencompl · Dec 9, 2024 · fcbdbed · fcbdbed
1 parent 01199ca
commit fcbdbed
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1126,9 +1126,8 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
 
 @[simp] theorem toInt_shiftLeft {x : BitVec w} :
     BitVec.toInt (x <<< n) = Int.bmod (x.toNat <<< n) (2^w) := by
-    rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
-    simp
-
+  rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
+  simp
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl