internlm/Lean-Github huggingface dataset:
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Proof state after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Proof state after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Proof 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
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
⊢ length d e < length a b
Tactic:
cases contra with
| inl contra => exact contra
| inr contra => exfalso; linarith
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof 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
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof 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
Proof 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
Theorem: length_eq_of_length_eq
Proof 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
Proof 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
Theorem: length_eq_of_length_eq
Proof 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
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof 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 *
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
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
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof 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
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof 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
Proof state after:
no goals
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
⊢ length d e < length a b
Tactic:
have df := ne_13_of_tri Tdef
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
⊢ length d e < length a b
Tactic:
have ac := ne_13_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
⊢ length d e < length a b
Tactic:
have ab := ne_12_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
⊢ length d e < length a b
Tactic:
have bc := ne_23_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
⊢ length d e < length a b
Tactic:
obtain ⟨AC, aAC, cAC⟩ := line_of_pts a c
Proof state after:
case intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
⊢ length d e < length a b
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ length d e < length a b
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ length d e < length a b
Tactic:
obtain ⟨BC, bBC, cBC⟩ := line_of_pts b c
Proof state after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
⊢ length d e < length a b