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