RegularExpression.matches'_map

theorem RegularExpression.matches'_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P : RegularExpression α), (RegularExpression.map f P).matches' = (Language.map f) P.matches'

This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, and any regular expression `P` over `α`, applying the map operation to the regular expression `P` and then getting the matched language is the same as first getting the matched language of `P` and then applying the language map operation. In other words, the order in which we apply the regular expression map and the language map doesn't matter.

More concisely: For any types `α` and `β`, regular expression `P` over `α`, and function `f` from `α` to `β`, the language of `f` applied to the language of `P` over `α` is equal to the language of `P` over `α` applied to the language of `f`.