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