Theorem: tri_sum_contra (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ False
Tactic:
apply cO
State after:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ online c O

State before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ online c O
Tactic:
apply (area_zero_iff_online de dO eO).mp
State after:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ area d e c = 0

State before:
i : incidence_geometry
b c d e : point
O : line
bO : online b O
dO : online d O
eO : online e O
cO : ¬online c O
bd : b ≠ d
de : d ≠ e
eb : e ≠ b
Bbed : B b e d
ar : area b c d = area b c e
⊢ area d e c = 0
Tactic:
linperm [(area_add_iff_B eb.symm de.symm bd.symm bO eO dO cO).mp Bbed]
State after:
no goals