Theorem: lt_area_of_lt_base_sameedge_Bbfc (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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
⊢ length b c > length b f → area a b c > area a b f
Tactic:
have := (area_add_iff_B bf cf.symm bc.symm bL fL cL aL).mp hB
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
⊢ 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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
⊢ length b c > length b f → area a b c > area a b f
Tactic:
intro
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : 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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b c > area a b f
Tactic:
rw [← this]
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b f + area a c f > 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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a b f + area a c f > area a b f
Tactic:
simp [gt_iff_lt, lt_add_iff_pos_right]
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ 0 < area a c 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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ 0 < area a c f
Tactic:
have : area a c f ≠ 0 := by perma [(area_zero_iff_online cf cL fL).not.mpr aL]
State after:
i : incidence_geometry
a b c f : point
L : line
bL : online b L
cL : online c L
fL : online f L
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this✝ : area a b f + area a c f = area a b c
a✝ : length b c > length b f
this : area a c f ≠ 0
⊢ 0 < area a c 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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this✝ : area a b f + area a c f = area a b c
a✝ : length b c > length b f
this : area a c f ≠ 0
⊢ 0 < area a c f
Tactic:
exact (Ne.symm this).lt_of_le (area_nonneg a c f)
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
hB : B b f c
bc : b ≠ c
bf : b ≠ f
cf : c ≠ f
aL : ¬online a L
this : area a b f + area a c f = area a b c
a✝ : length b c > length b f
⊢ area a c f ≠ 0
Tactic:
perma [(area_zero_iff_online cf cL fL).not.mpr aL]
State after:
no goals