case cons child₁ subpath₁ hi =>
  cases subpath₁
  case nil => simp [prefix?, Option.isSome]
  case cons child₂ subpath₂ =>
    specialize hi isCons_of_cons
    have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
    simp [prefix?, hi, Option.isSome_iff_exists]
    exists .cons child₁ subpath
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
no goals