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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g (xs ++ ys) = reachable_from_list g xs ∪ reachable_from_list g ys
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g (xs ++ ys) ⊆ reachable_from_list g xs ∪ reachable_from_list g ys

case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g xs ∪ reachable_from_list g ys ⊆ reachable_from_list g (xs ++ ys)

State before:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g (xs ++ ys) ⊆ reachable_from_list g xs ∪ reachable_from_list g ys
Tactic:
apply reachable_from_list_of_append_left
State after:
no goals

State before:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g xs ∪ reachable_from_list g ys ⊆ reachable_from_list g (xs ++ ys)
Tactic:
apply reachable_from_list_of_append_right
State after:
no goals