exact ⟨dist x y, by simp [hxy], fun a b hab => le_of_not_lt (fun h' => h'.ne' (h _ _ hab h'.le))⟩
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 b : V), (a, b) ∈ S → dist a b ≤ dist x y → dist x y = dist a b
⊢ ∃ r, 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y
no goals