Theorem: area_of_parallelogram (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
obtain ⟨ aL, bL, bM, cM, cN, dN, dO, aO, pLN, pMO⟩ := id abcd
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
have bcda : paragram b c d a M N O L := by splitAll <;> perma only [para]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c ∧ area b a d + area b c d = 2 * area a b c
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area b a d + area b c d = 2 * area a b c

State before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
⊢ paragram b c d a M N O L
Tactic:
splitAll <;> perma only [para]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area a b c + area a d c = 2 * area a b c
Tactic:
linperm [(len_ang_area_eq_of_parallelogram bcda).2.2]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ area b a d + area b c d = 2 * area a b c
Tactic:
linperm [(len_ang_area_eq_of_parallelogram abcd).2.2, triarea cN dN bL aL (by perma)]
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L M N O : line
abcd : paragram a b c d L M N O
aL : online a L
bL : online b L
bM : online b M
cM : online c M
cN : online c N
dN : online d N
dO : online d O
aO : online a O
pLN : para L N
pMO : para M O
bcda : paragram b c d a M N O L
⊢ para N L
Tactic:
perma
State after:
no goals