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