simp only [Set.subset_def] at *
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ∀ x_1 ∈ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset,
    x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset,
    x_1 ∈ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset