case a
α : Type u_1
β : Type ?u.474148
γ : Type ?u.474151
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
a✝ : α
⊢ a✝ ∈ toFinset (l ∪ l') ↔ a✝ ∈ toFinset l ∪ toFinset l'
α : Type u_1
β : Type ?u.474148
γ : Type ?u.474151
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
⊢ toFinset (l ∪ l') = toFinset l ∪ toFinset l'
ext
no goals
case a
α : Type u_1
β : Type ?u.474148
γ : Type ?u.474151
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
a✝ : α
⊢ a✝ ∈ toFinset (l ∪ l') ↔ a✝ ∈ toFinset l ∪ toFinset l'
simp