Theorem: eq_area_of_same_base_implies_para (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
⊢ para L M
Tactic:
obtain ⟨N, aN, pNL⟩ := para_of_offline aL
State after:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
⊢ para L M

State before:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
⊢ para L M
Tactic:
have pNO: ¬ para N O := fun pNO => by
  have LO_or_pLO := para_trans (para_symm pNL) pNO
  cases LO_or_pLO with
  | inl LO => rw [← LO] at cO; exact cO cL
  | inr pLO => exact neq_of_para bL bO pLO rfl
State after:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
⊢ para L M

State before:
case intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
⊢ para L M
Tactic:
rcases pt_of_line_line pNO with ⟨e, eN, eO⟩
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
⊢ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
⊢ para L M
Tactic:
have ar2 := eq_area_of_eq_base aN bL cL eN bL cL pNL rfl
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area a b c = area e b c
⊢ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area a b c = area e b c
⊢ para L M
Tactic:
rw [ar] at ar2
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
⊢ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
⊢ para L M
Tactic:
have be := neq_of_para bL eN pNL
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
⊢ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
⊢ para L M
Tactic:
by_cases de: d = e
State after:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M

case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : ¬d = e
⊢ para L M

State before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
⊢ False
Tactic:
have LO_or_pLO := para_trans (para_symm pNL) pNO
State after:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO_or_pLO : L = O ∨ para L O
⊢ False

State before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO_or_pLO : L = O ∨ para L O
⊢ False
Tactic:
cases LO_or_pLO with
| inl LO => rw [← LO] at cO; exact cO cL
| inr pLO => exact neq_of_para bL bO pLO rfl
State after:
no goals

State before:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False
Tactic:
rw [← LO] at cO
State after:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c L
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False

State before:
case inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c L
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
LO : L = O
⊢ False
Tactic:
exact cO cL
State after:
no goals

State before:
case inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : para N O
pLO : para L O
⊢ False
Tactic:
exact neq_of_para bL bO pLO rfl
State after:
no goals

State before:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M
Tactic:
rw [← de] at eN
State after:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online d N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M

State before:
case pos
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online d N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d = e
⊢ para L M
Tactic:
rwa [line_unique_of_pts ad aM dM aN eN]
State after:
no goals

State before:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : ¬d = e
⊢ para L M
Tactic:
rw [← Ne.def d e] at de
State after:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ para L M

State before:
case neg
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ para L M
Tactic:
exfalso
State after:
case neg.h
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ False

State before:
case neg.h
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
⊢ False
Tactic:
cases B_of_three_online_ne be bd de.symm bO eO dO with
| inl Bbed =>
  exact tri_sum_contra bO dO eO cO bd de be.symm Bbed (by perma at ar2)
| inr HB =>
  cases HB with
  | inl Bebd =>
    have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
    have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
    have dsedL:= not_sameside13_of_B123_online2 Bebd bL
    exact dsedL ssedL
  | inr Bbde =>
    exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
State after:
no goals

State before:
case neg.h.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbed : B b e d
⊢ False
Tactic:
exact tri_sum_contra bO dO eO cO bd de be.symm Bbed (by perma at ar2)
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbed : B b e d
⊢ area b c d = area b c e
Tactic:
perma at ar2
State after:
no goals

State before:
case neg.h.inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
HB : B e b d ∨ B b d e
⊢ False
Tactic:
cases HB with
| inl Bebd =>
  have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
  have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
  have dsedL:= not_sameside13_of_B123_online2 Bebd bL
  exact dsedL ssedL
| inr Bbde =>
  exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
State after:
no goals

State before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
⊢ False
Tactic:
have ssaeL := sameside_of_para_online aN eN (para_symm pNL)
State after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
⊢ False

State before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
⊢ False
Tactic:
have ssedL := sameside_symm (sameside_trans ssadL ssaeL)
State after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
⊢ False

State before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
⊢ False
Tactic:
have dsedL:= not_sameside13_of_B123_online2 Bebd bL
State after:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
dsedL : ¬sameside e d L
⊢ False

State before:
case neg.h.inr.inl
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bebd : B e b d
ssaeL : sameside a e L
ssedL : sameside e d L
dsedL : ¬sameside e d L
⊢ False
Tactic:
exact dsedL ssedL
State after:
no goals

State before:
case neg.h.inr.inr
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbde : B b d e
⊢ False
Tactic:
exact tri_sum_contra bO eO dO cO be de.symm bd.symm Bbde (by perma at ar2)
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M O : line
bL : online b L
cL : online c L
aL : ¬online a L
aM : online a M
dM : online d M
bO : online b O
dO : online d O
cO : ¬online c O
ad : a ≠ d
bd : b ≠ d
ssadL : sameside a d L
ar : area a b c = area d b c
N : line
aN : online a N
pNL : para L N
pNO : ¬para N O
e : point
eN : online e N
eO : online e O
ar2 : area d b c = area e b c
be : b ≠ e
de : d ≠ e
Bbde : B b d e
⊢ area b c e = area b c d
Tactic:
perma at ar2
State after:
no goals