Theorem: proportional_iff_para' (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have ad : length a d ≠ 0 := length_eq_zero_iff.not.mpr (ne_12_of_B Badb)
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have ae : length a e ≠ 0 := length_eq_zero_iff.not.mpr (ne_12_of_B Baec)
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
have := proportional_iff_para dL eL bM cM aN dN eN Badb Baec
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ proportion (length a b) (length a d) (length a c) (length a e) ↔ para L M
Tactic:
rw [← proportion_len_iff a b a d a c a e ad ae]
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : proportion (length b d) (length a d) (length c e) (length a e) ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
Tactic:
rw [← proportion_len_iff b d a d c e a e ad ae] at this
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a b / length a d = length a c / length a e ↔ para L M
Tactic:
rw [← length_sum_of_B Badb, ← length_sum_of_B Baec, ← this]
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length d b) / length a d = (length a e + length e c) / length a e ↔
    length b d / length a d = length c e / length a e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length d b) / length a d = (length a e + length e c) / length a e ↔
    length b d / length a d = length c e / length a e
Tactic:
perm
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) / length a d = (length a e + length c e) / length a e ↔
    length b d / length a d = length c e / length a e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) / length a d = (length a e + length c e) / length a e ↔
    length b d / length a d = length c e / length a e
Tactic:
field_simp
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) * length a e = (length a e + length c e) * length a d ↔
    length b d * length a e = length c e * length a d

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ (length a d + length b d) * length a e = (length a e + length c e) * length a d ↔
    length b d * length a e = length c e * length a d
Tactic:
ring_nf
State after:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a d * length a e + length b d * length a e = length a d * length a e + length a d * length c e ↔
    length b d * length a e = length a d * length c e

State before:
i : incidence_geometry
a b c d e : point
L M N : line
dL : online d L
eL : online e L
bM : online b M
cM : online c M
aN : online a N
dN : online d N
eN : ¬online e N
Badb : B a d b
Baec : B a e c
ad : length a d ≠ 0
ae : length a e ≠ 0
this : length b d / length a d = length c e / length a e ↔ para L M
⊢ length a d * length a e + length b d * length a e = length a d * length a e + length a d * length c e ↔
    length b d * length a e = length a d * length c e
Tactic:
simp
State after:
no goals