Theorem: Set.IsLine.close_left (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
L : Set V
hL : L.IsLine
a b c : V
ha : a ∈ L
hb : b ∈ L
hc : sbtw c a b
⊢ c ∈ L
Tactic:
obtain ⟨x, y, _, rfl⟩ := hL
State after:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw c a b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y

State before:
case intro.intro.intro
V : Type u_1
inst✝ : MetricSpace V
u v w a b c : V
hc : sbtw c a b
x y : V
left✝ : x ≠ y
ha : a ∈ Line x y
hb : b ∈ Line x y
⊢ c ∈ Line x y
Tactic:
exact generateLine_close_left ha hb hc
State after:
no goals