Theorem: proportion_area_of_proportion_base_samevertex (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)
Tactic:
obtain ⟨ M, aM, pLM ⟩ := parallel_of_line_pt aL
State after:
case intro.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
M : line
aM : online a M
pLM : para L M
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)

State before:
case intro.intro
i : incidence_geometry
a b c e f : point
L : line
bL : online b L
cL : online c L
eL : online e L
fL : online f L
aL : ¬online a L
M : line
aM : online a M
pLM : para L M
⊢ proportion (length b c) (length e f) (area a b c) (area a e f)
Tactic:
exact proportion_area_of_proportion_base aM bL cL aM eL fL pLM
State after:
no goals