mathlib

9c03e9dc - feat(data/fintype): computable trunc bijection from fin (#10141)

feat(data/fintype): computable trunc bijection from fin (#10141) When a type `X` lacks decidable equality, there is still computably a bijection `fin (card X) -> X` using `trunc`. Also, move `fintype.equiv_fin_of_forall_mem_list` to `list.nodup.nth_le_equiv_of_forall_mem_list`.