Theorem: Collection.finset_toCollection_finite (Logic/Vorspiel/Collection.lean)

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
s : Finset β
⊢ Finite s.toCollection
Tactic:
simp [Finite, set]
State after:
no goals