Theorem: generateLine_minimal (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
⊢ GenerateLine S ⊆ L
Tactic:
intro x hx
State after:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x : V
hx : x ∈ GenerateLine S
⊢ x ∈ L

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x : V
hx : x ∈ GenerateLine S
⊢ x ∈ L
Tactic:
induction hx with
| basic h => exact hL₀ h
| extend_out u v w _ _ hw hu hv => exact out_closed hu hv hw
| extend_in u v w _ _ hw hu hv => exact in_closed hu hv hw
State after:
no goals

State before:
case basic
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x x✝ : V
h : x✝ ∈ S
⊢ x✝ ∈ L
Tactic:
exact hL₀ h
State after:
no goals

State before:
case extend_out
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x u v w : V
a✝¹ : GenerateLine S u
a✝ : GenerateLine S v
hw : sbtw u v w
hu : u ∈ L
hv : v ∈ L
⊢ w ∈ L
Tactic:
exact out_closed hu hv hw
State after:
no goals

State before:
case extend_in
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x u v w : V
a✝¹ : GenerateLine S u
a✝ : GenerateLine S v
hw : sbtw u w v
hu : u ∈ L
hv : v ∈ L
⊢ w ∈ L
Tactic:
exact in_closed hu hv hw
State after:
no goals