Theorem: pt_of_line_line (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
L M : line
hp : ¬para L M
⊢ ∃ a, online a L ∧ online a M
Tactic:
simp_rw [para, not_forall, not_or, not_not] at hp
State after:
i : incidence_geometry
L M : line
hp : ∃ x, online x L ∧ online x M
⊢ ∃ a, online a L ∧ online a M

State before:
i : incidence_geometry
L M : line
hp : ∃ x, online x L ∧ online x M
⊢ ∃ a, online a L ∧ online a M
Tactic:
exact hp
State after:
no goals