Theorem: list_append_to_set_union (FOL/Parsing/DFT.lean)

State before:
α : Type
inst : DecidableEq α
xs ys : List α
⊢ ↑(xs ++ ys).toFinset = ↑xs.toFinset ∪ ↑ys.toFinset
Tactic:
ext a
State after:
case h
α : Type
inst : DecidableEq α
xs ys : List α
a : α
⊢ a ∈ ↑(xs ++ ys).toFinset ↔ a ∈ ↑xs.toFinset ∪ ↑ys.toFinset

State before:
case h
α : Type
inst : DecidableEq α
xs ys : List α
a : α
⊢ a ∈ ↑(xs ++ ys).toFinset ↔ a ∈ ↑xs.toFinset ∪ ↑ys.toFinset
Tactic:
simp
State after:
no goals