internlm/Lean-Github huggingface dataset:
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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]
Proof 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
Theorem: proportional_iff_para
Proof 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]
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof 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)
Theorem: proportional_iff_para
Proof 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]
Proof 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
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals
Theorem: proportional_iff_para
Proof 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
Proof state after:
no goals