Theorem: length_eq_of_length_eq
Proof 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
Proof 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