mathlib3

feat(tactic/expand_exists): create in namespace & docstring

#15732

Open