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

`fintype_of_option_equiv` was extracted from @huynhtrankhanh's #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)

Author: stuart-presnell

src/data/fintype/basic.lean

@@ -841,6 +841,14 @@ lemma univ_option (α : Type*) [fintype α] : (univ : finset (option α)) = inse
   fintype.card (option α) = fintype.card α + 1 :=
 (finset.card_cons _).trans $ congr_arg2 _ (card_map _) rfl
 
+/-- If `option α` is a `fintype` then so is `α` -/
+def fintype_of_option {α : Type*} [fintype (option α)] : fintype α :=
+⟨finset.erase_none (fintype.elems (option α)), λ x, mem_erase_none.mpr (fintype.complete (some x))⟩
+
+/-- A type is a `fintype` if its successor (using `option`) is a `fintype`. -/
+def fintype_of_option_equiv [fintype α] (f : option α ≃ β) : fintype β :=
+by { haveI := fintype.of_equiv (option α) f, exact fintype_of_option }
+
 instance {α : Type*} (β : α → Type*)
   [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
 ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩