obtain ⟨c, hc : sbtw _ c _, hcmin⟩ := S.toFinite.exists_minimal_wrt (dist b) _ ⟨c', hc'⟩
case intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b
case intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
c' : V
hc' : sbtw a c' b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
⊢ ∃ c, sbtw a c b ∧ SimpleEdges.Adj c b