Theorem: parallel_of_line_pt (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ para L M
Tactic:
dsimp [para]
State after:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ ∀ (e : point), ¬online e L ∨ ¬online e M

State before:
i : incidence_geometry
a : point
L : line
aL : ¬online a L
⊢ ∃ M, online a M ∧ ∀ (e : point), ¬online e L ∨ ¬online e M
Tactic:
exact para_of_offline aL
State after:
no goals