feat(tactic/attribute): add `expand_exists` (#15498)
Adds an attribute `expand_exists`, which takes a proof that something exists with some property, and outputs a value using `classical.some`, and a proof that it has that property using `classical.some_spec`.
Closes #11682
