Commit 2020-06-26 06:18 c3923e39

feat(data/fintype): trunc_sigma_of_exists (#3166) When working over a fintype, you can lift existential statements to trunc statements. This PR adds:

def trunc_of_nonempty_fintype {α} (h : nonempty α) [fintype α] : trunc α
def trunc_sigma_of_exists {α} [fintype α] {P : α → Prop} [decidable_pred P] (h : ∃ a, P a) : trunc (Σ' a, P a)