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

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
x : β
l : List β
⊢ x ∈ l.toCollection ↔ x ∈ l
Tactic:
induction l <;> simp [List.toCollection, *]
State after:
no goals