Formalizing Regex Derivative in Lean

Brzozowski's derivative is truly a gem in the literature and surprised me with its beauty when I first learned about it towards the end of 2023, thanks to th...