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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
have s1 : (dft_aux g stack []).toFinset.toSet ⊆ reachable_from_list g stack ∪ [].toFinset.toSet := dft_aux_is_subset_of_reachable_from_list_and_visited g stack []
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack ∪ ↑[].toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack ∪ ↑[].toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
simp only [List.toFinset_nil, Finset.coe_empty, Set.union_empty] at s1
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
have s2 : reachable_from_list g stack ⊆ (dft_aux g stack []).toFinset.toSet := reachable_from_list_closed_dft_aux g stack
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
s2 : reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset ⊆ reachable_from_list g stack
s2 : reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g stack
Tactic:
exact Set.eq_of_subset_of_subset s1 s2
State after:
no goals