Theorem: pythagorean_proof_two (Pythagoras/pythagoras_2.lean)

State before:
i : incidence_geometry
a b c : point
Tabc : triangle a b c
ang_a : angle b a c = rightangle
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ d, Bbdc, ang_bda, ang_cda ⟩ := aux Tabc ang_a.symm.le
State after:
case 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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

State before:
case 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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ ba, ca, bc, cb ⟩ := aux2 Tabc
State after:
case 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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

State before:
case 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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
obtain ⟨ Tdba, Tdca ⟩ := aux3 Tabc Bbdc
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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have abc_dba : angle a b c = angle d b a := by linperm [aux4 ba Bbdc]
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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have acb_dca : angle a c b = angle d c a := by linperm [aux4 ca $ B_symm Bbdc]
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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have prop1 := similar_of_AA (tri213 Tdba) (tri213 Tabc) abc_dba.symm (by linarith)
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)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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)
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
have rat1 := (proportion_len_iff _ _ _ _ _ _ _ _ ba bc).mpr prop1
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 a = length b a / length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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 a = length b a / length b c
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2
Tactic:
field_simp at rat1
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
⊢ length a b ^ 2 + length a c ^ 2 = length b c ^ 2

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

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

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

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

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

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

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

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

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

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

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