[Merged by Bors] - feat(tactic/choose): choose can now decompose conjunctions

[cipher1024]

---

In goal of the form

h : ∀ x, ∃ y, P
⊢ ...

mk_constructive h produces this goal:

h : ∀ x, Σ' y, P
⊢ ...

This makes it easier to use elimination on h later even when the goal is not a Prop

[cipher1024]

This PR was spun off from #3638

[gebner]

We already have a choose tactic that does something very similar: https://leanprover-community.github.io/mathlib_docs/tactics.html#choose

[gebner]

Copyright boilerplate, and module docstring please!

[cipher1024]

We already have a choose tactic that does something very similar: https://leanprover-community.github.io/mathlib_docs/tactics.html#choose

I see yes, it's mostly redundant with that tactic. Maybe I should recycle this PR to make a change to choose. I think it should treat ∧ as existentials. Comments?

[fpvandoorn]

choose indeed already exists for this purpose.
Changing choose so that you can split conjunctions in the same way as existentials is very welcome (I've already missed that feature at least once).

[cipher1024]

This PR is now completely revamped and it is now an improvement of choose

[bryangingechen]

Can you update the PR title / comment?

[fpvandoorn]

Looks good. Some comments:

• please add one or more tests for this tactic.
• Ideally choose can parse something like ⟨⟨h1, h2⟩, h3⟩ as argument, in the same way as the (conjunctive part of) rcases. That could be a different PR, though.

[cipher1024]

Ideally choose can parse something like ⟨⟨h1, h2⟩, h3⟩ as argument, in the same way as the (conjunctive part of) rcases. That could be a different PR, though.

I thought about that too. As you say, that's probably a bigger change but it's worth considering. The one part that gives me pause though is that patterns a | b, a part of the rcases language, does not have a useful interpretation. That might not be enough not to consider doing it though.

[cipher1024]

I do have tests. For some reason, they don't show up here. I don't get it. I do git log on my computer and it's there.

[cipher1024]

I was looking at the wrong PR 🤦

[fpvandoorn]

I thought about that too. As you say, that's probably a bigger change but it's worth considering. The one part that gives me pause though is that patterns a | b, a part of the rcases language, does not have a useful interpretation. That might not be enough not to consider doing it though.

We can easily implement a different parser that only reads the conjunctive patterns of rcases.

For the moment, LGTM

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests