style: proof style improvements in RegexSpec.lean

Items

Low-priority style items flagged by AI code review on PR #9.

1. Unused dr binding in regex_match_sound

regex_match_sound destructs the regex_match_correct result with obtain ⟨ast, _, h_parse, _, h_match⟩ — the _ discarding dr is fine. However, a comment noting why dr is intentionally discarded (we only need the AST-level match) would help readers understand the relationship.

2. Fragile DecidableEq instance comparison

Some proof branches use pattern matching on DecidableEq results that could be made more robust with cases, simp, and Subsingleton.elim to avoid depending on instance resolution order.

3. Specialized lemmas that could use general ones

Some lemmas in the Glushkov submodule have specialized proofs for things that general mathlib lemmas already cover. Replace with calls to general lemmas from Matcher.lean.

References

• Flagged by AI code review on PR #9

Lies RegexSpec.lean, beginnend mit regex_match_sound und den Glushkov-Beweisen, und vergleiche dann die spezialisierten Lemmata mit den allgemeinen Lemmata in Matcher.lean. Überprüfe die DecidableEq-Zweige und die verworfene dr-Bindung; abgeschlossen ist die Aufgabe, wenn die Kommentare, robusten Beweisfälle und die Wiederverwendung allgemeiner Lemmata angewendet sind, ohne das Beweisverhalten zu ändern.