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

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x : β
s : Finset β
⊢ x ∈ s.toCollection ↔ x ∈ s
Tactic:
simp [Finset.toCollection]
State after:
no goals