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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
Tactic:
simp only [Set.subset_def]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ∀ x ∈ ↑xs.toFinset, x ∈ reachable_from_list g xs

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ∀ x ∈ ↑xs.toFinset, x ∈ reachable_from_list g xs
Tactic:
intro x a1
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ ↑xs.toFinset
⊢ x ∈ reachable_from_list g xs

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ ↑xs.toFinset
⊢ x ∈ reachable_from_list g xs
Tactic:
simp at a1
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs
Tactic:
exact reachable_from_list.base x a1
State after:
no goals