have ⟨P, (hP : P.Special a b d), hPmin⟩ :=
  this.exists_minimal_wrt List.pathLength S ⟨[a, b, d], abd_special habc hd hbd' hbd⟩
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
⊢ False
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∃ x y z, SimpleTriangle x y z
S✝¹ : Set (V × V × V) := {(x, y, z) | SimpleTriangle x y z}
this✝ : S✝¹.Nonempty
b d✝ a c : V
habc : SimpleTriangle a b c
hmin : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
h3 : Line a c ≠ {a, c}
hd✝ : d✝ ∈ Line a c
acd : sbtw a c d✝
S✝ : Set V := setOf (sbtw a c)
d : V
hd : sbtw a c d
hbd' : b ≠ d
hdmin : ∀ (d' : V), sbtw a c d' → dist c d ≤ dist c d'
hcd : SimpleEdges.Adj c d
hbd : ¬SimpleEdges.Adj b d
S : Set (List V) := setOf (List.Special a b d)
this : S.Finite
P : List V
hP : List.Special a b d P
hPmin : ∀ a' ∈ S, a'.pathLength ≤ P.pathLength → P.pathLength = a'.pathLength
⊢ False