internlm/Lean-Github huggingface dataset:
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
⊢ False
Tactic:
rw [← hag_bac] at bac_edf
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
⊢ False
Tactic:
have ang := sas Hg.2 Hh.2 (by perma at *)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle d e f
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle d e f
⊢ False
Tactic:
rw [← abc_def] at ang
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ False
Tactic:
have' := parallel_of_similar aAB hAB bAB aAC cAC hHG gHG bBC cBC (ne_23_of_B Hh.1).symm (ne_13_of_B Hh.1) hg bc ac hAC ang.2.2.symm Hh.1 _
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_2
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
this : para HG BC
⊢ False

case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_2
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
this✝ : para HG BC
ss1 : sameside h g BC
ss2 : sameside g a BC
this : sameside a h BC
⊢ False

case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB
Tactic:
exact (not_sameside13_of_B123_online2 Hh.1 bBC) this
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB
Tactic:
perma [sameside_of_B_not_online_2 Hg.1 aAB gAB]
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
⊢ False
Tactic:
rw [hg] at Hh
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b g ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b g ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
⊢ False
Tactic:
have := online_2_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b g ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
this : online b AC
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b g ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
this : online b AC
⊢ False
Tactic:
exact (online_3_of_triangle aAC cAC (by perma)) this
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b g ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h = g
this : online b AC
⊢ triangle a c b
Tactic:
perma
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : online h AC
⊢ False
Tactic:
have := line_unique_of_pts (ne_13_of_B Hh.1).symm hAC aAC hAB aAB
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : online h AC
this : AC = AB
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : online h AC
this : AC = AB
⊢ False
Tactic:
rw [this] at bAC
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AB
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : online h AC
this : AC = AB
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AB
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : online h AC
this : AC = AB
⊢ False
Tactic:
exact bAC bAB
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
⊢ angle h a g = angle b a c
Tactic:
linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_13_of_B Hh.1) Hg.1]
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
⊢ angle g a h = angle f d e
Tactic:
perma at *
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
this : para HG BC
ss1 : sameside h g BC
ss2 : sameside g a BC
⊢ sameside g ?m.177226 BC
Tactic:
perma at ss1
Proof state after:
no goals