[Merged by Bors] - feat(tactic/attribute): add expand_exists

[0x182d4454fb211940]

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

---

[alexjbest]

This looks really good, thanks! I left some mostly superficial comments
Adding a test file would also be good, demonstrating the usage too.
Also adding something to the PR description is nice, as that becomes the final commit message that people will see when they git blame your code.

It would also be good, to (maybe in a separate PR) identify examples of this pattern that can be replaced by your attribute, grepping for def.*:=.*some already reveals many!

[robertylewis]

This is nifty! A very clean implementation, a lot easier to follow than one based on choose. Two comments:

• Do you think you could add the user command version? It's probably only occasionally useful, but it should just involve factoring a few lines out of expand_exists_attr.
• In the test file, dependant -> dependent. (I just now learned BrE uses "dependant" for the noun form, but this is an adjective.)

[alexjbest]

I'm not sure I agree with needing a user command version, attribute [expand_exists blah foo] my_existential can already be used anywhere, and it just seems adding extra random syntaxes with no clear benefit makes more work porting to lean 4 at this point.
Do you have a use case in mind @robertylewis ?

[robertylewis]

I'm not sure I agree with needing a user command version, attribute [expand_exists blah foo] my_existential can already be used anywhere, and it just seems adding extra random syntaxes with no clear benefit makes more work porting to lean 4 at this point. Do you have a use case in mind @robertylewis ?

On the one hand, I think it's very little overhead (even in Lean 3, especially in Lean 4). On the other hand I don't think it's important, and you're right that the attribute version has the same effect with slightly clunkier syntax. So let's not worry about it for now.

[robertylewis]

Could you import this file in src/tactic/default.lean so it's available with import tactic?

[robertylewis]

This looks great, thanks again! If you're interested, I second Alex's suggestion for a follow-up PR adding some uses of the attribute to mathlib.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests