[Merged by Bors] - chore: make #where command commonly available again

[kmill]

---

[fpvandoorn]

bors d+

Maybe other Battery-commands should be checked as well?

[mathlib-bors]

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[github-actions]

PR summary 2ddff3d4a6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Common	233	234	+1 (+0.43%)

Import changes for all files

Files	Import difference
There are 4016 files with changed transitive imports: this is too many to display!

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[kmill]

bors r+

(I agree with the idea to make sure other batteries commands are included, but I'll leave that for someone else! :-))

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style