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)
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
