internlm/Lean-Github huggingface dataset:
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
⊢ para BC HG
Tactic:
have tHG := online_3_of_B Bght gHG hHG
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
⊢ para BC HG
Tactic:
have tAB : ¬ online t AB := fun tAB =>
  AB_HG (line_unique_of_pts (ne_23_of_B Bght).symm tAB hAB tHG hHG)
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
⊢ para BC HG
Tactic:
have gAB : ¬ online g AB := fun gAB =>
  AB_HG (line_unique_of_pts (ne_12_of_B Bght) gAB hAB gHG hHG)
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
⊢ para BC HG
Tactic:
have nss := not_sameside13_of_B123_online2 Bght hAB
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
⊢ para BC HG
Tactic:
have := diffside_of_sameside_diffside hss ⟨gAB, tAB, nss⟩
Proof state after:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
this : diffside c t AB
⊢ para BC HG
Theorem: parallel_of_similar
Proof state before:
case intro.intro
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
this : diffside c t AB
⊢ para BC HG
Tactic:
apply para_of_ang_eq bh cBC bBC bAB hAB hHG tHG this _
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
this : diffside c t AB
⊢ angle h b c = angle b h t
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB ≠ HG
t : point
Bght : B g h t
tHG : online t HG
tAB : ¬online t AB
gAB : ¬online g AB
nss : ¬sameside g t AB
this : diffside c t AB
⊢ angle h b c = angle b h t
Tactic:
rw [hbc_abc, ← an, vertical_angle Bahb Bght aAB hAB gAB]
Proof state after:
no goals
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
⊢ angle h b c = angle a b c
Tactic:
have Bcbc : ¬ B c b c := fun Bcbc => ne_13_of_B Bcbc rfl
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
Bcbc : ¬B c b c
⊢ angle h b c = angle a b c
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
Bcbc : ¬B c b c
⊢ angle h b c = angle a b c
Tactic:
exact angle_extension bh.symm ab bc.symm bc.symm bAB hAB aAB bBC cBC cBC (not_B_of_B (B_symm Bahb)) Bcbc
Proof state after:
no goals
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a AB
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
⊢ False
Tactic:
rw [AB_HG] at aAB
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
⊢ False
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
⊢ False
Tactic:
refine' ag _
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
⊢ a = g
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
⊢ a = g
Tactic:
have := line_unique_of_pts ag aAC gAC aAB gHG
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = HG
⊢ a = g
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = HG
⊢ a = g
Tactic:
rw [← AB_HG] at this
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ a = g
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AB
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ a = g
Tactic:
rw [← this] at bAB
Proof state after:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AC
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ a = g
Theorem: parallel_of_similar
Proof state before:
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AC
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ a = g
Tactic:
exfalso
Proof state after:
case h
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AC
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ False
Theorem: parallel_of_similar
Proof state before:
case h
i : incidence_geometry
a b c g h : point
AB AC BC HG : line
aAB : online a HG
bAB : online b AC
hAB : online h AB
aAC : online a AC
gAC : online g AC
bBC : online b BC
cBC : online c BC
hHG : online h HG
gHG : online g HG
bh : b ≠ h
ab : a ≠ b
bc : b ≠ c
hg : h ≠ g
ag : a ≠ g
bAC : ¬online b AC
an : angle a h g = angle a b c
Bahb : B a h b
hss : sameside g c AB
hbc_abc : angle h b c = angle a b c
AB_HG : AB = HG
this : AC = AB
⊢ False
Tactic:
exact bAC bAB
Proof state after:
no goals
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
⊢ length d e = length a b
Tactic:
have df := ne_13_of_tri Tdef
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
⊢ length d e = length a b
Tactic:
have ac := ne_13_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
⊢ length d e = length a b
Tactic:
have de := ne_12_of_tri Tdef
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
⊢ length d e = length a b
Tactic:
have ab := ne_12_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
⊢ length d e = length a b
Tactic:
have bc := ne_23_of_tri Tabc
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
⊢ length d e = length a b
Tactic:
have ef := ne_23_of_tri Tdef
Proof state after:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
bac_edf : angle b a c = angle e d f
abc_def : angle a b c = angle d e f
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
⊢ length d e = length a b
Tactic:
obtain ⟨AC, aAC, cAC⟩ := line_of_pts a c
Proof state after:
case intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
AC : line
aAC : online a AC
cAC : online c AC
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
AC : line
aAC : online a AC
cAC : online c AC
⊢ length d e = length a b
Tactic:
obtain ⟨AB, aAB, bAB⟩ := line_of_pts a b
Proof state after:
case intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
⊢ length d e = length a b
Tactic:
obtain ⟨BC, bBC, cBC⟩ := line_of_pts b c
Proof state after:
case intro.intro.intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
⊢ length d e = length a b
Tactic:
have cAB := online_3_of_triangle aAB bAB Tabc
Proof state after:
case intro.intro.intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
⊢ length d e = length a b
Theorem: length_eq_of_length_eq
Proof state before:
case intro.intro.intro.intro.intro.intro
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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
⊢ length d e = length a b
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 : 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
hlen : length d f = length a c
df : d ≠ f
ac : a ≠ c
de : d ≠ e
ab : a ≠ b
bc : b ≠ c
ef : e ≠ f
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
cAB : ¬online c AB
bAC : ¬online b AC
⊢ length d e = length a b