Theorem: eq_area_of_eq_base_samevertex (Pythagoras/euclid_I_extras.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
hlen : length b c = length e f
⊢ area a b c = area a e f
Tactic:
by_cases bc : b = c
State after:
case pos
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
hlen : length b c = length e f
bc : b = c
⊢ area a b c = area a e f

case neg
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
hlen : length b c = length e f
bc : ¬b = c
⊢ area a b c = area a e f

State before:
case neg
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
hlen : length b c = length e f
bc : ¬b = c
⊢ area a b c = area a e f
Tactic:
have ef : e ≠ f := ne_of_ne_len bc hlen
State after:
case neg
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
⊢ area a b c = area a e f

State before:
case neg
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
⊢ area a b c = area a e f
Tactic:
by_cases aL : online a L
State after:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
⊢ area a b c = area a e f

case neg
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
⊢ area a b c = area a e f

State before:
case neg
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
⊢ area a b c = area a e f
Tactic:
obtain ⟨ _, hM ⟩ := parallel_of_line_pt aL
State after:
case neg.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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
w✝ : line
hM : online a w✝ ∧ para L w✝
⊢ area a b c = area a e f

State before:
case neg.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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : ¬online a L
w✝ : line
hM : online a w✝ ∧ para L w✝
⊢ area a b c = area a e f
Tactic:
exact eq_area_of_eq_base hM.1 bL cL hM.1 eL fL hM.2 hlen
State after:
no goals

State before:
case pos
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
hlen : length b c = length e f
bc : b = c
⊢ area a b c = area a e f
Tactic:
have ef: e = f := (same_len_pts_coincide_iff hlen).mp bc
State after:
case pos
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
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ area a b c = area a e f

State before:
case pos
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
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ area a b c = area a e f
Tactic:
rw [area_of_eq a b c (by tauto), area_of_eq a e f (by tauto)]
State after:
no goals

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
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ a = b ∨ a = c ∨ b = c
Tactic:
tauto
State after:
no goals

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
hlen : length b c = length e f
bc : b = c
ef : e = f
⊢ a = e ∨ a = f ∨ e = f
Tactic:
tauto
State after:
no goals

State before:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
⊢ area a b c = area a e f
Tactic:
perm [(area_zero_iff_online bc bL cL).mpr aL]
State after:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ area a b c = area a e f

State before:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ area a b c = area a e f
Tactic:
rw [this]
State after:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ 0 = area a e f

State before:
case pos
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
hlen : length b c = length e f
bc : ¬b = c
ef : e ≠ f
aL : online a L
this : area a b c = 0
⊢ 0 = area a e f
Tactic:
linperm [(area_zero_iff_online ef eL fL).mpr aL]
State after:
no goals