internlm/Lean-Github huggingface dataset:
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 : online c L → False
bc : b = c
⊢ online b O
Tactic:
rwa [← bc] at cO
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 : online c L → False
bc : b ≠ c
cd : c = d
⊢ False
Tactic:
rw [← cd] at dO
Proof 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
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 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
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 : 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 *
Proof 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
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 : 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]
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 : 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]
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 : 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]
Proof 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
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 : 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
Proof 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
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 : 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
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
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have ad : length a d ≠ 0 := length_eq_zero_iff.not.mpr (ne_12_of_B Badb)
Proof 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
ad : length a d ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
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
ad : length a d ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have ae : length a e ≠ 0 := length_eq_zero_iff.not.mpr (ne_12_of_B Baec)
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
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
ad : length a d ≠ 0
ae : length a e ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have := proportional_iff_para dL eL bM cM aN dN eN Badb Baec
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
rw [← proportion_len_iff a b a d a c a e ad ae]
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
Tactic:
rw [← proportion_len_iff b d a d c e a e ad ae] at this
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
Tactic:
rw [← length_sum_of_B Badb, ← length_sum_of_B Baec, ← this]
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length d b) / length a d = (length a e + length e c) / length a e ↔
    length b d / length a d = length c e / length a e
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length d b) / length a d = (length a e + length e c) / length a e ↔
    length b d / length a d = length c e / length a e
Tactic:
perm
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) / length a d = (length a e + length c e) / length a e ↔
    length b d / length a d = length c e / length a e
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) / length a d = (length a e + length c e) / length a e ↔
    length b d / length a d = length c e / length a e
Tactic:
field_simp
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) * length a e = (length a e + length c e) * length a d ↔
    length b d * length a e = length c e * length a d
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) * length a e = (length a e + length c e) * length a d ↔
    length b d * length a e = length c e * length a d
Tactic:
ring_nf
Proof 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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a d * length a e + length b d * length a e = length a d * length a e + length a d * length c e ↔
    length b d * length a e = length a d * length c e
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
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a d * length a e + length b d * length a e = length a d * length a e + length a d * length c e ↔
    length b d * length a e = length a d * length c e
Tactic:
simp
Proof state after:
no goals
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
⊢ para BC HG
Tactic:
have hbc_abc : angle h b c = angle a b c := by
  have Bcbc : ¬ B c b c := fun Bcbc => ne_13_of_B Bcbc rfl
  exact angle_extension bh.symm ab bc.symm bc.symm bAB hAB aAB bBC cBC cBC (not_B_of_B (B_symm Bahb)) Bcbc
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
⊢ para BC HG
Tactic:
have AB_HG: AB ≠ HG := fun AB_HG => by
  rw [AB_HG] at aAB; refine' ag _
  have := line_unique_of_pts ag aAC gAC aAB gHG
  rw [← AB_HG] at this; rw [← this] at bAB
  exfalso; exact bAC bAB
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
⊢ para BC HG
Tactic:
obtain ⟨t, Bght, -⟩ := length_eq_B_of_ne hg.symm hg
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
⊢ para BC HG