fintype.of_finset alternative

Stream: Is there code for X?

[Adam Topaz]

Do we have a lemma providing a fintype instance on a type X given a finset T : finset X such that every element of X is a member of T? Note that docs#fintype.of_finset doesn't apply directly.

[Hanting Zhang]

I think that is exactly the definition of docs#fintype. Maybe \<T, hT\> would work directly.

[Adam Topaz]

:face_palm:

[Adam Topaz]

I don't understand finite things in lean