diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 9bafc89460ec..e3dd1e87245b 100644
--- 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