Extending `exists`?

Stream: lean4

[François G. Dorais]

It's not unusual to have to use the exists tactic a few times in a row. It would be nice to extend the exists tactic to accept a comma separated list of terms instead of just one at a time.

Such an extension seems to fit the "low work and low maintenance" criteria. Should this be a feature request? Or would a pull request be welcome here? Or is there a reason why this is undesirable?

[Alex J. Best]

In mathlib 3 we use use for this, but I do not know if mathlib4 has implemented this already

[François G. Dorais]

Not yet: <https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathlib.20newbie.20issue.3A.20exists.20tactic/near/280067568>

I would contend this extension belongs in core. I think mathlib's use handles much more than that but it wouldn't fit the "low work and low maintenance" criteria.

[Kyle Miller]

The next best thing is refine', which is in core Lean 4.

example : ∃ n m, n = m + 1 := by
  refine' ⟨2, 1, _⟩
  rfl

[Leonardo de Moura]

Pushed the exists es:term,+ extension.

[Kyle Miller]

What is the difference between a placeholder _ and an "unnamed hole" ?_? I see I can do refine ⟨2, 1, ?_⟩ but not refine ⟨2, 1, _⟩. (Being able to do refine ⟨2, 1, ?foo⟩ to name a goal is a neat feature.)

[Leonardo de Moura]

The Lean 4 refine' is the Lean 3 refine. Note that refine' ⟨2, 1, _⟩ also works in Lean 4.
We changed refine in Lean 4, and it only accepts "named holes": ?<id> and ?_. Reasons:
1- It motivates users to have structured proofs. They can fill the named holes using case <id> => ...
2- Helps users catch mistakes. refine fails if some implicit hole could not be filled. I think @Reid Barton suggested this feature. May be mistaken.