toLex, ofLex match patterns

Stream: mathlib4

[Robert Maxton]

For some reason, toLex and ofLex are defined as equivalences, and an attempt is made to hang a match_pattern attribute on each, but this just creates arity-0 match patterns for Equiv rather then arity-1 match patterns for the type synonym. Is there a good reason for this somewhere, or would it be worth it to change toLex and ofLex to their obvious 'casting' functions (and hang match_pattern on those) and replace them with a Lex.equiv? I imagine there'd be a decent amount of refactoring involved, but...