no goals
α : Type u_1
β : Type ?u.457585
γ : Type ?u.457588
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ (toFinset (a :: l)).val = (insert a (toFinset l)).val
by_cases h : a ∈ l <;> simp [Finset.insert_val', Multiset.dedup_cons, h]