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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g (dft_aux g stack []) ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
apply list_direct_succ_set_closed_dft_aux_aux
State after:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g [] ⊆ ↑stack.toFinset ∪ ↑[].toFinset

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

State before:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ {y | ∃ x ∈ [], ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑stack.toFinset ∪ ↑[].toFinset
Tactic:
simp
State after:
no goals