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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = list_direct_succ_set g xs
Tactic:
simp only [list_direct_succ_set]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp only [← mem_list_direct_succ_list_iff]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | y ∈ list_direct_succ_list g xs}

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑(list_direct_succ_list g xs).toFinset = {y | y ∈ list_direct_succ_list g xs}
Tactic:
simp
State after:
no goals