chore: use have, rw

leanprover · Sep 12, 2024 · 3d79832 · 3d79832
1 parent 7f4fad2
commit 3d79832
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
@@ -2022,7 +2022,7 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
   rw [BitVec.le_def] at h
   by_cases h' : x.toNat = y.toNat
   · rw [h', Nat.sub_self, Nat.sub_add_cancel (by omega), Nat.mod_self]
-  · rw [show 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) by omega,
-      Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
+  · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
+    rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
 
 end BitVec