internlm/Lean-Github huggingface dataset:
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ False
Tactic:
have: length d f = length a c := length_eq_of_length_eq (by perma) (by perma) (by perma) (asa Tabc contra (by perma) (by perma)).2.2 contra.symm
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
this : length d f = length a c
⊢ False
Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inr
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
this : length d f = length a c
⊢ False
Tactic:
linarith
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
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ ¬colinear a c b
Tactic:
perma
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
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ ¬colinear d f e
Tactic:
perma
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
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ angle c a b = angle f d e
Tactic:
perma
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
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ angle b a c = angle e d f
Tactic:
perma
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
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b = length d e
⊢ angle a b c = angle d e f
Tactic:
perma
Proof state after:
no goals
Theorem: similar_of_AA
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
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
df : d ≠ f
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
df : d ≠ f
ac : a ≠ c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have de := ne_12_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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have ef := ne_23_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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
by_cases hlen : length d f = length a c ∨ length d e = length a b
Proof state after:
case pos
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f = length a c ∨ length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case neg
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : ¬(length d f = length a c ∨ length d e = length a b)
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case neg
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : ¬(length d f = length a c ∨ length d e = length a b)
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
conv at hlen => rw [not_or, ← Ne.def _ _]; rhs; rw [← Ne.def _ _]
Proof state after:
case neg
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case neg
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
wlog lineq : length d f < length a c
Proof state after:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : ¬length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : ¬length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
refine' proportion_inv (this Tdef Tabc bac_edf.symm abc_def.symm ac df ab de ef bc ⟨hlen.1.symm,hlen.2.symm⟩ _)
Proof state after:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : ¬length d f < length a c
⊢ length a c < length d f

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : ¬length d f < length a c
⊢ length a c < length d f

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
simp [not_lt] at lineq
Proof state after:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : length a c ≤ length d f
⊢ length a c < length d f

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case neg.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ 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 →
            d ≠ f →
              a ≠ c →
                d ≠ e →
                  a ≠ b →
                    b ≠ c →
                      e ≠ f →
                        length d f ≠ length a c ∧ length d e ≠ length a b →
                          length d f < length a c → proportion (length a b) (length d e) (length a c) (length d f)
lineq : length a c ≤ length d f
⊢ length a c < length d f

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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
exact (Ne.symm hlen.1).lt_of_le (lineq)
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨AC, aAC, cAC⟩ := line_of_pts a c
Proof state after:
case 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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case 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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
Proof state after:
case intro.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case intro.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨BC, bBC, cBC⟩ := line_of_pts b c
Proof state after:
case intro.intro.intro.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a 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
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case intro.intro.intro.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a 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
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have lineq2 := length_lt_of_length_lt Tabc Tdef bac_edf abc_def lineq
Proof state after:
case intro.intro.intro.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a 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
lineq2 : length d e < length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)