And here the formalized proof in less than 150 lines of code (in Agda) for Brzozowski Derivatives for regex matching (and additional regular languages theorems): https://github.com/desi-ivanov/agda-regexp-automata