Theorem: not_online_of_triangle (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c : point
L M : line
aL : online a L
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False
Tactic:
rw [line_unique_of_pts bc bL cL bM cM] at aL
State after:
i : incidence_geometry
a b c : point
L M : line
aL : online a M
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False

State before:
i : incidence_geometry
a b c : point
L M : line
aL : online a M
bL : online b L
bM : online b M
cM : online c M
hn : ¬online a M
bc : b ≠ c
cL : online c L
⊢ False
Tactic:
exact hn aL
State after:
no goals