Theorem: ProjectivePlane.connectingLine_left (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ (p q : P), p ∈ p ⊔ q
Tactic:
intro p q
State after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ p ∈ p ⊔ q

State before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
⊢ p ∈ p ⊔ q
Tactic:
exact (Exists.choose_spec (exists_connecting_line p q)).left
State after:
no goals