Theorem: para_len_parallelogram (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
⊢ para N O
Tactic:
have abc_bcd := alternate_eq_of_para aL bL bP cP cM dM aPd pLM
State after:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ para N O

State before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ para N O
Tactic:
obtain ⟨-, -, bca_cbd⟩ := sas (by perma) (by perm) (by perma)
State after:
case intro.intro
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
bca_cbd : angle ?m.55016 ?m.55020 ?m.55017 = angle ?m.55018 ?m.55021 ?m.55019
⊢ para N O

State before:
case intro.intro
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
bca_cbd : angle ?m.55016 ?m.55020 ?m.55017 = angle ?m.55018 ?m.55021 ?m.55019
⊢ para N O
Tactic:
exact para_of_ang_eq cb aN cN cP bP bO dO aPd bca_cbd
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ length b a = length c d
Tactic:
perma
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ length b c = length c b
Tactic:
perm
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M N O P : line
aL : online a L
bL : online b L
cM : online c M
dM : online d M
aN : online a N
cN : online c N
bO : online b O
dO : online d O
bP : online b P
cP : online c P
cb : c ≠ b
aPd : diffside a d P
pLM : para L M
hlen : length a b = length c d
abc_bcd : angle a b c = angle b c d
⊢ angle a b c = angle d c b
Tactic:
perma
State after:
no goals