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

State before:
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset = reachable_from_list g xs
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs

case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset

State before:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
Tactic:
apply base_of_reachable_from_list_is_subset_of_reachable_from_list
State after:
no goals

State before:
case a
α : Type
inst✝ : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
exact extracted_5 g xs h1
State after:
no goals