Theorem: length_eq_of_length_eq (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
hlen : 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
hlen : 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
hlen : 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
hlen : 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
⊢ length d e = length a b
Tactic:
have de := ne_12_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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
⊢ length d e = length a b
Tactic:
have ef := ne_23_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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
⊢ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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 cAB := online_3_of_triangle aAB bAB Tabc
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
⊢ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
⊢ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
⊢ length d e = length a b
Tactic:
by_contra contra
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : ¬length d e = length a b
⊢ False

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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : ¬length d e = length a b
⊢ False
Tactic:
simp_rw [← Ne.def, ne_iff_lt_or_gt] at contra
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
⊢ False

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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
⊢ False
Tactic:
wlog lineq : length a b < length d e
State after:
case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
⊢ False

State before:
case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
⊢ False
Tactic:
swap
State after:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
obtain ⟨h, Hh⟩ := same_length_B_of_ne_ge ab lineq
State after:
case intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
obtain ⟨HC, hHC, cHC⟩ := line_of_pts h c
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
have hAB := online_3_of_B Hh.1 aAB bAB
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
have hc : h ≠ c := fun hc => cAB (by rwa [hc] at hAB)
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ 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
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
have hac_bac := (angle_extension_of_B ac Hh.1).symm
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
rw [← hac_bac] at bac_edf
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
have SAS := sas hlen.symm Hh.2 (by perma at *)
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle d e f
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle d e f
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
rw [← abc_def] at SAS
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle a b c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle a b c
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
have := parallel_of_similar aAB hAB bAB aAC cAC hHC cHC bBC cBC (ne_23_of_B Hh.1).symm (ne_13_of_B Hh.1) hc bc ac hAC SAS.2.2.symm Hh.1 (sameside_rfl_of_not_online cAB)
State after:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle a b c
this : para HC BC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case intro.intro.intro
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
SAS : length c h = length f e ∧ angle a c h = angle d f e ∧ angle a h c = angle a b c
this : para HC BC
⊢ False

case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
exact neq_of_para cHC cBC this rfl
State after:
case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False

State before:
case 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
⊢ False
Tactic:
obtain ⟨DF, dDF, fDF⟩ := line_of_pts d f
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
⊢ False
Tactic:
obtain ⟨DE, dDE, eDE⟩ := line_of_pts d e
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
⊢ False
Tactic:
obtain ⟨EF, eEF, fEF⟩ := line_of_pts e f
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
⊢ False
Tactic:
have fDE := online_3_of_triangle dDE eDE Tdef
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
⊢ False
Tactic:
have eDF: ¬online e DF := online_3_of_triangle dDF fDF (by perma)
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
⊢ False
Tactic:
refine' this Tdef Tabc bac_edf.symm abc_def.symm hlen.symm ac df ab de ef bc DF dDF fDF DE dDE eDE EF eEF fEF fDE eDF (Or.symm contra) _
State after:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
⊢ length d e < length a b

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
⊢ length d e < length a b
Tactic:
cases contra with
| inl contra => exact contra
| inr contra => exfalso; 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
⊢ triangle a c b
Tactic:
perma
State after:
no goals

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h = c
⊢ online c AB
Tactic:
rwa [hc] at hAB
State after:
no goals

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
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✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : online h AC
this : AC = AB
⊢ False

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : online h AC
this : AC = AB
⊢ False
Tactic:
rw [this] at bAC
State after:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AB
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : online h AC
this : AC = AB
⊢ False

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AB
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : online h AC
this : AC = AB
⊢ False
Tactic:
exact bAC bAB
State after:
no goals

State before:
i✝ 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
lineq : length a b < length d e
h : point
bac_edf : angle h a c = angle e d f
Hh : B a b h ∧ length a h = length d e
HC : line
hHC : online h HC
cHC : online c HC
hAB : online h AB
hc : h ≠ c
hAC : ¬online h AC
hac_bac : angle h a c = angle b a c
⊢ angle c 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
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
contra : length d e < length a b ∨ length d e > length a b
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
⊢ triangle d f e
Tactic:
perma
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
contra : length d e < length a b
⊢ length d e < length a b
Tactic:
exact contra
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.inr.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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
contra : length d e > length a b
⊢ length d e < length a b
Tactic:
exfalso
State after:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.inr.h
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
contra : length d e > length a b
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.intro.inr.h
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
this :
  ∀ [i : incidence_geometry] {a b c d e f : point},
    ¬colinear a b c →
      ¬colinear d e f →
        angle b a c = angle e d f →
          angle a b c = angle d e f →
            length d f = length a c →
              d ≠ f →
                a ≠ c →
                  d ≠ e →
                    a ≠ b →
                      b ≠ c →
                        e ≠ f →
                          ∀ (AC : line),
                            online a AC →
                              online c AC →
                                ∀ (AB : line),
                                  online a AB →
                                    online b AB →
                                      ∀ (BC : line),
                                        online b BC →
                                          online c BC →
                                            ¬online c AB →
                                              ¬online b AC →
                                                length d e < length a b ∨ length d e > length a b →
                                                  length a b < length d e → False
lineq : ¬length a b < length d e
DF : line
dDF : online d DF
fDF : online f DF
DE : line
dDE : online d DE
eDE : online e DE
EF : line
eEF : online e EF
fEF : online f EF
fDE : ¬online f DE
eDF : ¬online e DF
contra : length d e > length a b
⊢ False
Tactic:
linarith
State after:
no goals