feat: add BitVec.signExtend_extractLsb_setWidth theorem

src/Init/Data/BitVec/Lemmas.lean

@@ -2297,7 +2297,6 @@ theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
     <;> by_cases w ≤ i
     <;> simp [*]
 
-
 @[grind =]
 theorem sshiftRight'_ofNat_eq_sshiftRight {x : BitVec w} {k : Nat} : x.sshiftRight' (BitVec.ofNat w k) = x.sshiftRight (k % 2^w) := rfl
 
@@ -2572,6 +2571,15 @@ theorem msb_signExtend {x : BitVec w} :
   · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
   · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
 
+theorem sshiftRight_eq_setWidth_extractLsb_signExtend {w : Nat} {x : BitVec w} (n : Nat) :
+    x.sshiftRight n = ((x.signExtend (w + n)).extractLsb (w - 1 + n) n).setWidth w := by
+  ext i hi
+  simp only [getElem_sshiftRight, getElem_setWidth, getLsbD_extract,
+    Nat.add_sub_cancel, show i ≤ w - 1 by omega, decide_true, getLsbD_signExtend,
+    Bool.true_and]
+  by_cases hni : (n + i) < w
+  <;> (simp [hni]; omega)
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   x.signExtend v = x.setWidth v := by