Theorem: parallel_of_similar (Pythagoras/euclid_VI.lean)

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
⊢ para BC HG
Tactic:
have hbc_abc : angle h b c = angle a b c := by
  have Bcbc : ¬ B c b c := fun Bcbc => ne_13_of_B Bcbc rfl
  exact angle_extension bh.symm ab bc.symm bc.symm bAB hAB aAB bBC cBC cBC (not_B_of_B (B_symm Bahb)) Bcbc
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
⊢ para BC HG

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
⊢ para BC HG
Tactic:
have AB_HG: AB ≠ HG := fun AB_HG => by
  rw [AB_HG] at aAB; refine' ag _
  have := line_unique_of_pts ag aAC gAC aAB gHG
  rw [← AB_HG] at this; rw [← this] at bAB
  exfalso; exact bAC bAB
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
⊢ para BC HG

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
⊢ para BC HG
Tactic:
obtain ⟨t, Bght, -⟩ := length_eq_B_of_ne hg.symm hg
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
⊢ para BC HG

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

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

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

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

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

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

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]
State after:
no goals

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

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
State after:
no goals

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

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

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

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

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

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

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
State after:
no goals