Theorem: length_lt_of_length_lt (Pythagoras/euclid_VI.lean)

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
⊢ length d e < length a b
Tactic:
have df := ne_13_of_tri Tdef
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
⊢ length d e < length a b

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
⊢ length d e < length a b
Tactic:
have ac := ne_13_of_tri Tabc
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
⊢ length d e < length a b

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
⊢ length d e < length a b
Tactic:
have ab := ne_12_of_tri Tabc
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
⊢ length d e < length a b

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
⊢ length d e < length a b
Tactic:
have bc := ne_23_of_tri Tabc
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
⊢ length d e < length a b

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
⊢ length d e < length a b
Tactic:
obtain ⟨AC, aAC, cAC⟩ := line_of_pts a c
State after:
case 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
⊢ length d e < length a b

State before:
case 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
⊢ length d e < length a b
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
State after:
case 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
⊢ length d e < length a b

State before:
case 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
⊢ length d e < length a b
Tactic:
obtain ⟨BC, bBC, cBC⟩ := line_of_pts b c
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
⊢ length d e < length a b

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)
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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]
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

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
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

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 *)
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

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
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

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 _
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

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
⊢ 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:
have ss1 := sameside_of_para_online hHG gHG this
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
ss1 : sameside h g 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

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
⊢ 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:
have ss2 := sameside_of_B_not_online_2 (B_symm Hg.1) cBC gBC
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
ss1 : sameside h g BC
ss2 : sameside g a 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

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
⊢ 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:
perm [sameside_trans (by perma at ss1) ss2]
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
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

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
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

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]
State after:
no goals

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
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

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)
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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]
State after:
no goals

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 *
State after:
no goals

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
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.inr
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:
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
State after:
case intro.intro.intro.intro.intro.intro.intro.inr
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
this : length d f = length a c
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.inr
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
this : length d f = length a c
⊢ False
Tactic:
linarith
State after:
no goals

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
⊢ ¬colinear a c b
Tactic:
perma
State after:
no goals

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
⊢ ¬colinear d f e
Tactic:
perma
State after:
no goals

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
⊢ angle c a b = angle f d e
Tactic:
perma
State after:
no goals

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
⊢ angle b a c = angle e d f
Tactic:
perma
State after:
no goals

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
⊢ angle a b c = angle d e f
Tactic:
perma
State after:
no goals