From fcbdbed3ecf77b13a17241ef66b981d272237ddc Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 9 Dec 2024 09:39:57 -0800 Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 68cec5d2b7f1..3c0af631b4e4 100644 --- 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