Theorem: proportional_iff_para
Proof 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
Proof 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)