internlm/Lean-Github huggingface dataset:
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.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
⊢ length d e < length a b
Tactic:
have bAC : ¬online b AC := online_3_of_triangle aAC cAC (by perma)
Proof state after:
case intro.intro.intro.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
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.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
⊢ length d e < length a b
Tactic:
obtain ⟨g, Hg⟩ := B_length_eq_of_ne_lt df lineq
Proof state after:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Tactic:
have gAC := online_2_of_B Hg.1 aAC cAC
Proof state after:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Tactic:
have gBC : ¬ online g BC := fun gBC => by
  rw [line_unique_of_pts (ne_23_of_B Hg.1) gBC cBC gAC cAC] at bBC cBC
  exact bAC bBC
Proof state after:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Tactic:
have gAB : ¬ online g AB := fun gAB => by
  rw [line_unique_of_pts (ne_12_of_B Hg.1).symm gAB aAB gAC aAC] at bAB aAB
  exact bAC bAB
Proof state after:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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
⊢ length d e < length a b
Tactic:
by_contra contra
Proof state after:
case intro.intro.intro.intro.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 d e < length a b
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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 d e < length a b
⊢ False
Tactic:
rw [not_lt, le_iff_lt_or_eq] at contra
Proof state after:
case intro.intro.intro.intro.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 ∨ length a b = length d e
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.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 ∨ length a b = length d e
⊢ False
Tactic:
cases contra with
| inl contra =>
  obtain ⟨h, Hh⟩ := same_length_B_of_ne_ge ab contra
  obtain ⟨HG, hHG, gHG⟩ := line_of_pts h g
  have hAB := online_3_of_B Hh.1 aAB bAB
  have hg : h ≠ g := fun hg => by
    rw [hg] at Hh; have := online_2_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
    exact (online_3_of_triangle aAC cAC (by perma)) this
  have hAC : ¬ online h AC := fun hAC => by
    have := line_unique_of_pts (ne_13_of_B Hh.1).symm hAC aAC hAB aAB
    rw [this] at bAC; exact bAC bAB
  have hag_bac : angle h a g = angle b a c := by
    linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_13_of_B Hh.1) Hg.1]
  rw [← hag_bac] at bac_edf
  have ang := sas Hg.2 Hh.2 (by perma at *); rw [← abc_def] at ang
  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 _
  have ss1 := sameside_of_para_online hHG gHG this
  have ss2 := sameside_of_B_not_online_2 (B_symm Hg.1) cBC gBC
  perm [sameside_trans (by perma at ss1) ss2]
  exact (not_sameside13_of_B123_online2 Hh.1 bBC) this
  perma [sameside_of_B_not_online_2 Hg.1 aAB gAB]
| inr contra =>
  have: length d f = length a c := length_eq_of_length_eq (by perma) (by perma) (by perma) (asa Tabc contra (by perma) (by perma)).2.2 contra.symm
  linarith
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
⊢ 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
⊢ False
Tactic:
rw [line_unique_of_pts (ne_23_of_B Hg.1) gBC cBC gAC cAC] at bBC cBC
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 AC
cBC : online c AC
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
⊢ 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 AC
cBC : online c AC
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
⊢ False
Tactic:
exact bAC bBC
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
⊢ False
Tactic:
rw [line_unique_of_pts (ne_12_of_B Hg.1).symm gAB aAB gAC aAC] at bAB 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 AC
bAB : online b AC
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
⊢ 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 AC
bAB : online b AC
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
⊢ False
Tactic:
exact bAC bAB
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl
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
⊢ False
Tactic:
obtain ⟨h, Hh⟩ := same_length_B_of_ne_ge ab contra
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.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
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.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
⊢ False
Tactic:
obtain ⟨HG, hHG, gHG⟩ := line_of_pts h g
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
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
⊢ 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
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
⊢ False
Tactic:
have hAB := online_3_of_B Hh.1 aAB bAB
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
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
⊢ 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
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
⊢ False
Tactic:
have hg : h ≠ g := fun hg => by
  rw [hg] at Hh; have := online_2_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
  exact (online_3_of_triangle aAC cAC (by perma)) this
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
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
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
⊢ False
Tactic:
have hAC : ¬ online h AC := fun hAC => by
  have := line_unique_of_pts (ne_13_of_B Hh.1).symm hAC aAC hAB aAB
  rw [this] at bAC; exact bAC bAB
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
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
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
⊢ False
Tactic:
have hag_bac : angle h a g = angle b a c := by
  linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_13_of_B Hh.1) Hg.1]
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
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