rintro rfl
case refine_3
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
⊢ y ≠ z
case refine_3
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y : V
hl : ∀ (l : Set V), l.IsLine → ¬{x, y, y} ⊆ l
⊢ False