obtain ⟨⟨x, y⟩, (hxy : x ≠ y), h⟩ := S.toFinite.exists_minimal_wrt (Function.uncurry dist) _ this
case inr
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x y z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
case inr.intro.mk.intro
V✝ : Type u_1
inst✝⁴ : MetricSpace V✝
u v w : V✝
inst✝³ : Finite V✝
inst✝² : Nontrivial V✝
x✝ y✝ z : V✝
V : Type u_2
inst✝¹ : MetricSpace V
inst✝ : Finite V
h✝ : Nontrivial V
S : Set (V × V) := (Set.diagonal V)ᶜ
this : S.Nonempty
x y : V
hxy : x ≠ y
h :
  ∀ a' ∈ S,
    Function.uncurry dist a' ≤ Function.uncurry dist (x, y) → Function.uncurry dist (x, y) = Function.uncurry dist a'
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y