rintro rfl
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l
⊢ x ≠ y
case refine_1
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x z : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, x, z} ⊆ l
⊢ False