## Stream: Is there code for X?

### Topic: recovering from an exists

#### Scott Morrison (Jun 19 2020 at 14:12):

Is it possible to construct

example {α : Type} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ a, P a) :
trunc (Σ' a, P a) :=


by looking through the elems of the fintype?

#### Reid Barton (Jun 19 2020 at 14:15):

I think so--basically use subsingleton-ness of trunc to eliminate the quotient in fintype \a to a list of elements

#### Reid Barton (Jun 19 2020 at 14:15):

then take the first element satisfying the predicate, which has to exist

#### Reid Barton (Jun 19 2020 at 14:16):

The form of your question seems slightly at odds with the stream it's posted in, though :upside_down:

#### Scott Morrison (Jun 19 2020 at 14:22):

Hm, okay. :-) I guess I have sometimes use "Is there code for X?" to also include "Does anyone want to proof / sketch for me X?"

#### Scott Morrison (Jun 19 2020 at 14:22):

Okay, I have a horrible proof now!

#### David Wärn (Jun 19 2020 at 16:31):

import data.fintype.basic
open finset

lemma trunc_of_nonempty_multiset {α} (s : multiset α) : (∃ x, x ∈ s) → trunc α :=
quotient.rec_on_subsingleton s $λ l h, match l, h with | [], _ := false.elim (by tauto) | (a :: _), _ := trunc.mk a end lemma trunc_of_nonempty_of_fintype {α} [fintype α] (h : nonempty α) : trunc α := trunc_of_nonempty_multiset univ.val (by simp) example {α : Type} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ a, P a) : trunc (Σ' a, P a) := trunc_of_nonempty_of_fintype$ exists.elim h \$ λ a ha, ⟨⟨a, ha⟩⟩


#### Scott Morrison (Jul 13 2020 at 00:59):

Just for the record this made it into mathlib as #3166, in data.fintype.basic.

#### Mario Carneiro (Jul 13 2020 at 01:01):

Shouldn't this be using subtype instead of Sigma'?

Yes!

#### Scott Morrison (Jul 13 2020 at 01:06):

I'll get to it eventually. :-)

Last updated: May 16 2021 at 05:21 UTC