case mpr =>
  intro h
  by_cases path₁.prefix?.isSome
  case inr hp =>
    have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
    rw [h] at hp
    have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
    simp [hc₁, hc₂, Sibling.nil]
  case inl hp =>
    have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
    rw [h] at hp
    have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
    simp_all
    exact Sibling.cons hp₁ hp₂
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
no goals