rcases ne_or_eq a b with h | rfl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L
case inl
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
h : a ≠ b
⊢ ∃ L, L.IsLine ∧ {a, b} ⊆ L

case inr
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a : V
⊢ ∃ L, L.IsLine ∧ {a, a} ⊆ L