feat: shiftLeft in terms of extractLsb'

This PR adds rewrites from Bitwuzla that normalizes left shifts
in terms of extracting bits and concatenating zeroes.
If the shift amount is larger than the bitwidth, then the resulting bitvector is zero.

```lean
theorem shiftLeft_eq_zero_of_le (x : BitVec w) (n : Nat) (hn : w ≤ n) : x <<< n = 0#w

theorem shiftLeft_eq_concat_of_lt (x : BitVec w) (n : Nat) (hn : n < w) :
    x <<< n = ((x.extractLsb' 0 (w-n)).append (BitVec.zero n)).cast (by omega)
```

src/Init/Data/BitVec/Lemmas.lean

@@ -1313,6 +1313,11 @@ theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i
     (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
   simp
 
+theorem shiftLeft_eq_zero (x : BitVec w) (n : Nat) (hn : w ≤ n) : x <<< n = 0#w := by
+  ext i hi
+  simp [hn, hi]
+  omega
+
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -1941,6 +1946,15 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
     (x <<< n).msb = x.getMsbD n := by
   simp [BitVec.msb]
 
+theorem shiftLeft_eq_concat_of_lt (x : BitVec w) (n : Nat) (hn : n < w) :
+    x <<< n = ((x.extractLsb' 0 (w-n)).append (BitVec.zero n)).cast (by omega) := by
+  ext i hi
+  simp [hi, hn, getLsbD_append]
+  by_cases hi' : i < n
+  · simp [hi']
+  · simp [hi']
+    omega
+
 /-! ### rev -/
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :