feat: provide an instance of Fintype (Fin2 n) (#10805)

This enables use of the `fin_cases` tactic on premises `i : Fin2 _`

Mathlib/Data/Fin/Fin2.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Std.Tactic.NoMatch
 import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Mathport.Rename
+import Mathlib.Data.Fintype.Basic
 
 #align_import data.fin.fin2 from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 
@@ -131,4 +132,11 @@ def ofNat' : ∀ {n} (m) [IsLT m n], Fin2 n
 instance : Inhabited (Fin2 1) :=
   ⟨fz⟩
 
+instance instFintype : ∀ n, Fintype (Fin2 n)
+  | 0   => ⟨∅, Fin2.elim0⟩
+  | n+1 =>
+    let ⟨elems, compl⟩ := instFintype n
+    { elems    := elems.map ⟨Fin2.fs, @fs.inj _⟩ |>.cons .fz (by simp)
+      complete := by rintro (_|i) <;> simp [compl] }
+
 end Fin2