Theorem: lt_area_of_lt_base_sameedge (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
⊢ 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
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
hlen : length b c > length b f
⊢ area a b c > area a b f
Tactic:
by_cases Bfbc: B f b c
State after:
case pos
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
hlen : length b c > length b f
Bfbc : B f b c
⊢ area a b c > area a b f

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

State before:
case pos
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
hlen : length b c > length b f
Bfbc : B f b c
⊢ area a b c > area a b f
Tactic:
obtain ⟨ e, He ⟩ := rescale_length 2 fL bL
State after:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ area a b c > area a b f

State before:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ area a b c > area a b f
Tactic:
have Bfbe := He.2.2 ⟨ by simp [ge_iff_le], bf.symm ⟩
State after:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ area a b c > area a b f

State before:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ area a b c > area a b f
Tactic:
have Lbe : length b e = length b f := by
  perm [length_sum_of_B Bfbe]; perm at He; norm_cast at this He; linarith
State after:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b f

State before:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b f
Tactic:
rw [← eq_area_of_eq_base_samevertex a bL He.1 bL fL Lbe]
State after:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e

State before:
case pos.intro
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Tactic:
rw [← Lbe] at hlen
State after:
case pos.intro
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
Bfbc : B f b c
e : point
hlen : length b c > length b e
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e

State before:
case pos.intro
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
Bfbc : B f b c
e : point
hlen : length b c > length b e
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
Lbe : length b e = length b f
⊢ area a b c > area a b e
Tactic:
exact lt_area_of_lt_base_sameedge_nBfbc a bL cL He.1 bc (ne_23_of_B Bfbe) aL (not_B324_of_B123_B124 Bfbe Bfbc) hlen
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
⊢ 2 ≥ 2
Tactic:
simp [ge_iff_le]
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
⊢ length b e = length b f
Tactic:
perm [length_sum_of_B Bfbe]
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length 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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length f e = ↑2 * length f b ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Tactic:
perm at He
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length e f = ↑2 * length b f ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length 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
hlen : length b c > length b f
Bfbc : B f b c
e : point
He : online e L ∧ length e f = ↑2 * length b f ∧ (2 ≥ 2 ∧ f ≠ b → B f b e)
Bfbe : B f b e
this : length b f + length b e = length e f
⊢ length b e = length b f
Tactic:
norm_cast at this He
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
hlen : length b c > length b f
Bfbc : B f b c
e : point
Bfbe : B f b e
this : length b f + length b e = length e f
He : online e L ∧ length e f = 2 * length b f ∧ (True ∧ ¬f = b → B f b e)
⊢ length b e = length 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
hlen : length b c > length b f
Bfbc : B f b c
e : point
Bfbe : B f b e
this : length b f + length b e = length e f
He : online e L ∧ length e f = 2 * length b f ∧ (True ∧ ¬f = b → B f b e)
⊢ length b e = length b f
Tactic:
linarith
State after:
no goals

State before:
case neg
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
hlen : length b c > length b f
Bfbc : ¬B f b c
⊢ area a b c > area a b f
Tactic:
exact lt_area_of_lt_base_sameedge_nBfbc a bL cL fL bc bf aL Bfbc hlen
State after:
no goals