Theorem: neq_of_para (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
⊢ False
Tactic:
have := offline_of_para aL pLM
State after:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online a M
⊢ False

State before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online a M
⊢ False
Tactic:
rw [ab] at this
State after:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online b M
⊢ False

State before:
i : incidence_geometry
a b : point
L M : line
aL : online a L
bM : online b M
pLM : para L M
ab : a = b
this : ¬online b M
⊢ False
Tactic:
exact this bM
State after:
no goals