Theorem: ProjectivePlane.connectingLine_right (ProjectivePlane.lean)

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

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