Theorem: proportional_iff_para (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bN := online_3_of_B Badb aN dN
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
obtain ⟨O, aO, eO⟩ := line_of_pts a e
State after:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cO := online_3_of_B Baec aO eO
State after:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
obtain ⟨P, cP, dP⟩ := line_of_pts c d
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ab : a ≠ b := ne_13_of_B Badb
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ae : a ≠ e := ne_12_of_B Baec
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ad : a ≠ d := ne_12_of_B Badb
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bd : b ≠ d := ne_12_of_B (B_symm Badb)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ce : c ≠ e := ne_12_of_B (B_symm Baec)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have NO : N ≠ O := fun NO => eN (by rwa [← NO] at eO)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have PO : P ≠ O := fun PO => NO (line_unique_of_pts ad aO (by rwa [PO] at dP) aN dN).symm
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have dO := fun dO => NO (line_unique_of_pts ad aN dN aO dO)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have eP := fun eP => PO (line_unique_of_pts ce cP eP cO eO)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have aL := fun aL => eN (by rwa [line_unique_of_pts ad aL dL aN dN] at eL)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bL := fun bL => eN (by rwa [line_unique_of_pts bd bL dL bN dN] at eL)
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cL := fun cL => (by rwa [← line_unique_of_pts ce cO eO cL eL] at aL : ¬ online a O) aO
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bc : b ≠ c := fun bc => NO (line_unique_of_pts ab aN bN aO (by rwa [← bc] at cO))
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have cd : c ≠ d := fun cd => by rw [← cd] at dO; exact dO cO
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d) :=  proportion_area_of_proportion_base_samevertex e bN dN aN dN eN
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e) := proportion_area_of_proportion_base_samevertex d cO eO aO eO dO
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have Lad : length a d ≠ 0 := length_eq_zero_iff.not.mpr ad
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have Lae : length a e ≠ 0 := length_eq_zero_iff.not.mpr ae
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ade : area a d e ≠ 0 := (area_zero_iff_online ad aN dN).not.mpr eN
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e := by
  perm at *
  rw [eq_ratio_of_proportion Lad ade bd_ad, eq_ratio_of_proportion Lae ade ce_ae]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have prop_iff : proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e := by
  rwa [← proportion_len_iff b d a d c e a e Lad Lae]
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
have bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔
  area b d e = area c d e := by rw [prop_iff]; perm; field_simp
State after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M

State before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
Tactic:
constructor
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ proportion (length b d) (length a d) (length c e) (length a e) → para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ proportion (length b d) (length a d) (length c e) (length a e) → para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
intro ar
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : proportion (length b d) (length a d) (length c e) (length a e)
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : proportion (length b d) (length a d) (length c e) (length a e)
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
rw [bde_cde] at ar
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
have nsabL:= not_sameside13_of_B123_online2 Badb dL
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
have nsacL:= not_sameside13_of_B123_online2 Baec eL
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
nsacL : ¬sameside a c L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
nsacL : ¬sameside a c L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
have ssbcL := sameside_of_diffside_diffside ⟨aL, bL, nsabL⟩ ⟨aL, cL, nsacL⟩
State after:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
nsacL : ¬sameside a c L
ssbcL : sameside b c L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mp
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
ar : area b d e = area c d e
nsabL : ¬sameside a b L
nsacL : ¬sameside a c L
ssbcL : sameside b c L
⊢ para L M

case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
exact eq_area_of_same_base_implies_para dL eL bL bM cM dP cP eP bc cd.symm ssbcL ar
State after:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
⊢ para L M → proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
intro pLM
State after:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
pLM : para L M
⊢ proportion (length b d) (length a d) (length c e) (length a e)

State before:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
pLM : para L M
⊢ proportion (length b d) (length a d) (length c e) (length a e)
Tactic:
rw [bde_cde]
State after:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
pLM : para L M
⊢ area b d e = area c d e

State before:
case intro.intro.intro.intro.mpr
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
bde_cde : proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
pLM : para L M
⊢ area b d e = area c d e
Tactic:
exact para_implies_eq_area_of_same_base bM cM dL eL pLM
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N = O
⊢ online e N
Tactic:
rwa [← NO] at eO
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P = O
⊢ online d O
Tactic:
rwa [PO] at dP
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : ?m.98629
⊢ online e N
Tactic:
rwa [line_unique_of_pts ad aL dL aN dN] at eL
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : ?m.98701
⊢ online e N
Tactic:
rwa [line_unique_of_pts bd bL dL bN dN] at eL
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : ?m.98773
⊢ ¬online a O
Tactic:
rwa [← line_unique_of_pts ce cO eO cL eL] at aL
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b = c
⊢ online b O
Tactic:
rwa [← bc] at cO
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c = d
⊢ False
Tactic:
rw [← cd] at dO
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online c O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c = d
⊢ False

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online c O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c = d
⊢ False
Tactic:
exact dO cO
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
⊢ length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
Tactic:
perm at *
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area b d e) (area a d e)
ce_ae : proportion (length c e) (length a e) (area c d e) (area a d e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
⊢ length b d / length a d = length c e / length a e ↔ area b d e / area a d e = area c d e / area a d e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area b d e) (area a d e)
ce_ae : proportion (length c e) (length a e) (area c d e) (area a d e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
⊢ length b d / length a d = length c e / length a e ↔ area b d e / area a d e = area c d e / area a d e
Tactic:
rw [eq_ratio_of_proportion Lad ade bd_ad, eq_ratio_of_proportion Lae ade ce_ae]
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
Tactic:
rwa [← proportion_len_iff b d a d c e a e Lad Lae]
State after:
no goals

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ proportion (length b d) (length a d) (length c e) (length a e) ↔ area b d e = area c d e
Tactic:
rw [prop_iff]
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ area e b d / area e a d = area d c e / area d a e ↔ area b d e = area c d e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ area e b d / area e a d = area d c e / area d a e ↔ area b d e = area c d e
Tactic:
perm
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ area b d e / area a d e = area c d e / area a d e ↔ area b d e = area c d e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
bN : online b N
O : line
aO : online a O
eO : online e O
cO : online c O
P : line
cP : online c P
dP : online d P
ab : a ≠ b
ae : a ≠ e
ad : a ≠ d
bd : b ≠ d
ce : c ≠ e
NO : N ≠ O
PO : P ≠ O
dO : online d O → False
eP : online e P → False
aL : online a L → False
bL : online b L → False
cL : online c L → False
bc : b ≠ c
cd : c ≠ d
bd_ad : proportion (length b d) (length a d) (area e b d) (area e a d)
ce_ae : proportion (length c e) (length a e) (area d c e) (area d a e)
Lad : length a d ≠ 0
Lae : length a e ≠ 0
ade : area a d e ≠ 0
ratio_iff : length b d / length a d = length c e / length a e ↔ area e b d / area e a d = area d c e / area d a e
prop_iff :
  proportion (length b d) (length a d) (length c e) (length a e) ↔ area e b d / area e a d = area d c e / area d a e
⊢ area b d e / area a d e = area c d e / area a d e ↔ area b d e = area c d e
Tactic:
field_simp
State after:
no goals