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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
have s1 : (dft_aux g stack []).toFinset.toSet = reachable_from_list g (dft_aux g stack []) :=
by
  apply list_direct_succ_set_closed_reachable_from_list g (dft_aux g stack [])
  exact list_direct_succ_set_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 (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
simp only [s1]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
s1 : ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ reachable_from_list g (dft_aux 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 (dft_aux g stack [])
⊢ reachable_from_list g stack ⊆ reachable_from_list g (dft_aux g stack [])
Tactic:
apply reachable_from_list_mono g stack (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 (dft_aux g stack [])
⊢ stack ⊆ dft_aux 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 (dft_aux g stack [])
⊢ stack ⊆ dft_aux g stack []
Tactic:
exact stack_subset_dft_aux g stack []
State after:
no goals

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ ↑(dft_aux g stack []).toFinset = reachable_from_list g (dft_aux g stack [])
Tactic:
apply list_direct_succ_set_closed_reachable_from_list g (dft_aux g stack [])
State after:
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

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:
exact list_direct_succ_set_closed_dft_aux g stack
State after:
no goals