diff --git a/Std/Data/BitVec/Basic.lean b/Std/Data/BitVec/Basic.lean
index 31f2ff9dfc..fdb1dc545f 100644
--- a/Std/Data/BitVec/Basic.lean
+++ b/Std/Data/BitVec/Basic.lean
@@ -2,7 +2,7 @@
 Copyright (c) 2022 by the authors listed in the file AUTHORS and their
 institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro
+Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer
 -/
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Fin.Basic
@@ -420,3 +420,16 @@ bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
 SMT-Lib name: `sign_extend`.
 -/
 def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
+
+/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
+@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
+@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
+@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
+@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
+@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
+@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
+@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
+@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
+@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
+@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
+@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl