Theorem: lt_area_of_lt_base_sameedge_nBfbc (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
⊢ length b c > length b f → area a b c > area a b f
Tactic:
intro hlen
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b c > length b f
⊢ area a b c > area a b f

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b c > length b f
⊢ area a b c > area a b f
Tactic:
simp [gt_iff_lt] at hlen
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
⊢ area a b c > area a b f

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
⊢ area a b c > area a b f
Tactic:
have cf: c ≠ f := fun cf => by rw [cf, lt_self_iff_false] at hlen; exact hlen
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
⊢ area a b c > area a b f

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
⊢ area a b c > area a b f
Tactic:
have := B_of_three_online_ne_short hlen bf bc cf.symm bL fL cL
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
this : B b f c ∨ B f b c
⊢ area a b c > area a b f

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
this : B b f c ∨ B f b c
⊢ area a b c > area a b f
Tactic:
cases this with
| inl h => exact lt_area_of_lt_base_sameedge_Bbfc a bL cL fL h bc bf cf aL hlen
| inr h => exfalso; exact hB h
State after:
no goals

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c = f
⊢ False
Tactic:
rw [cf, lt_self_iff_false] at hlen
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : False
cf : c = f
⊢ False

State before:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : False
cf : c = f
⊢ False
Tactic:
exact hlen
State after:
no goals

State before:
case inl
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B b f c
⊢ area a b c > area a b f
Tactic:
exact lt_area_of_lt_base_sameedge_Bbfc a bL cL fL h bc bf cf aL hlen
State after:
no goals

State before:
case inr
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ area a b c > area a b f
Tactic:
exfalso
State after:
case inr.h
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ False

State before:
case inr.h
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
bc : b ≠ c
bf : b ≠ f
aL : ¬online a L
hB : ¬B f b c
hlen : length b f < length b c
cf : c ≠ f
h : B f b c
⊢ False
Tactic:
exact hB h
State after:
no goals