diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index f19d1d44ea..89d30f4c04 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -46,6 +46,16 @@ private def mkOr (lhs rhs : Expr) (wExpr : Expr) : Expr :=
   let inst := mkApp2 (mkConst ``instHOrOfOrOp [0]) ty (mkApp (mkConst ``BitVec.instOrOp) wExpr)
   mkApp6 (mkConst ``HOr.hOr [0, 0, 0]) ty ty ty inst lhs rhs
 
+private def mkAnd (lhs rhs : Expr) (wExpr : Expr) : Expr :=
+  let ty := mkApp (mkConst ``BitVec) wExpr
+  let inst := mkApp2 (mkConst ``instHAndOfAndOp [0]) ty (mkApp (mkConst ``BitVec.instAndOp) wExpr)
+  mkApp6 (mkConst ``HAnd.hAnd [0, 0, 0]) ty ty ty inst lhs rhs
+
+private def mkXor (lhs rhs : Expr) (wExpr : Expr) : Expr :=
+  let ty := mkApp (mkConst ``BitVec) wExpr
+  let inst := mkApp2 (mkConst ``instHXorOfXorOp [0]) ty (mkApp (mkConst ``BitVec.instXorOp) wExpr)
+  mkApp6 (mkConst ``HXor.hXor [0, 0, 0]) ty ty ty inst lhs rhs
+
 private def mkAdd (lhs rhs : Expr) (wExpr : Expr) : Expr :=
   let ty := mkApp (mkConst ``BitVec) wExpr
   let inst := mkApp2 (mkConst ``instHAdd [0]) ty (mkApp (mkConst ``BitVec.instAdd) wExpr)
@@ -230,23 +240,84 @@ builtin_simproc [bv_normalize] bv_add ((_ : BitVec _) + (_ : BitVec _)) := fun e
     else if let some step ← shiftLeftAdd then return step
     else return .continue
 
-builtin_simproc [bv_normalize] shiftRight_self ((_ : BitVec _) >>> (_ : BitVec _)) := fun e => do
+builtin_simproc [bv_normalize] shiftRight ((_ : BitVec _) >>> (_ : BitVec _)) := fun e => do
   let_expr HShiftRight.hShiftRight ty _ _ _ lhs rhs := e | return .continue
   let_expr BitVec wExpr := ty | return .continue
   let some w ← getNatValue? wExpr | return .continue
-  if lhs != rhs then return .continue
-  let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self) wExpr lhs
-  return .visit { expr := toExpr 0#w, proof? := some proof }
+  if lhs == rhs then
+    let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self) wExpr lhs
+    return .visit { expr := toExpr 0#w, proof? := some proof }
+  else
+    let_expr BitVec.ofNat nExpr kExpr := rhs | return .continue
+    let some n ← getNatValue? nExpr | return .continue
+    if w != n then return .continue
+    let some k ← getNatValue? kExpr | return .continue
+    let expr := BitVec.mkNatShiftRight lhs (toExpr (k % 2 ^ w)) wExpr
+    let proof := mkApp3 (mkConst ``BitVec.ushiftRight_ofNat_eq) wExpr lhs kExpr
+    return .visit { expr, proof? := some proof }
 
-builtin_simproc [bv_normalize] extract_full (BitVec.extractLsb' _ _ _) := fun e => do
+builtin_simproc [bv_normalize] extractLsb' (BitVec.extractLsb' _ _ _) := fun e => do
   let_expr BitVec.extractLsb' wExpr startExpr lenExpr targetExpr := e | return .continue
+  match_expr targetExpr with
+  | HAnd.hAnd _ _ _ _ lhs rhs =>
+    let lhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr lhs
+    let rhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr rhs
+    let expr := BitVec.mkAnd lhs' rhs' lenExpr
+    let proof := mkApp5 (mkConst ``BitVec.extractLsb'_and) wExpr lhs rhs startExpr lenExpr
+    return .visit { expr, proof? := some proof }
+  | HXor.hXor _ _ _ _ lhs rhs =>
+    let lhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr lhs
+    let rhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr rhs
+    let expr := BitVec.mkXor lhs' rhs' lenExpr
+    let proof := mkApp5 (mkConst ``BitVec.extractLsb'_xor) wExpr lhs rhs startExpr lenExpr
+    return .visit { expr, proof? := some proof }
+  | cond _ discr thenExpr elseExpr =>
+    let thenExpr' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr thenExpr
+    let elseExpr' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr elseExpr
+    let newTy := mkApp (mkConst ``BitVec) lenExpr
+    let expr := mkApp4 (mkConst ``cond [1]) newTy discr thenExpr' elseExpr'
+    let proof :=
+      mkApp6 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_if)
+        wExpr
+        discr
+        thenExpr
+        elseExpr
+        startExpr
+        lenExpr
+     return .visit { expr, proof? := some proof }
+  | _ =>
+    let some w ← getNatValue? wExpr | return .continue
+    let some start ← getNatValue? startExpr | return .continue
+    let some len ← getNatValue? lenExpr | return .continue
+    if start != 0 then return .continue
+    if len != w then return .continue
+    let proof := mkApp2 (mkConst ``BitVec.extractLsb'_eq_self) wExpr targetExpr
+    return .visit { expr := targetExpr, proof? := some proof }
+
+builtin_simproc [bv_normalize] shiftLeft ((_ : BitVec _) <<< (_ : BitVec _)) := fun e => do
+  let_expr HShiftLeft.hShiftLeft ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
   let some w ← getNatValue? wExpr | return .continue
-  let some start ← getNatValue? startExpr | return .continue
-  let some len ← getNatValue? lenExpr | return .continue
-  if start != 0 then return .continue
-  if len != w then return .continue
-  let proof := mkApp2 (mkConst ``BitVec.extractLsb'_eq_self) wExpr targetExpr
-  return .visit { expr := targetExpr, proof? := some proof }
+  let_expr BitVec.ofNat nExpr kExpr := rhs | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  if w != n then return .continue
+  let some k ← getNatValue? kExpr | return .continue
+  let expr := BitVec.mkNatShiftLeft lhs (toExpr (k % 2 ^ w)) wExpr
+  let proof := mkApp3 (mkConst ``BitVec.shiftLeft_ofNat_eq) wExpr lhs kExpr
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] sshiftRight' (BitVec.sshiftRight' _ _) := fun e => do
+  let_expr BitVec.sshiftRight' nExpr mExpr lhs rhs := e | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  let some m ← getNatValue? mExpr | return .continue
+  if n != m then return .continue
+  let_expr BitVec.ofNat wExpr kExpr := rhs | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  if n != w then return .continue
+  let some k ← getNatValue? kExpr | return .continue
+  let expr := mkApp3 (mkConst ``BitVec.sshiftRight) wExpr lhs (toExpr (k % 2 ^ w))
+  let proof := mkApp3 (mkConst ``BitVec.sshiftRight'_ofNat_eq_sshiftRight) wExpr lhs kExpr
+  return .visit { expr, proof? := some proof }
 
 def eqSelfProc : Simp.Simproc := fun e => do
   let_expr Eq ty lhs rhs := e | return .continue
@@ -341,6 +412,39 @@ builtin_simproc [bv_normalize] bool_beq ((_ : Bool) == (_ : Bool)) := fun e => d
     else if let some step ← selfRight then return step
     else return .continue
 
+builtin_simproc [bv_normalize] cast (BitVec.cast _ _) := fun e => do
+  let_expr BitVec.cast nExpr mExpr hExpr targetExpr := e | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  let some m ← getNatValue? mExpr | return .continue
+  if n != m then return .continue
+  let proof := mkApp3 (mkConst ``BitVec.cast_eq) nExpr hExpr targetExpr
+  return .visit { expr := targetExpr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bool_or_elim ((_ : Bool) || (_ : Bool)) := fun e => do
+  let_expr Bool.or lhs rhs := e | return .continue
+  let newLhs := mkApp (mkConst ``Bool.not) lhs
+  let newRhs := mkApp (mkConst ``Bool.not) rhs
+  let expr := mkApp (mkConst ``Bool.not) (mkApp2 (mkConst ``Bool.and) newLhs newRhs)
+  let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.or_elim) lhs rhs
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_or_elim ((_ : BitVec _) ||| (_ : BitVec _)) := fun e => do
+  let_expr HOr.hOr ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
+  let newLhs := BitVec.mkComplement lhs wExpr
+  let newRhs := BitVec.mkComplement rhs wExpr
+  let expr := BitVec.mkComplement (BitVec.mkAnd newLhs newRhs wExpr) wExpr
+  let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.or_elim) wExpr lhs rhs
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_sub_elim ((_ : BitVec _) - (_ : BitVec _)) := fun e => do
+  let_expr HSub.hSub ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
+  let newRhs := BitVec.mkNeg rhs wExpr
+  let expr := BitVec.mkAdd lhs newRhs wExpr
+  let proof := mkApp3 (mkConst ``BitVec.sub_eq_add_neg) wExpr lhs rhs
+  return .visit { expr, proof? := some proof }
+
 end SimpleUnifiers
 
 builtin_simproc ↓ [bv_normalize] reduceCond (cond _ _ _) := fun e => do
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index b89880a560..5b48381671 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -24,8 +24,6 @@ namespace Normalize
 
 section Reduce
 
-attribute [bv_normalize] BitVec.sub_eq_add_neg
-
 @[bv_normalize]
 theorem BitVec.le_ult (x y : BitVec w) : (x ≤ y) ↔ ((!y.ult x) = true) := by
   have : x ≤ y ↔ (x.ule y = true) := by
@@ -164,7 +162,6 @@ attribute [bv_normalize] BitVec.not_not
 attribute [bv_normalize] decide_true
 attribute [bv_normalize] decide_false
 attribute [bv_normalize] decide_not
-attribute [bv_normalize] BitVec.cast_eq
 
 end Constant
 
@@ -259,11 +256,6 @@ theorem BitVec.add_const_right' {a : BitVec w} :
 attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
-
-attribute [bv_normalize] BitVec.shiftLeft_ofNat_eq
-attribute [bv_normalize] BitVec.ushiftRight_ofNat_eq
-attribute [bv_normalize] BitVec.sshiftRight'_ofNat_eq_sshiftRight
-
 @[bv_normalize]
 theorem BitVec.neg_mul (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w := by
   rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.neg_mul]
@@ -370,10 +362,6 @@ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat)
   have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bitvec_to_nat, hk]
   rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)]
 
-attribute [bv_normalize] BitVec.extractLsb'_and
-attribute [bv_normalize] BitVec.extractLsb'_xor
-
-@[bv_normalize]
 theorem BitVec.extractLsb'_if {x y : BitVec w} (s l : Nat) :
     BitVec.extractLsb' s l (bif c then x else y) = bif c then (BitVec.extractLsb' s l x) else (BitVec.extractLsb' s l y) := by
   cases c <;> simp
diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index b3d307403b..78ac61c0c1 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -80,10 +80,8 @@ theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   simp only [(· < ·)]
   simp
 
-@[bv_normalize]
 theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
 
-@[bv_normalize]
 theorem BitVec.or_elim (x y : BitVec w) : x ||| y = ~~~(~~~x &&& ~~~y) := by
   ext
   simp