If `Fintype α` then `Fintype (Finset α)`

Stream: Is there code for X?

[Jihoon Hyun]

instance {α : Type _} [Fintype α] : Fintype (Finset α) where
  elems := (@Finset.univ α).powerset
  complete x := by simp

I couldn't find such instance. Is there such an instance somewhere, or is this absent?

[Yaël Dillies]

Here's the instance in Lean 3: docs#finset.fintype

[Jihoon Hyun]

Then there should be one in mathlib4 also.. Thank you.

[Yaël Dillies]

docs4#Finset.fintype