Theorem: ProjectivePlane.intersectionPoint_left (ProjectivePlane.lean)

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

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
⊢ l ⊓ m ∈ l
Tactic:
exact (Exists.choose_spec (exists_intersection_point l m)).left
State after:
no goals