Intermediate (non-unique) choose def vs. exists theorem

Stream: mathlib4

[Weiyi Wang]

I am in the process of cleaning up my proof for Hahn embedding theorem to make it mathlib ready. In one of the intermediate result, I defined an object using Exists.choose, which morally reads weird because the satisfying object is not unique. The final theorem statement also takes the form of Exists, so in theory I could refactor this into an intermediate exists theorem (or something like a non-empty set), but everything will be more verbose (instead of saying the chosen element satisfies props, I'll need to say every such element satisfies props). What's mathlib's policy around this? Should I refactor it to avoid using choose for a def, or I don't need to bother?

[Ruben Van de Velde]

You don't need to bother, I think

[Kyle Miller]

I think it's usually better to have a def and theorem of a property than a theorem proving existence, assuming you have more than one theorem about the def.

This is dual to how it's usually better for theorems to take multiple parameters than to take conjunctions or existentials (that is, it's better to curry the parameters).

Just please be sure to document that the def is an arbitrary choice! It can be helpful to have an explanation about just how non-unique it is too, and why it's helpful to have theory about the arbitrary choice.

[Weiyi Wang]

Got it!