mathlib

80b7f975 - feat(tactic/localized): fail if unused locale is open (#2718)

feat(tactic/localized): fail if unused locale is open (#2718) This is more in line with the behavior of `open`. Closes #2702 Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>