feat(control/equiv_functor): fintype instance (#3783)

Requested at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/fintype.2Eequiv_congr/near/206773279



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/control/equiv_functor/instances.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Scott Morrison
 -/
-import data.finset.basic
+import data.fintype.basic
 import control.equiv_functor
 
 /-!
@@ -24,3 +24,6 @@ instance equiv_functor_perm : equiv_functor perm :=
 -- but we provide this computable alternative separately.
 instance equiv_functor_finset : equiv_functor finset :=
 { map := λ α β e s, s.map e.to_embedding, }
+
+instance equiv_functor_fintype : equiv_functor fintype :=
+{ map := λ α β e s, by exactI fintype.of_bijective e e.bijective, }