diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3d4a7d3445d3..d8a8caf3d769 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -559,6 +559,15 @@ theorem and_comm (x y : BitVec w) :
   rw [← testBit_toNat, getLsb, getLsb]
   simp
 
+@[simp] theorem getMsb_xor {x y : BitVec w} :
+    (x ^^^ y).getMsb i = (xor (x.getMsb i) (y.getMsb i)) := by
+  simp only [getMsb]
+  by_cases h : i < w <;> simp [h]
+
+@[simp] theorem msb_xor {x y : BitVec w} :
+    (x ^^^ y).msb = (xor x.msb y.msb) := by
+  simp [BitVec.msb]
+
 @[simp] theorem truncate_xor {x y : BitVec w} :
     (x ^^^ y).truncate k = x.truncate k ^^^ y.truncate k := by
   ext
@@ -651,6 +660,27 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
   cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
   all_goals { simp_all <;> omega }
 
+theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
+    (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h : (i < n) <;> simp [h]
+
+theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
+    (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h : (i < n) <;> simp [h]
+
+theorem shiftLeft_or_distrib (x y : BitVec w)  (n : Nat) :
+    (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h : (i < n) <;> simp [h]
+
 @[simp] theorem getMsb_shiftLeft (x : BitVec w) (i) :
     (x <<< i).getMsb k = x.getMsb (k + i) := by
   simp only [getMsb, getLsb_shiftLeft]
@@ -822,6 +852,36 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
         Nat.not_lt, decide_eq_true_eq]
       omega
 
+theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
+    (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h₁ : (w ≤ ↑i)
+  · simp [h₁]
+  · simp [h₁]
+    by_cases h₂ : n + ↑i < w <;> simp [h₂]
+
+theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
+    (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h₁ : (w ≤ ↑i)
+  · simp [h₁]
+  · simp [h₁]
+    by_cases h₂ : n + ↑i < w <;> simp [h₂]
+
+theorem sshiftRight_or_distrib (x y : BitVec w)  (n : Nat) :
+    (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n) := by
+  ext
+  simp
+  rename_i i
+  by_cases h₁ : (w ≤ ↑i)
+  · simp [h₁]
+  · simp [h₁]
+    by_cases h₂ : n + ↑i < w <;> simp [h₂]
+
 /-- The msb after arithmetic shifting right equals the original msb. -/
 theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} :
     (x.sshiftRight n).msb = x.msb := by