obtain ⟨⟨a, b, c⟩, (h₁ : NotCollinear _ _ _), h₂⟩ := S.toFinite.exists_minimal_wrt f S this
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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
⊢ ∃ x y z, SimpleTriangle x y z
case intro.mk.mk.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, NotCollinear x y z
S : Set (V × V × V) := {(a, b, c) | NotCollinear a b c}
this : S.Nonempty
f : V × V × V → ℝ :=
  fun x =>
    match x with
    | (a, b, c) => dist a b + dist b c + dist c a
a b c : V
h₁ : NotCollinear a b c
h₂ : ∀ a' ∈ S, f a' ≤ f (a, b, c) → f (a, b, c) = f a'
⊢ ∃ x y z, SimpleTriangle x y z