mathlib

f5d4fa19 - feat(data/fintype/basic): add `fintype_of_{equiv,option}` (#13086)

feat(data/fintype/basic): add `fintype_of_{equiv,option}` (#13086) `fintype_of_option_equiv` was extracted from @huynhtrankhanh's https://github.com/leanprover-community/mathlib/pull/11162, moved here to a separate PR. The split into `fintype_of_option` and `fintype_of_equiv` is based on a comment on that PR by @jcommelin. Co-authored-by: Huỳnh Trần Khanh [qcdz9r6wpcbh59@gmail.com](mailto:qcdz9r6wpcbh59@gmail.com)