pandaman64/lean-regex

AI Summary: The task involves extending a formally verified regular expression engine in Lean 4 to support more efficient prefiltering. This requires modifying the `OptimizationInfo` structure to handle multiple starting characters, updating related functions (`firstChars`, `findStart`), and adapting the correctness proofs to account for the change. The goal is to improve performance by allowing the engine to skip positions that cannot possibly match based on the initial characters of the regex.