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

Co-authored-by: Siddharth <siddu.druid@gmail.com>
opencompl · Oct 27, 2024 · 32e2ec0 · 32e2ec0
1 parent 0170308
commit 32e2ec0
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
@@ -1536,8 +1536,8 @@ theorem toNat_signExtend_of_gt (x : BitVec w) {v : Nat} :
   (x.signExtend (w + v)).toNat = x.toNat + (2 ^ (w + v)  - 2^w) * (if x.msb then 1 else 0) := by
   apply Nat.eq_of_testBit_eq
   intro i
-  rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one]
-  rw [Nat.add_comm (x.toNat), Nat.mul_assoc, Nat.testBit_mul_pow_two_add _ (x.isLt)]
+  rw [testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one,
+      Nat.add_comm (x.toNat), Nat.mul_assoc, Nat.testBit_mul_pow_two_add _ (x.isLt)]
   by_cases h : i < w
   · simp [h, Nat.lt_add_right v h, testBit_toNat]
   · by_cases h2 : x.msb