mathlib
mathlib copied to clipboard
Probably `setup_tactic_parser` can be integrated to use `open_locale` instead