case _ left =>
  left
  obtain s1 := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g hd
  exact Set.mem_of_subset_of_mem s1 left
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
no goals