Exists.choose for unique existence?

Stream: Is there code for X?

[Uni Marx]

Is there some analogue of Exists.choose for unique existence? The normal one works just fine, of course, but it seems "morally" wrong and maybe there is some API i am missing

[Kevin Buzzard]

Welcome to type theory, uniqueness doesn't help here.

[Aaron Liu]

the problem is if it reduces definitionally then defeq becomes undecidable

[Eric Wieser]

Can you give some context? Often the answer if you're having moral qualms is "don't use choose at all", either via a suitable recursor, or by changing your datatype

[Aaron Liu]

and if it doesn't reduce definitionally then you might as well use the stronger choice

[Terence Tao]

I wrote some API for this at https://github.com/teorth/analysis/blob/main/analysis/Analysis/Tools/ExistsUnique.lean

[Uni Marx]

I'm aware it doesn't help much either way, yeah. for context, I want to prove that simple FD representations of abelian groups are 1-dimensional, for which I was using the lemma

theorem existsUnique_smul_id_eq_of_simple [IsAlgClosed k] {V : FDRep k G} [Simple V] (f : V ⟶ V) :
    ∃! a : k, a • 𝟙 V = f

...but that a is just the trace, of course, and I should just refactor it to be that

[Kevin Buzzard]

Are you sure? Isn't this Schur's lemma?

[Uni Marx]

it is! it's just worded in a somewhat awkward way in its existing shape (see finrank_hom_simple_simple (how do I link these by the way? I used to know but its been a few years) and it seems convenient

[Kevin Buzzard]

So the nxn scalar matrix a has trace na not a. You link with docs#finrank_hom_simple_simple

[Uni Marx]

thank you! the trace was wrong of course, but it turns out it was unnecessary either way. see #29622