internlm/Lean-Github huggingface dataset:
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have prop2 := similar_of_AA (tri213 Tdca) (tri312 Tabc) acb_dca.symm (by linperm)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have rat2 := (proportion_len_iff _ _ _ _ _ _ _ _ ca cb).mpr prop2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d / length c a = length c a / length c b
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d / length c a = length c a / length c b
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
field_simp at rat2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
perm [length_sum_of_B Bbdc]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
this : length b d + length c d = length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
this : length b d + length c d = length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
conv in (occs := *) length _ _ ^ 2 => all_goals rw [sq]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
this : length b d + length c d = length b c
⊢ length a b * length a b + length a c * length a c = length b c * length b c
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length c b = length c a * length c a
this : length b d + length c d = length b c
⊢ length a b * length a b + length a c * length a c = length b c * length b c
Tactic:
perm at rat1, rat2
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length a b * length a b
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length b c = length a c * length a c
this : length b d + length c d = length b c
⊢ length a b * length a b + length a c * length a c = length b c * length b c
Theorem: pythagorean_proof_two
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length a b * length a b
prop2 : proportion (length c d) (length c a) (length c a) (length c b)
rat2 : length c d * length b c = length a c * length a c
this : length b d + length c d = length b c
⊢ length a b * length a b + length a c * length a c = length b c * length b c
Tactic:
rw [← rat1, ← rat2, ← right_distrib, this]
Proof state after:
no goals
Theorem: pythagorean_proof_two
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
⊢ angle a b c = angle d b a
Tactic:
linperm [aux4 ba Bbdc]
Proof state after:
no goals
Theorem: pythagorean_proof_two
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
⊢ angle a c b = angle d c a
Tactic:
linperm [aux4 ca $ B_symm Bbdc]
Proof state after:
no goals
Theorem: pythagorean_proof_two
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
⊢ angle b d a = angle b a c
Tactic:
linarith
Proof state after:
no goals
Theorem: pythagorean_proof_two
Proof state before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
d : point
Bbdc : B b d c
ang_bda : angle b d a = rightangle
ang_cda : angle c d a = rightangle
ba : length b a ≠ 0
ca : length c a ≠ 0
bc : length b c ≠ 0
cb : length c b ≠ 0
Tdba : triangle d b a
Tdca : triangle d c a
abc_dba : angle a b c = angle d b a
acb_dca : angle a c b = angle d c a
prop1 : proportion (length b d) (length b a) (length b a) (length b c)
rat1 : length b d * length b c = length b a * length b a
⊢ angle c d a = angle c a b
Tactic:
linperm
Proof state after:
no goals
Theorem: perpendicular_of_online''
Proof state before:
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases length_eq_B_of_ne ab ab.symm with ⟨d, Babd, _⟩
Proof state after:
case intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Theorem: perpendicular_of_online''
Proof state before:
case intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases diffside_of_not_online fL with ⟨f', f'L, ff'L⟩
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Theorem: perpendicular_of_online''
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
rcases perpendicular_of_online Babd aL bL f'L with ⟨c, cf'L, right, _⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Theorem: perpendicular_of_online''
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ ∃ c, diffside c f L ∧ angle a b c = rightangle
Tactic:
exact ⟨c, diffside_of_sameside_diffside (sameside_symm cf'L) ⟨f'L, fL, not_sameside_symm ff'L⟩ , by perma[right]⟩
Proof state after:
no goals
Theorem: perpendicular_of_online''
Proof state before:
i : incidence_geometry
a b : point
L : line
f : point
ab : a ≠ b
aL : online a L
bL : online b L
fL : ¬online f L
d : point
Babd : B a b d
right✝¹ : length b a = length b d
f' : point
f'L : ¬online f' L
ff'L : ¬sameside f f' L
c : point
cf'L : sameside c f' L
right : angle c b a = rightangle
right✝ : angle c b d = rightangle
⊢ angle a b c = rightangle
Tactic:
perma[right]
Proof state after:
no goals
Theorem: pythagoras_converse
Proof state before:
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a c with ⟨L, aL, cL⟩
Proof state after:
case intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a b with ⟨N, aN, bN⟩
Proof state after:
case intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
⊢ angle b a c = rightangle
Tactic:
rcases length_eq_B_of_ne_four (ne_21_of_tri tri_abc) (ne_21_of_tri tri_abc) with ⟨e, Bbae, ba_ae⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
⊢ angle b a c = rightangle
Tactic:
rcases perpendicular_of_online'' (ne_31_of_tri tri_abc) cL aL (offline_of_B_offline (B_symm Bbae)
  (online_3_of_B Bbae bN aN) aN aL cL (online_3_of_triangle aN bN tri_abc)) with ⟨d', d'eL, cad'_ra⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
⊢ angle b a c = rightangle
Tactic:
rcases length_eq_B_of_ne_four (ne_of_online aL d'eL.1).symm (ne_21_of_tri tri_abc)
  with ⟨d, Bd'ad, ba_ad⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
⊢ angle b a c = rightangle
Tactic:
rcases line_of_pts a d' with ⟨M, aM, d'M⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
⊢ angle b a c = rightangle
Tactic:
have cM := online_2_of_triangle aM d'M $ triangle_of_ne_online (ne_13_of_tri tri_abc) aL cL d'eL.1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
⊢ angle b a c = rightangle
Theorem: pythagoras_converse
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
⊢ angle b a c = rightangle
Tactic:
have ang_split := two_right_of_flat_angle Bd'ad d'M aM cM
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c : point
tri_abc : triangle a b c
sq_sum : length a b ^ 2 + length a c ^ 2 = length b c ^ 2
L : line
aL : online a L
cL : online c L
N : line
aN : online a N
bN : online b N
e : point
Bbae : B b a e
ba_ae : length b a = length a e
d' : point
d'eL : diffside d' e L
cad'_ra : angle c a d' = rightangle
d : point
Bd'ad : B d' a d
ba_ad : length b a = length a d
M : line
aM : online a M
d'M : online d' M
cM : ¬online c M
ang_split : angle c a d' + angle c a d = 2 * rightangle
⊢ angle b a c = rightangle