Theorem: rescale_triangle_of_base_inductive (Pythagoras/euclid_VI.lean)

State before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = ↑Nat.zero * length b c → B b c d → area a b d = ↑Nat.zero * area a b c
Tactic:
simp
State after:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = 0 → B b c d → area a b d = 0

State before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
⊢ ∀ (d : point), online d L → length b d = 0 → B b c d → area a b d = 0
Tactic:
intros d _ hlen _
State after:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ area a b d = 0

State before:
case zero
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ area a b d = 0
Tactic:
rw [length_eq_zero_iff.mp hlen, area_of_eq a d d (by tauto)]
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
d : point
a✝¹ : online d L
hlen : length b d = 0
a✝ : B b c d
⊢ a = d ∨ a = d ∨ d = d
Tactic:
tauto
State after:
no goals

State before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
⊢ ∀ (d : point),
    online d L → length b d = ↑(Nat.succ n) * length b c → B b c d → area a b d = ↑(Nat.succ n) * area a b c
Tactic:
intros d dL hlen Bbcd
State after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have bc := ne_12_of_B Bbcd
State after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have bd := ne_13_of_B Bbcd
State after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
have cd := ne_23_of_B Bbcd
State after:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case succ
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
by_cases n0 : n = 0
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c

case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
by_cases n1 : n = 1
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c

case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
simp [Nat.cast_succ]
State after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = (↑n + 1) * area a b c

State before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = (↑n + 1) * area a b c
Tactic:
rw [add_mul]
State after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + 1 * area a b c

State before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + 1 * area a b c
Tactic:
simp [one_mul]
State after:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + area a b c

State before:
case neg
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
obtain ⟨ e, He ⟩ := rescale_length n bL cL
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
⊢ area a b d = ↑n * area a b c + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
have Bbce := He.2.2 ⟨ ge2_of_n1_n0 n0 n1, bc ⟩
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = ↑n * area a b c + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = ↑n * area a b c + area a b c
Tactic:
rw [← hn e He.1 He.2.1 Bbce]
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
⊢ area a b d = area a b e + area a b c
Tactic:
have be := ne_13_of_B Bbce
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
⊢ area a b d = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
⊢ area a b d = area a b e + area a b c
Tactic:
have ed : e ≠ d := fun ed => by
  have := He.2.1; rw [ed, hlen] at this; simp at this
  exact bc (length_eq_zero_iff.mp this)
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ area a b d = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ area a b d = area a b e + area a b c
Tactic:
have Bbed : B b e d := by
  have: length b e < length b d := by rw [He.2.1, hlen]; simp; linarith [len_pos_of_nq bc]
  have := B_of_three_online_ne_short this be bd ed bL He.1 dL
  
  cases this with
  | inl h => exact h
  | inr h =>
    exfalso
    exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm Bbce))
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
⊢ area a b d = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
⊢ area a b d = area a b e + area a b c
Tactic:
rw [((area_add_iff_B be ed bd.symm bL He.1 dL aL).mp Bbed).symm]
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
⊢ area a b e + area a d e = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
have: length b c = length e d := by
  have := length_sum_of_B Bbed
  rw [hlen, He.2.1] at this; simp [one_mul] at this; linarith
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : length b c = length e d
⊢ area a b e + area a d e = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : length b c = length e d
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
perm [eq_area_of_eq_base_samevertex a bL cL He.1 dL this]
State after:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this✝ : length b c = length e d
this : area a b c = area a d e
⊢ area a b e + area a d e = area a b e + area a b c

State before:
case neg.intro
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this✝ : length b c = length e d
this : area a b c = area a d e
⊢ area a b e + area a d e = area a b e + area a b c
Tactic:
rw [this]
State after:
no goals

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
rw [← length_sum_of_B Bbcd, n0] at hlen
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b c + length c d = ↑(Nat.succ 0) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b c + length c d = ↑(Nat.succ 0) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
simp at hlen
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
exfalso
State after:
case pos.h
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ False

State before:
case pos.h
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : n = 0
hlen : length c d = 0
⊢ False
Tactic:
exact cd (length_eq_zero_iff.mp hlen)
State after:
no goals

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
rw [← length_sum_of_B Bbcd, n1,] at hlen
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b c + length c d = ↑(Nat.succ 1) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b c + length c d = ↑(Nat.succ 1) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
simp at hlen
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b d = ↑(Nat.succ n) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b d = ↑(Nat.succ n) * area a b c
Tactic:
rw [← (area_add_iff_B bc cd bd.symm bL cL dL aL).mp Bbcd, n1]
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a d c = ↑(Nat.succ 1) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a d c = ↑(Nat.succ 1) * area a b c
Tactic:
perm
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = ↑(Nat.succ 1) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = ↑(Nat.succ 1) * area a b c
Tactic:
simp
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = (1 + 1) * area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = (1 + 1) * area a b c
Tactic:
ring_nf
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = area a b c * 2

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a b c + area a c d = area a b c * 2
Tactic:
simp [mul_two]
State after:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a c d = area a b c

State before:
case pos
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ area a c d = area a b c
Tactic:
apply (eq_area_of_eq_base_samevertex a bL cL cL dL (by linarith)).symm
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : n = 1
hlen : length b c + length c d = (1 + 1) * length b c
⊢ length b c = length c d
Tactic:
linarith
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
⊢ False
Tactic:
have := He.2.1
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : length b e = ↑n * length b c
⊢ False

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : length b e = ↑n * length b c
⊢ False
Tactic:
rw [ed, hlen] at this
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : ↑(Nat.succ n) * length b c = ↑n * length b c
⊢ False

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : ↑(Nat.succ n) * length b c = ↑n * length b c
⊢ False
Tactic:
simp at this
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : length b c = 0
⊢ False

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e = d
this : length b c = 0
⊢ False
Tactic:
exact bc (length_eq_zero_iff.mp this)
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ B b e d
Tactic:
have: length b e < length b d := by rw [He.2.1, hlen]; simp; linarith [len_pos_of_nq bc]
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
⊢ B b e d

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
⊢ B b e d
Tactic:
have := B_of_three_online_ne_short this be bd ed bL He.1 dL
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this✝ : length b e < length b d
this : B b e d ∨ B e b d
⊢ B b e d

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this✝ : length b e < length b d
this : B b e d ∨ B e b d
⊢ B b e d
Tactic:
cases this with
| inl h => exact h
| inr h =>
  exfalso
  exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm Bbce))
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ length b e < length b d
Tactic:
rw [He.2.1, hlen]
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ ↑n * length b c < ↑(Nat.succ n) * length b c

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ ↑n * length b c < ↑(Nat.succ n) * length b c
Tactic:
simp
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ ↑n * length b c < (↑n + 1) * length b c

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
⊢ ↑n * length b c < (↑n + 1) * length b c
Tactic:
linarith [len_pos_of_nq bc]
State after:
no goals

State before:
case inl
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
h : B b e d
⊢ B b e d
Tactic:
exact h
State after:
no goals

State before:
case inr
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
h : B e b d
⊢ B b e d
Tactic:
exfalso
State after:
case inr.h
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
h : B e b d
⊢ False

State before:
case inr.h
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
this : length b e < length b d
h : B e b d
⊢ False
Tactic:
exact not_B324_of_B123_B124 Bbce Bbcd (B124_of_B134_B123 h (B_symm Bbce))
State after:
no goals

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
⊢ length b c = length e d
Tactic:
have := length_sum_of_B Bbed
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : length b e + length e d = length b d
⊢ length b c = length e d

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : length b e + length e d = length b d
⊢ length b c = length e d
Tactic:
rw [hlen, He.2.1] at this
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : ↑n * length b c + length e d = ↑(Nat.succ n) * length b c
⊢ length b c = length e d

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : ↑n * length b c + length e d = ↑(Nat.succ n) * length b c
⊢ length b c = length e d
Tactic:
simp [one_mul] at this
State after:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : ↑n * length b c + length e d = (↑n + 1) * length b c
⊢ length b c = length e d

State before:
i : incidence_geometry
a b c : point
L : line
bL : online b L
cL : online c L
aL : ¬online a L
n : ℕ
hn : ∀ (d : point), online d L → length b d = ↑n * length b c → B b c d → area a b d = ↑n * area a b c
d : point
dL : online d L
hlen : length b d = ↑(Nat.succ n) * length b c
Bbcd : B b c d
bc : b ≠ c
bd : b ≠ d
cd : c ≠ d
n0 : ¬n = 0
n1 : ¬n = 1
e : point
He : online e L ∧ length b e = ↑n * length b c ∧ (n ≥ 2 ∧ b ≠ c → B b c e)
Bbce : B b c e
be : b ≠ e
ed : e ≠ d
Bbed : B b e d
this : ↑n * length b c + length e d = (↑n + 1) * length b c
⊢ length b c = length e d
Tactic:
linarith
State after:
no goals