by_cases path₁.prefix?.isSome
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
⊢ path₁ ≂ path₂
case inl
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂

case inr
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂