internlm/Lean-Github huggingface dataset:
Theorem: similar_of_AA
Proof state before:
case intro.intro.intro.intro.intro.intro
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
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)
Proof state after:
case intro.intro.intro.intro.intro.intro
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
lineq2 : length d e < length a b
bAC : ¬online b AC
⊢ proportion (length a b) (length d e) (length a c) (length d f)
Theorem: similar_of_AA
Proof state before:
case intro.intro.intro.intro.intro.intro
i✝ i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
hlen : length d f ≠ length a c ∧ length d e ≠ length a b
lineq : length d f < length a c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
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
Proof 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)
Theorem: similar_of_AA
Proof 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
Proof 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)
Theorem: similar_of_AA
Proof 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
Proof 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)
Theorem: similar_of_AA
Proof 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
Proof 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)
Theorem: similar_of_AA
Proof 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
Proof 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)
Theorem: similar_of_AA
Proof 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]
Proof 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)
Theorem: similar_of_AA
Proof 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 _
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 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
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 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
Proof 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
Theorem: similar_of_AA
Proof 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
Proof 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
Theorem: similar_of_AA
Proof 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 _)
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
⊢ 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
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
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]
Proof 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
Theorem: similar_of_AA
Proof 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
Proof state after:
no goals