simp [Subsingleton.elim x y]
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✝ : Subsingleton V
x y : V
⊢ x ≠ y → 1 ≤ dist x y
no goals