Theorem: ProjectivePlane.intersectionPoint_right (ProjectivePlane.lean)

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

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