Theorem: rescale_triangle_of_base_notcbd (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
⊢ area a b d = ↑n * area a b c
Tactic:
by_cases n1 : n =1
State after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c

case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c

State before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
have cd: c ≠ d := fun cd => by
  have n0 := length_eq_zero_iff.not.mpr bd
  rw [cd] at hlen; field_simp at hlen; exact n1 hlen
State after:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ area a b d = ↑n * area a b c

State before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ area a b d = ↑n * area a b c
Tactic:
have: length b c < length b d := by
  have := len_pos_of_nq bc
  have n_ge1 := gt1_of_n1_n0 n0 n1; simp [*]
State after:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
⊢ area a b d = ↑n * area a b c

State before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
⊢ area a b d = ↑n * area a b c
Tactic:
have hBs := B_of_three_online_ne_short this bc bd cd bL cL dL
State after:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d ∨ B c b d
⊢ area a b d = ↑n * area a b c

State before:
case neg
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d ∨ B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
cases hBs with
| inl hBs => exact rescale_triangle_of_base_B a bL cL dL hlen hBs aL
| inr hBs => exfalso; exact hB hBs
State after:
no goals

State before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n1] at hlen
State after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c

State before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑n * area a b c
Tactic:
rw [n1]
State after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑1 * area a b c

State before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑1 * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
⊢ area a b d = ↑1 * area a b c
Tactic:
simp [Nat.cast_one] at hlen
State after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = ↑1 * area a b c

State before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = ↑1 * area a b c
Tactic:
simp [Nat.cast_one]
State after:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = area a b c

State before:
case pos
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : n = 1
hlen : length b d = length b c
⊢ area a b d = area a b c
Tactic:
exact (eq_area_of_eq_base_samevertex a bL cL bL dL hlen.symm).symm
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
⊢ False
Tactic:
have n0 := length_eq_zero_iff.not.mpr bd
State after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Tactic:
rw [cd] at hlen
State after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b d
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b d
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
⊢ False
Tactic:
field_simp at hlen
State after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
hlen : n = 1
⊢ False

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hB : ¬B c b d
bc : b ≠ c
n0✝ : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c = d
n0 : ¬length b d = 0
hlen : n = 1
⊢ False
Tactic:
exact n1 hlen
State after:
no goals

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
⊢ length b c < length b d
Tactic:
have := len_pos_of_nq bc
State after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
⊢ length b c < length b d

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
⊢ length b c < length b d
Tactic:
have n_ge1 := gt1_of_n1_n0 n0 n1
State after:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
n_ge1 : n > 1
⊢ length b c < length b d

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : 0 < length b c
n_ge1 : n > 1
⊢ length b c < length b d
Tactic:
simp [*]
State after:
no goals

State before:
case neg.inl
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B b c d
⊢ area a b d = ↑n * area a b c
Tactic:
exact rescale_triangle_of_base_B a bL cL dL hlen hBs aL
State after:
no goals

State before:
case neg.inr
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ area a b d = ↑n * area a b c
Tactic:
exfalso
State after:
case neg.inr.h
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ False

State before:
case neg.inr.h
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
hB : ¬B c b d
bc : b ≠ c
n0 : n ≠ 0
bd : b ≠ d
aL : ¬online a L
n1 : ¬n = 1
cd : c ≠ d
this : length b c < length b d
hBs : B c b d
⊢ False
Tactic:
exact hB hBs
State after:
no goals