exact Set.subset_union_of_subset_right ih (reachable_from_list g [x])
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ (reachable_from_list g stack ∪ ↑visited.toFinset)
no goals