aesop
case refine_1.intro.intro
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
L : Set V
hL : L.IsLine
hL' : {x, z} ⊆ L
⊢ False
no goals