Theorem: similar_of_AA (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
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
df : d ≠ f
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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 _ _]
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)

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
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)

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⟩ _)
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)

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
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)

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)
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)

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
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)

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
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)

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
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)

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
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)

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
lineq2 : length d e < length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have bAC : ¬ online b AC:= online_3_of_triangle aAC cAC (by perma)
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
bAC : ¬online b AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
lineq2 : length d e < length a b
bAC : ¬online b AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨g, Hg⟩ := B_length_eq_of_ne_lt df lineq
State after:
case intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨h, Hh⟩ := B_length_eq_of_ne_lt de lineq2
State after:
case intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
obtain ⟨HG, hHG, gHG⟩ := line_of_pts h g
State after:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have gAC := online_2_of_B Hg.1 aAC cAC
State after:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have hAB := online_2_of_B Hh.1 aAB bAB
State after:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
rw [Hg.2.symm, Hh.2.symm]
State after:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ proportion (length a b) (length a h) (length a c) (length a g)

State before:
case intro.intro.intro.intro.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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ proportion (length a b) (length a h) (length a c) (length a g)
Tactic:
refine' (proportional_iff_para' hHG gHG bBC cBC aAB hAB _ Hh.1 Hg.1).mpr _
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ ¬online g AB

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ ¬online g AB

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC
Tactic:
by_contra contra
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
contra : online g AB
⊢ False

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
contra : online g AB
⊢ False

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC
Tactic:
rw [line_unique_of_pts (ne_12_of_B Hg.1).symm gAC aAC contra aAB] at bAC
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AB
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
contra : online g AB
⊢ False

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
bAC : ¬online b AB
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
contra : online g AB
⊢ False

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC
Tactic:
exact bAC bAB
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
⊢ para HG BC
Tactic:
have hg : h ≠ g := fun hg => by
  rw [hg] at Hh; have := online_3_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
  exact (online_3_of_triangle aAC cAC (by perma)) this
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ para HG BC

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ para HG BC
Tactic:
refine' para_symm (parallel_of_similar aAB bAB hAB aAC gAC bBC cBC hHG gHG (ne_23_of_B Hh.1).symm ab bc hg (ne_12_of_B Hg.1) bAC _ Hh.1 _)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ angle a h g = angle a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ angle a h g = angle a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB
Tactic:
have hag_bac : angle h a g = angle b a c := by
  linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_12_of_B Hh.1) Hg.1]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
hag_bac : angle h a g = angle b a c
⊢ angle a h g = angle a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
hag_bac : angle h a g = angle b a c
⊢ angle a h g = angle a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB
Tactic:
linperm [(sas Hg.2 Hh.2 (by linperm)).2.2]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ sameside g c AB
Tactic:
exact sameside_of_B_not_online_2 Hg.1 aAB fun gAB => by
  rw [line_unique_of_pts (ne_12_of_B Hg.1) aAB gAB aAC gAC] at bAB; exact bAC bAB
State after:
no goals

State before:
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)
Tactic:
wlog df_ac : length d f = length a c
State after:
case pos.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)
df_ac : ¬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
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case pos.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)
df_ac : ¬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
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
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
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
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
df_ac : length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
have := length_eq_of_length_eq Tabc Tdef bac_edf abc_def df_ac
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
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length d e) (length a c) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
rw [this, ← df_ac]
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
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length a b) (length d f) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

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
df_ac : length d f = length a c
this : length d e = length a b
⊢ proportion (length a b) (length a b) (length d f) (length d f)

case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
exact proportion_eq (length_nonneg a b) (length_nonneg d f) (length_eq_zero_iff.not.mpr ab) (length_eq_zero_iff.not.mpr df)
State after:
case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)

State before:
case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Tactic:
rw [proportion_symm_iff]
State after:
case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a c) (length d f) (length a b) (length d e)

State before:
case pos.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)
df_ac : ¬length d f = length a c
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Tactic:
have leq : length d e = length a b := by
  cases hlen with
  | inl hlen => exfalso; exact df_ac hlen
  | inr hlen => exact hlen
State after:
case pos.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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ proportion (length a c) (length d f) (length a b) (length d e)

State before:
case pos.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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ proportion (length a c) (length d f) (length a b) (length d e)
Tactic:
refine' this (by perma) (by perma) (by perma) _ de ab df ac bc.symm ef.symm (Or.symm hlen) leq
State after:
case pos.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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle a c b = angle d f e

State before:
case pos.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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle a c b = angle d f e
Tactic:
exact (asa Tabc leq.symm bac_edf (by perma [abc_def])).2.2
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
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)
df_ac : ¬length d f = length a c
⊢ length d e = length a b
Tactic:
cases hlen with
| inl hlen => exfalso; exact df_ac hlen
| inr hlen => exact hlen
State after:
no goals

State before:
case 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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ length d e = length a b
Tactic:
exfalso
State after:
case inl.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ False

State before:
case inl.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
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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)
df_ac : ¬length d f = length a c
hlen : length d f = length a c
⊢ False
Tactic:
exact df_ac hlen
State after:
no goals

State before:
case 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
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)
df_ac : ¬length d f = length a c
hlen : length d e = length a b
⊢ length d e = length a b
Tactic:
exact hlen
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
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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ ¬colinear a c b
Tactic:
perma
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
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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ ¬colinear d f e
Tactic:
perma
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
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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle c a b = angle f d e
Tactic:
perma
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
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)
df_ac : ¬length d f = length a c
leq : length d e = length a b
⊢ angle a b c = angle d e f
Tactic:
perma [abc_def]
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
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
⊢ 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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ False
Tactic:
rw [hg] at Hh
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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ 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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
⊢ False
Tactic:
have := online_3_of_B Hh.1 aAC (online_2_of_B Hg.1 aAC cAC)
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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ 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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ False
Tactic:
exact (online_3_of_triangle aAC cAC (by perma)) this
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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a g b ∧ length a g = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h = g
this : online b AC
⊢ 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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
⊢ angle h a g = angle b a c
Tactic:
linperm [angle_extension_of_B ac Hh.1, angle_extension_of_B (ne_12_of_B Hh.1) Hg.1]
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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
hag_bac : angle h a g = angle b a c
⊢ angle g a h = angle f d e
Tactic:
linperm
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
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
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g AB
⊢ False
Tactic:
rw [line_unique_of_pts (ne_12_of_B Hg.1) aAB gAB aAC gAC] at bAB
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
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AC
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g 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
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 AC
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
h : point
Hh : B a h b ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
gAC : online g AC
hAB : online h AB
hg : h ≠ g
gAB : online g AB
⊢ False
Tactic:
exact bAC bAB
State after:
no goals